1 files changed, 83 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3166.v b/test-suite/bugs/opened/3166.v
new file mode 100644
index 00000000..e1c29a95
--- /dev/null
+++ b/test-suite/bugs/opened/3166.v
@@ -0,0 +1,83 @@
+Set Asymmetric Patterns.
+
+Section eq.
+  Let A := { X : Type & X }.
+  Let B := (fun x : A => projT1 x).
+  Let T := (fun (a' : A) (b' : B a') => projT2 a' = b').
+  Let T' := T.
+  Let t1T := (fun _ : A => unit).
+  Let f1 := (fun x (_ : t1T x) => projT2 x).
+  Let t1 := (fun x (y : t1T x) => @eq_refl (projT1 x) (projT2 x)).
+  Let t1T' := t1T.
+  Let f1' := f1.
+  Let t1' := t1.
+
+  Theorem eq_matches_commute
+          a' b' (t' : T a' b')
+          (rta : forall b'', T' a' b'' -> A)
+          (rtb : forall b'' t'', B (rta b'' t''))
+          (rt1 : forall y, T _ (rtb (f1' a' y) (@t1' a' y)))
+          (R : forall (b : B (rta b' t')), T _ b -> Type)
+          (r1 : forall y, R (f1 _ y) (@t1 _ y))
+  : match
+      match t' as t0' in (@eq _ _ b0') return T (rta b0' t0') (rtb b0' t0') with
+        | eq_refl => rt1 tt
+      end
+      as t0 in (@eq _ _ b0)
+      return R b0 t0
+    with
+      | eq_refl => r1 tt
+    end
+    =
+    match t'
+          as t0' in (@eq _ _ b0')
+          return (forall (R : forall (b : B (rta b0' t0')), T _ b -> Type)
+                         (r1 : forall y, R (f1 _ y) (@t1 _ y)),
+                    R _ (match t0' as t0'0 in (@eq _ _ b0'0) return T (rta b0'0 t0'0) (rtb b0'0 t0'0) with
+                           | eq_refl => rt1 tt
+                         end))
+    with
+      | eq_refl => fun _ r1 =>
+                      match rt1 tt with
+                        | eq_refl => r1 tt
+                      end
+    end R r1.
+  Proof.
+    destruct t'; reflexivity.
+  Defined.
+
+  Theorem eq_match_beta2
+          a b (t : T a b)
+          X
+          (R : forall b' (t' : T a b'), X b' -> Type)
+          (r1 : forall y x, R _ (@t1 _ y) x)
+          x
+  : match t as t' in (@eq _ _ b') return forall x, R b' t' x with
+      | eq_refl => r1 tt
+    end (x b)
+    =
+    match t as t' in (@eq _ _ b') return R b' t' (x b') with
+      | eq_refl => r1 tt (x _)
+    end.
+  Proof.
+    destruct t; reflexivity.
+  Defined.
+End eq.
+
+Definition typeof {T} (_ : T) := T.
+
+Eval compute in (eq_sym (eq_sym _)).
+Goal forall T (x y : T) (p : x = y), True.
+  intros.
+  pose proof
+       (@eq_matches_commute
+          (existT (fun T => T) T x) y p
+          (fun b'' _ => existT (fun T => T) T b'')
+          (fun _ _ => x)
+          (fun _ => eq_refl)
+          (fun x' _ => x' = y)
+          (fun _ => eq_refl)
+        ) as H0.
+  compute in H0.
+  change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0.
+  Fail pose proof (fun k => @eq_trans _ _ _ k H0).