Stream: Coq devs & plugin devs

Topic: Hint Constants Opaque breaks trivial unification problems?


view this post on Zulip Jason Gross (Mar 01 2023 at 22:39):

What's going on at https://github.com/coq/coq/issues/17323?

Debug: 1.1: exact TemplateMonad_Monad on (Monad ?m6) failed with: Cannot unify TemplateMonad and TemplateMonad
Debug: 1.1: exact option_monad on (Monad ?m6) failed with: Cannot unify option and option

(I'll try to set up coqbot to minimize shortly)

view this post on Zulip Paolo Giarrusso (Mar 01 2023 at 22:48):

Please print logs with Set Printing All

view this post on Zulip Paolo Giarrusso (Mar 01 2023 at 22:51):

Nevermind, I see that would not make a difference...

view this post on Zulip Paolo Giarrusso (Mar 01 2023 at 22:52):

(I'm used to terms hiding constants that must be transparent, but that seems unlikely here unless there's a hidden coercion in your goal)

view this post on Zulip Jason Gross (Mar 01 2023 at 23:28):

This was already with Set Printing All. Even with Set Printing Universes I still get "Cannot unify option and option"

view this post on Zulip Paolo Giarrusso (Mar 01 2023 at 23:55):

Have you already bisected if there are constants you can make Hint Transparent for these problems to succeed again, and if the problem is indeed due to universe polymorphism? Not that I see any non-buggy option

view this post on Zulip Jason Gross (Mar 02 2023 at 00:01):

Here are some logs with constants opaque vs not, with and without printing universes opaque.log opaque-nounivs.log transparent.log transparent-nounivs.log

Without Hint Constants Opaque, the logs begin with

Debug: Calling typeclass resolution with flags: depth = ,unique = false,do_split = true,fail = false
Debug: Starting resolution with 32 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded
Debug: Launching resolution fixpoint on 32 goals:
?X294 : (Monad TemplateMonad)
?X303 : (Monad TemplateMonad)
?X314 : (Monad TemplateMonad)
?X336 : (Monad TemplateMonad)
?X345 : (Monad TemplateMonad)
?X388 : (Monad TemplateMonad)
?X397 : (Monad TemplateMonad)
?X405 : (Monad TemplateMonad)
?X420 : (Monad TemplateMonad)
?X430 : (Monad TemplateMonad)
?X439 : (Monad TemplateMonad)
?X445 : (Monad TemplateMonad)
?X452 : (Monad TemplateMonad)
?X461 : (Monad TemplateMonad)
?X478 : (Monad TemplateMonad)
?X486 : (Monad TemplateMonad)
?X495 : (Monad TemplateMonad)
?X509 : (Monad TemplateMonad)
?X543 : (Monad TemplateMonad)
?X552 : (Monad TemplateMonad)
?X565 : (Monad TemplateMonad)
?X612 : (Monad TemplateMonad)
?X620 : (Monad TemplateMonad)
?X635 : (Monad TemplateMonad)
?X652 : (Monad TemplateMonad)
?X661 : (Monad TemplateMonad)
?X674 : (Monad TemplateMonad)

while with Hint Constants Opaque, the logs begin with

Debug: Calling typeclass resolution with flags: depth = ,unique = false,do_split = true,fail = false
Debug: Starting resolution with 32 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded
Debug: Launching resolution fixpoint on 32 goals:
?X294 : (Monad ?m6)
?X303 : (Monad ?m7)
?X314 : (Monad ?m8)
?X336 : (Monad ?m9)
?X345 : (Monad ?m10)
?X388 : (Monad ?T1)
?X397 : (Monad ?m2)
?X405 : (Monad ?m3)
?X420 : (Monad ?m)
?X430 : (Monad ?m20)
?X439 : (Monad ?m18)
?X445 : (Monad ?T7)
?X452 : (Monad ?m17)
?X461 : (Monad ?T8)
?X478 : (Monad ?T0)
?X486 : (Monad ?m4)
?X495 : (Monad ?T3@{c0:=cst_universes cb})
?X509 : (Monad ?m5)
?X543 : (Monad ?m0)
?X552 : (Monad ?T2)
?X565 : (Monad ?m1)
?X612 : (Monad ?m13)
?X620 : (Monad ?m12)
?X635 : (Monad ?m11)
?X652 : (Monad ?m14)
?X661 : (Monad ?T6)
?X674 : (Monad ?m15)

Note that Monad and TemplateMonad are both inductive types.

view this post on Zulip Jason Gross (Mar 02 2023 at 00:02):

I'm not sure what constants I should be looking at to make transparent. Like, Typeclasses Transparent TemplateMonad, for example, says Error: Cannot coerce TemplateMonad to an evaluable reference., and I don't see anything in sight, typeclass-wise, that is even a candidate for unfolding...

view this post on Zulip Jason Gross (Mar 02 2023 at 05:46):

There's now a standalone example at https://github.com/coq/coq/issues/17323#issuecomment-1451332183

view this post on Zulip Matthieu Sozeau (Mar 02 2023 at 07:17):

It’s strange that it has an impact on the goals before calling TC resolution…

view this post on Zulip Gaëtan Gilbert (Mar 02 2023 at 10:42):

found it, see issue


Last updated: Dec 07 2023 at 17:01 UTC