You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
For a term t, Check @eq_refl _ t. gives tt = tt but Check @eq_refl _ t : tt = tt fails.
The root cause (for which I reverse engineered an example) is that CClosure.conv cannot access the qmap to normalize qvars during its conversions, yet such unification qvars may appear.
The issue also arises when I try to implement non-linear rewrite rules using the same function for testing conversion.
Small Coq file to reproduce the bug
#[universes(polymorphic)]
Inductive sig@{s s' s''|u v| } {A:Type@{s|u}} (P:A -> Type@{s'|v}) : Type@{s''|max(u,v)} :=
exist : forall x:A, P x -> sig P.
Notation "{ x : A & P }" := (sig (A:=A) (fun x => P)) (at level 0, x at level 99) : type_scope.
#[universes(polymorphic)]
Definition proj1_sig@{s s'|u v| } {A:Type@{s|u}} {P:A -> Type@{s'|v}} (e:sig@{_ _ s|_ _} P) :=
match e with
| exist _ a b => a
end.
Notation "x .1" := (proj1_sig x) (at level 1, left associativity, format "x .1").
Definition projT1_eq {A} {P : A -> Type} {u v : { a : A & P a }} (p : u = v) : u.1 = v.1
:= match p with eq_refl => eq_refl end.
Context {A} {P : A -> Type} {u : { a : A & P a }} (b : P u.1).
Set Definitional UIP.
Inductive SEq (A : Type) (a : A) : forall (B : Type), B -> SProp := Seq_refl : SEq A a A a.
Check
@eq_refl _
((fun (A : Type) (a : A) (B: Type) (b : B) (e : SEq A a B b) =>
match e with Seq_refl _ _ => tt end) _ (P u.1) _ (P u.1)
((fun x : SEq _ (P u.1) _ (P u.1) => x) (Seq_refl _ _))).
Check @eq_refl _
((fun (A : Type) (a : A) (B: Type) (b : B) (e : SEq A a B b) =>
match e with Seq_refl _ _ => tt end) _ (P u.1) _ (P u.1)
((fun x : SEq _ (P u.1) _ (P u.1) => x) (Seq_refl _ _)))
: tt = tt.
Version of Coq where this bug occurs
8.19.1, master (fc1b697e47)
Last version of Coq where the bug did not occur
No response
The text was updated successfully, but these errors were encountered:
Description of the problem
For a term
t
,Check @eq_refl _ t.
givestt = tt
butCheck @eq_refl _ t : tt = tt
fails.The root cause (for which I reverse engineered an example) is that
CClosure.conv
cannot access theqmap
to normalizeqvars
during its conversions, yet such unification qvars may appear.The issue also arises when I try to implement non-linear rewrite rules using the same function for testing conversion.
Small Coq file to reproduce the bug
Version of Coq where this bug occurs
8.19.1, master (
fc1b697e47
)Last version of Coq where the bug did not occur
No response
The text was updated successfully, but these errors were encountered: