Brandon Moore (Nov 05 2020 at 21:51): Brandon Moore (Nov 05 2020 at 21:51):I'm trying add modes to some code where instances like StrictlyComparable X -> StrictlyComparable (option X) can lead to diverging instance searches, but it turns out the code also has places where some instances are directly in scope as hypotheses, and completely ambiguous goals are expected to be solved by trying the instances in scope. For example, compare is a field of our StrictlyComparable so this happens even in the type signature of
Lemma option_compare_reflexive
(X : Type)
{Xsc : StrictlyComparable X}
: CompareReflexive (option_compare compare).
If I try to set a mod StrictlyComparable ! this declaration is rejected complaining about an unsolvable goal of the form StrictlyComparable ?G. It's also rejected if I Set Typeclasses Filtered Unification, which surprised me. Is there any way to support code like this while preventing the diverging instance searches?
Brandon Moore (Nov 05 2020 at 21:57):Also, this is the first time I've ever tried the option, but it seems Set Typeclasses Filtered Unification completely breaks setoid rewriting. I guess many Proper instances need fancy unification.
Paolo Giarrusso (Nov 05 2020 at 23:17):per my usual, I looked at stdpp, and I suggest adding an instance StrictlyComparable T for a ground type T.
Paolo Giarrusso (Nov 05 2020 at 23:17):IIRC the manual, it documents such an instance has automatically priority over your instance for option.
Paolo Giarrusso (Nov 05 2020 at 23:19):They have both:
Class Equiv A := equiv: relation A.
(* No Hint Mode set because of Coq bug #5735
Hint Mode Equiv ! : typeclass_instances. *)
and
Instance option_equiv `{Equiv A} : Equiv (option A) := ...
Do you mean not trying to set the mode, and adding an instance for a particular concrete ground type to try to avoid the searches going wrong?
Paolo Giarrusso (Nov 05 2020 at 23:19):yes
Paolo Giarrusso (Nov 05 2020 at 23:21):setting the mode would be better, of course, but it has issues — those are now closed (and fixed?), but I am not sure solving those issues would help in your case
Paolo Giarrusso (Nov 05 2020 at 23:21):meanwhile, in stdpp divergence doesn't happen, thanks to such an issue:
Goal { A : Type & Equiv A }.
eexists.
Set Typeclasses Debug.
apply _.
About Empty_set_equiv.
Instance Empty_set_equiv : Equiv Empty_set := λ _ _, True.
and the only thing saving stdpp seems priority, since changing priority does cause a loop — the code below might flood your system:
Instance option_equiv `{Equiv A} : Equiv (option A) | 0 := option_Forall2 (≡).
Goal { A : Type & Equiv A }.
eexists.
Set Typeclasses Debug.
timeout 1 apply _. (* loops, floods editor, and doesn't even time out *)
as a fix it sounds horrible, but this part of std++ seems to work pretty well here.
Brandon Moore (Nov 05 2020 at 23:30):It looks like the referenced bugs were closed. And looking closer, a lot of the code that didn't work with the mode looks bad. Like writing Goal forall {Equiv X} a, equiv a a and expecting a to get type X just because it's the most obvious Equiv instance. With this suggestion it might randomly decide a:T` instead. I think we should just change the code and not rely on this behavior.
Paolo Giarrusso (Nov 05 2020 at 23:34):are you using 8.12 already (to get those fixes)?
Paolo Giarrusso (Nov 05 2020 at 23:36):but I agree that CompareReflexive (option_compare compare). seems like it should be written `
Instance option_compare_reflexive `{Xsc : !StrictlyComparable X} : CompareReflexive (compare (X := option X)).
in stdpp style, you'd end up with some notation, say <>?, and a variant with type arguments, here <>?@{T}, and then write:
Paolo Giarrusso (Nov 05 2020 at 23:38):... : CompareReflexive (<>?@{T})
Paolo Giarrusso (Nov 05 2020 at 23:39):ahem, for that you'd also need Notation (<>?@{T}) := (compare (X := T)).
Brandon Moore (Nov 05 2020 at 23:40):I don't think we're depending on things affected by those bugs. Certainly not on purpose.
Brandon Moore (Nov 11 2020 at 19:59):Now I seem to be running into something with typeclass modes and context variables. I have a class like Ops (x:Type) with mode !, a record/product like Structure (x:Type), and a function forall x, Structure x -> Ops x registered as an instance. In a section with context (X:Type)(structure:Structure X) a goal Ops X isn't solved by typeclasses eauto. Debug shows it's not even trying the hint.
I thought the manual says the mode ! excludes only terms whose head is an evar, so I wouldn't expect the mode to prevent the instance from applying.
Brandon Moore (Nov 11 2020 at 20:02):Oh, Verbosity 2 shows that is applying the instance and attempting a recursive goal for Structure X as expected, but not finding the value from the context. I guess because Structure isn't actually a class.
Gaëtan Gilbert (Nov 11 2020 at 20:02):
forall x, Ops x -> Structure x
shouldn't it be Structrure -> Ops to solve an Ops goal?
Brandon Moore (Nov 11 2020 at 20:03):Yes, that's the direction it actually is. Just a typo here.
Gaëtan Gilbert (Nov 11 2020 at 20:05):I guess because Structure isn't actually a class.
yes
Brandon Moore (Nov 11 2020 at 20:08):I thought auto/eauto/typeclasses eauto automatically tried assumption. Not sure if it's a good idea compared to making it a class, but a Hint Extern 4 (Structure _) => assumption : typeclass_instances lets that typeclass search succeed.
Brandon Moore (Nov 11 2020 at 20:10):Well, that worked in most places, but I also hit an Anomaly "grounding a non evar-free term"
Paolo Giarrusso (Nov 11 2020 at 22:00):Why not make that record a class?
Paolo Giarrusso (Nov 11 2020 at 22:01):"Existing Class Structure." will do it.
Karl Palmskog (Nov 11 2020 at 22:03):yes, that's how it ended up (but at the upstream definition)
Last updated: Oct 13 2024 at 01:02 UTC