Better errors when tactic fails to automatically resolve some side-condition
@robbertkrebbers and me sketched a plan (or rather, two possible plans) for how to show better error messages for common stumbling blocks, such as iMod
with mismatching masks:
-
ElimModal
already has support for a pure side-condition; we could introduce something like
Definition pm_error (s : string) := False
and add instances with error "foo"
as their side-condition; together with some support in iSolveSideCondition
this could be used to then show better, instance-specific error messages when iMod
fails.
- We could add a new typeclass like
ElimModalError
that is used to compute an error message whenElimModal
failed to find an instance.
Since this is used for diagnostics only, there are no backwards compatibility concerns -- so I feel like we should start with the first approach, since it is easy to implement; we can always switch to something more principled later.
Edited by Ralf Jung