Merge PR #7776: [ssr] Fix rewrite with universes

4 files changed, 108 insertions, 7 deletions

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 2c046190f4..7fe2421f90 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -47,6 +47,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
     let cl = EConstr.Unsafe.to_constr cl in
     try fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1
     with NoMatch -> redex_of_pattern ~resolve_typeclasses:true env pat, cl in
+  let gl = pf_merge_uc ucst gl in
   let c = EConstr.of_constr c in
   let cl = EConstr.of_constr cl in
   if Termops.occur_existential sigma c then errorstrm(str"The pattern"++spc()++
@@ -56,7 +57,6 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
   | Cast(t, DEFAULTcast, ty) -> t, (gl, ty)
   | _ -> c, pfe_type_of gl c in
   let cl' = EConstr.mkLetIn (Name id, c, cty, cl) in
-  let gl = pf_merge_uc ucst gl in
   Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl cl')) (introid id) gl
 
 open Util
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index c20e415b43..9d9b1b2e8c 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -561,8 +561,8 @@ let filter_upat i0 f n u fpats =
   let na = Array.length u.up_a in
   if n < na then fpats else
   let np = match u.up_k with
-  | KpatConst when equal u.up_f f -> na
-  | KpatFixed when equal u.up_f f -> na 
+  | KpatConst when eq_constr_nounivs u.up_f f -> na
+  | KpatFixed when eq_constr_nounivs u.up_f f -> na
   | KpatEvar k when isEvar_k k f -> na
   | KpatLet when isLetIn f -> na
   | KpatLam when isLambda f -> na
@@ -582,8 +582,8 @@ let filter_upat_FO i0 f n u fpats =
   let np = nb_args u.up_FO in
   if n < np then fpats else
   let ok = match u.up_k with
-  | KpatConst -> equal u.up_f f 
-  | KpatFixed -> equal u.up_f f 
+  | KpatConst -> eq_constr_nounivs u.up_f f
+  | KpatFixed -> eq_constr_nounivs u.up_f f
   | KpatEvar k -> isEvar_k k f
   | KpatLet -> isLetIn f
   | KpatLam -> isLambda f
@@ -764,8 +764,8 @@ let mk_tpattern_matcher ?(all_instances=false)
       let match_let f = match kind f with
       | LetIn (_, v, _, b) -> unif_EQ env sigma pv v && unif_EQ env' sigma pb b
       | _ -> false in match_let
-    | KpatFixed -> equal u.up_f
-    | KpatConst -> equal u.up_f
+    | KpatFixed -> eq_constr_nounivs u.up_f
+    | KpatConst -> eq_constr_nounivs u.up_f
     | KpatLam -> fun c ->
        (match kind c with
        | Lambda _ -> unif_EQ env sigma u.up_f c
diff --git a/test-suite/ssr/rew_polyuniv.v b/test-suite/ssr/rew_polyuniv.v
new file mode 100644
index 0000000000..e2bbbc9ecc
--- /dev/null
+++ b/test-suite/ssr/rew_polyuniv.v
@@ -0,0 +1,90 @@
+From Coq Require Import Utf8 Setoid ssreflect.
+Set Default Proof Using "Type".
+
+Local Set Universe Polymorphism.
+
+(** Telescopes *)
+Inductive tele : Type :=
+  | TeleO : tele
+  | TeleS {X} (binder : X → tele) : tele.
+
+Arguments TeleS {_} _.
+
+(** The telescope version of Coq's function type *)
+Fixpoint tele_fun (TT : tele) (T : Type) : Type :=
+  match TT with
+  | TeleO => T
+  | TeleS b => ∀ x, tele_fun (b x) T
+  end.
+
+Notation "TT -t> A" :=
+  (tele_fun TT A) (at level 99, A at level 200, right associativity).
+
+(** A sigma-like type for an "element" of a telescope, i.e. the data it
+  takes to get a [T] from a [TT -t> T]. *)
+Inductive tele_arg : tele → Type :=
+| TargO : tele_arg TeleO
+(* the [x] is the only relevant data here *)
+| TargS {X} {binder} (x : X) : tele_arg (binder x) → tele_arg (TeleS binder).
+
+Definition tele_app {TT : tele} {T} (f : TT -t> T) : tele_arg TT → T :=
+  λ a, (fix rec {TT} (a : tele_arg TT) : (TT -t> T) → T :=
+     match a in tele_arg TT return (TT -t> T) → T with
+     | TargO => λ t : T, t
+     | TargS x a => λ f, rec a (f x)
+     end) TT a f.
+Arguments tele_app {!_ _} _ !_ /.
+
+Coercion tele_arg : tele >-> Sortclass.
+Coercion tele_app : tele_fun >-> Funclass.
+
+(** Inversion lemma for [tele_arg] *)
+Lemma tele_arg_inv {TT : tele} (a : TT) :
+  match TT as TT return TT → Prop with
+  | TeleO => λ a, a = TargO
+  | TeleS f => λ a, ∃ x a', a = TargS x a'
+  end a.
+Proof. induction a; eauto. Qed.
+Lemma tele_arg_O_inv (a : TeleO) : a = TargO.
+Proof. exact (tele_arg_inv a). Qed.
+Lemma tele_arg_S_inv {X} {f : X → tele} (a : TeleS f) :
+  ∃ x a', a = TargS x a'.
+Proof. exact (tele_arg_inv a). Qed.
+
+(** Operate below [tele_fun]s with argument telescope [TT]. *)
+Fixpoint tele_bind {U} {TT : tele} : (TT → U) → TT -t> U :=
+  match TT as TT return (TT → U) → TT -t> U with
+  | TeleO => λ F, F TargO
+  | @TeleS X b => λ (F : TeleS b → U) (x : X), (* b x -t> U *)
+                  tele_bind (λ a, F (TargS x a))
+  end.
+Arguments tele_bind {_ !_} _ /.
+
+(* Show that tele_app ∘ tele_bind is the identity. *)
+Lemma tele_app_bind {U} {TT : tele} (f : TT → U) x :
+  (tele_app (tele_bind f)) x = f x.
+Proof.
+  induction TT as [|X b IH]; simpl in *.
+  - rewrite (tele_arg_O_inv x). auto.
+  - destruct (tele_arg_S_inv x) as [x' [a' ->]]. simpl.
+    rewrite IH. auto.
+Qed.
+
+(** Notation-compatible telescope mapping *)
+(* This adds (tele_app ∘ tele_bind), which is an identity function, around every
+   binder so that, after simplifying, this matches the way we typically write
+   notations involving telescopes. *)
+Notation "'λ..' x .. y , e" :=
+  (tele_app (tele_bind (λ x, .. (tele_app (tele_bind (λ y, e))) .. )))
+  (at level 200, x binder, y binder, right associativity,
+   format "'[  ' 'λ..'  x  ..  y ']' ,  e").
+
+(* The testcase *)
+Lemma test {TA TB : tele} {X} (α' β' γ' : X → Prop) (Φ : TA → TB → Prop) x' :
+  (forall P Q, ((P /\ Q) = Q) * ((P -> Q) = Q)) ->
+  ∀ a b, Φ a b = (λ.. x y, β' x' ∧ (γ' x' → Φ x y)) a b.
+Proof.
+intros cheat a b.
+rewrite !tele_app_bind.
+by rewrite !cheat.
+Qed.
diff --git a/test-suite/ssr/set_polyuniv.v b/test-suite/ssr/set_polyuniv.v
new file mode 100644
index 0000000000..436eeafc79
--- /dev/null
+++ b/test-suite/ssr/set_polyuniv.v
@@ -0,0 +1,11 @@
+From Coq Require Import ssreflect.
+Set Default Proof Using "Type".
+
+Local Set Universe Polymorphism.
+
+Axiom foo : Type -> Prop.
+
+Lemma test : foo nat.
+Proof.
+set x := foo _. (* key @foo{i} matches @foo{j} *)
+Abort.