Fix #7421: constr_eq ignores universe constraints.

The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.

8 files changed, 92 insertions, 11 deletions

diff --git a/CHANGES b/CHANGES
index ce8e313b9..c36f59726 100644
--- a/CHANGES
+++ b/CHANGES
@@ -28,6 +28,12 @@ Tactics
 - The `simple apply` tactic now respects the `Opaque` flag when called from
   Ltac (`auto` still does not respect it).
 
+- Tactic `constr_eq` now adds universe constraints needed for the
+  identity to the context (it used to ignore them). New tactic
+  `constr_eq_strict` checks that the required constraints already hold
+  without adding new ones. Preexisting tactic `constr_eq_nounivs` can
+  still be used if you really want to ignore universe constraints.
+
 Tools
 
 - Coq_makefile lets one override or extend the following variables from
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 29c2f8b81..d0a0d568e 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3949,9 +3949,20 @@ succeeds, and results in an error otherwise.
    :name: constr_eq
 
    This tactic checks whether its arguments are equal modulo alpha
-   conversion and casts.
+   conversion, casts and universe constraints. It may unify universes.
 
 .. exn:: Not equal.
+.. exn:: Not equal (due to universes).
+
+.. tacn:: constr_eq_strict @term @term
+   :name: constr_eq_strict
+
+   This tactic checks whether its arguments are equal modulo alpha
+   conversion, casts and universe constraints. It does not add new
+   constraints.
+
+.. exn:: Not equal.
+.. exn:: Not equal (due to universes).
 
 .. tacn:: unify @term @term
    :name: unify
diff --git a/engine/evd.ml b/engine/evd.ml
index 0c9c3a29b..f56f9662d 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -894,6 +894,9 @@ let check_eq evd s s' =
 let check_leq evd s s' =
   UGraph.check_leq (UState.ugraph evd.universes) s s'
 
+let check_constraints evd csts =
+  UGraph.check_constraints csts (UState.ugraph evd.universes)
+
 let fix_undefined_variables evd =
   { evd with universes = UState.fix_undefined_variables evd.universes }
 
diff --git a/engine/evd.mli b/engine/evd.mli
index c40e925d8..405fcc403 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -552,6 +552,8 @@ val set_eq_instances : ?flex:bool ->
 val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
 val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
 
+val check_constraints : evar_map -> Univ.Constraint.t -> bool
+
 val evar_universe_context : evar_map -> UState.t
 val universe_context_set : evar_map -> Univ.ContextSet.t
 val universe_subst : evar_map -> UnivSubst.universe_opt_subst
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index f2899ab63..660e29ca8 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -793,17 +793,12 @@ END
 
 (* ********************************************************************* *)
 
-let eq_constr x y = 
-  Proofview.Goal.enter begin fun gl ->
-    let env = Tacmach.New.pf_env gl in
-    let evd = Tacmach.New.project gl in
-      match EConstr.eq_constr_universes env evd x y with
-      | Some _ -> Proofview.tclUNIT () 
-      | None -> Tacticals.New.tclFAIL 0 (str "Not equal")
-  end
-
 TACTIC EXTEND constr_eq
-| [ "constr_eq" constr(x) constr(y) ] -> [ eq_constr x y ]
+| [ "constr_eq" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:false x y ]
+END
+
+TACTIC EXTEND constr_eq_strict
+| [ "constr_eq_strict" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:true x y ]
 END
 
 TACTIC EXTEND constr_eq_nounivs
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 770e31fea..c430edf2e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5034,6 +5034,26 @@ let tclABSTRACT ?(opaque=true) name_op tac =
     else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
   abstract_subproof ~opaque s gk tac
 
+let constr_eq ~strict x y =
+  let fail = Tacticals.New.tclFAIL 0 (str "Not equal") in
+  let fail_universes = Tacticals.New.tclFAIL 0 (str "Not equal (due to universes)") in
+  Proofview.Goal.enter begin fun gl ->
+    let env = Tacmach.New.pf_env gl in
+    let evd = Tacmach.New.project gl in
+      match EConstr.eq_constr_universes env evd x y with
+      | Some csts ->
+        let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in
+        if strict then
+          if Evd.check_constraints evd csts then Proofview.tclUNIT ()
+          else fail_universes
+        else
+          (match Evd.add_constraints evd csts with
+           | evd -> Proofview.Unsafe.tclEVARS evd
+           | exception Univ.UniverseInconsistency _ ->
+             fail_universes)
+      | None -> fail
+  end
+
 let unify ?(state=full_transparent_state) x y =
   Proofview.Goal.enter begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 8d4302450..57f20d2ff 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -409,6 +409,11 @@ val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -
 
 (** {6 Other tactics. } *)
 
+(** Syntactic equality up to universes. With [strict] the universe
+   constraints must be already true to succeed, without [strict] they
+   are added to the evar map. *)
+val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic
+
 val unify           : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic
 
 val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
diff --git a/test-suite/bugs/closed/7421.v b/test-suite/bugs/closed/7421.v
new file mode 100644
index 000000000..afcdd35fc
--- /dev/null
+++ b/test-suite/bugs/closed/7421.v
@@ -0,0 +1,39 @@
+
+
+Universe i j.
+
+Goal False.
+Proof.
+  Check Type@{i} : Type@{j}.
+  Fail constr_eq_strict Type@{i} Type@{j}.
+  assert_succeeds constr_eq Type@{i} Type@{j}. (* <- i=j is forgotten after assert_succeeds *)
+  Fail constr_eq_strict Type@{i} Type@{j}.
+
+  constr_eq Type@{i} Type@{j}. (* <- i=j is retained *)
+  constr_eq_strict Type@{i} Type@{j}.
+  Fail Check Type@{i} : Type@{j}.
+
+  Fail constr_eq Prop Set.
+  Fail constr_eq Prop Type.
+
+  Fail constr_eq_strict Type Type.
+  constr_eq Type Type.
+
+  constr_eq_strict Set Set.
+  constr_eq Set Set.
+  constr_eq Prop Prop.
+
+  let x := constr:(Type) in constr_eq_strict x x.
+  let x := constr:(Type) in constr_eq x x.
+
+  Fail lazymatch type of prod with
+       | ?A -> ?B -> _ => constr_eq_strict A B
+       end.
+  lazymatch type of prod with
+  | ?A -> ?B -> _ => constr_eq A B
+  end.
+  lazymatch type of prod with
+  | ?A -> ?B -> ?C => constr_eq A C
+  end.
+
+Abort.