Jason Gross (Mar 01 2023 at 22:39): 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)
Paolo Giarrusso (Mar 01 2023 at 22:48):Please print logs with Set Printing All
Paolo Giarrusso (Mar 01 2023 at 22:51):Nevermind, I see that would not make a difference...
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)
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"
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
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.
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...
Jason Gross (Mar 02 2023 at 05:46):There's now a standalone example at https://github.com/coq/coq/issues/17323#issuecomment-1451332183
Matthieu Sozeau (Mar 02 2023 at 07:17):It’s strange that it has an impact on the goals before calling TC resolution…
Gaëtan Gilbert (Mar 02 2023 at 10:42):found it, see issue
Last updated: Jun 04 2023 at 19:30 UTC