Stream: Coq users

Topic: Typeclass modes and instances in scope


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 05 2020 at 23:17):

IIRC the manual, it documents such an instance has automatically priority over your instance for option.

view this post on Zulip 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) := ...

view this post on Zulip Brandon Moore (Nov 05 2020 at 23:19):

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?

view this post on Zulip Paolo Giarrusso (Nov 05 2020 at 23:19):

yes

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 05 2020 at 23:21):

Instance Empty_set_equiv : Equiv Empty_set := λ _ _, True.

view this post on Zulip Paolo Giarrusso (Nov 05 2020 at 23:24):

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 *)

view this post on Zulip Paolo Giarrusso (Nov 05 2020 at 23:25):

as a fix it sounds horrible, but this part of std++ seems to work pretty well here.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 05 2020 at 23:34):

are you using 8.12 already (to get those fixes)?

view this post on Zulip 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)).

view this post on Zulip Paolo Giarrusso (Nov 05 2020 at 23:37):

in stdpp style, you'd end up with some notation, say <>?, and a variant with type arguments, here <>?@{T}, and then write:

view this post on Zulip Paolo Giarrusso (Nov 05 2020 at 23:38):

... : CompareReflexive (<>?@{T})

view this post on Zulip Paolo Giarrusso (Nov 05 2020 at 23:39):

ahem, for that you'd also need Notation (<>?@{T}) := (compare (X := T)).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Brandon Moore (Nov 11 2020 at 20:03):

Yes, that's the direction it actually is. Just a typo here.

view this post on Zulip Gaëtan Gilbert (Nov 11 2020 at 20:05):

I guess because Structure isn't actually a class.

yes

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Paolo Giarrusso (Nov 11 2020 at 22:00):

Why not make that record a class?

view this post on Zulip Paolo Giarrusso (Nov 11 2020 at 22:01):

"Existing Class Structure." will do it.

view this post on Zulip Karl Palmskog (Nov 11 2020 at 22:03):

yes, that's how it ended up (but at the upstream definition)


Last updated: Jan 27 2023 at 01:03 UTC