Quentin VERMANDE (Jan 10 2024 at 16:48): Quentin VERMANDE (Jan 10 2024 at 16:48):I found a unification problem which fails when triggered with coq.unify-eq but succeeds when triggered with Check. The unification debug messages are exactly the same (up to the first message in the Check version). They both end with
[unification] tt|
?c|ZCase(_UNBOUND_REL_1)
but only in the Check case does ?c get instantiated. Why is that ? Is there a way to ask for ?c to be instantiated ?
From elpi Require Import elpi.
Class C1 (T : Type) := {x1 : unit}.
Structure S1 := {sort1 :> Type; class1 : C1 sort1}.
Canonical generic_S1 (T : Type) (c : C1 T) := Build_S1 T c.
Class C2 (T : Type) := {x2 : unit}.
Structure S2 := {sort2 :> Type; class2 : C2 sort2}.
Canonical generic_S2 (T : Type) (c : C2 T) := Build_S2 T c.
Definition C2_to_1 (T : Type) (c : C2 T) := Build_C1 T (@x2 T c).
Definition S2_to_1 (x : S2) := Build_S1 x (C2_to_1 (sort2 x) (class2 x)).
Coercion S2_to_1 : S2 >-> S1.
Instance natC2 : C2 nat := Build_C2 nat tt.
Axiom f : S1 -> Type.
Set Debug "unification".
Check fun (x : f (generic_S1 nat (Build_C1 nat tt))) => x : f (@S2_to_1 (@generic_S2 nat _)).
Elpi Command foo.
Elpi Query lp:{{
coq.unify-eq {{ generic_S1 nat (Build_C1 nat tt) }}
{{ @S2_to_1 (@generic_S2 nat lp:X) }} R.
}}.
Last updated: Oct 13 2024 at 01:02 UTC