Thibaut Pérami (Mar 14 2024 at 16:13): Thibaut Pérami (Mar 14 2024 at 16:13):Hi, I've embarked on a doomed quest of making my typeclass error messages more readable. My main problem is the following:
Class A := {}.
Class B := {}.
Global Instance AB `{A} : B := {}.
Goal B.
apply _.
This gives: Error: Cannot infer this placeholder of type "B" (no type class instance found).
But I would like a way to explain to Coq that the AB instance is canonical and safe, so that it can instead complain about not finding A. In complicated setups figuring out which classes are missing deep into the search tree at the leaves is really a pain.
So far I've tried typeclass eauto best_effort and using Set Typeclass Unique Instances, but neither worked to achieve that. Is this something that currently exists in Coq, or not at all?
Last updated: Oct 13 2024 at 01:02 UTC