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:
ElimModalalready 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
- We could add a new typeclass like
ElimModalErrorthat is used to compute an error message when
ElimModalfailed 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.