Stop using infer_conv_ustate in unification

pretyping/reductionops.ml

@@ -1266,6 +1266,30 @@ let is_conv ?(reds=TransparentState.full) env sigma x y =
 let is_conv_leq ?(reds=TransparentState.full) env sigma x y =
   is_fconv ~reds Conversion.CUMUL env sigma x y
 
+let is_conv_nounivs ?(reds=TransparentState.full) env sigma t1 t2 =
+  if EConstr.eq_constr_nounivs sigma t1 t2 then true
+  else
+    let evars = Evd.evar_handler sigma in
+    let t1 = EConstr.Unsafe.to_constr t1 in
+    let t2 = EConstr.Unsafe.to_constr t2 in
+    try
+      let env = Environ.set_universes (Evd.universes sigma) env in
+      let ignore_univs = let open Conversion in {
+        compare_sorts = (fun _ _ _ () -> Ok ());
+        compare_instances = (fun ~flex:_ _ _ () -> Ok ());
+        compare_cumul_instances = (fun _ _ _ _ () -> Ok ());
+      }
+      in
+      begin match Conversion.generic_conv ~l2r:false CONV ~evars reds env ((), ignore_univs) t1 t2 with
+      | Result.Ok () -> true
+      | Result.Error None -> false
+      | Result.Error (Some e) -> Empty.abort e
+      end
+    with
+    | e ->
+      let e = Exninfo.capture e in
+      report_anomaly e
+
 let sigma_compare_sorts pb s0 s1 sigma =
   match pb with
   | Conversion.CONV ->
@@ -1372,34 +1396,6 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Conversion.CUMUL)
 let infer_conv = infer_conv_gen { genconv = fun pb ~l2r sigma ->
       Conversion.generic_conv pb ~l2r ~evars:(Evd.evar_handler sigma) }
 
-let infer_conv_ustate ?(catch_incon=true) ?(pb=Conversion.CUMUL)
-    ?(ts=TransparentState.full) env sigma x y =
-  try
-      let ans = match pb with
-      | Conversion.CUMUL ->
-          EConstr.leq_constr_universes env sigma x y
-      | Conversion.CONV ->
-          EConstr.eq_constr_universes env sigma x y
-      in
-      match ans with
-      | Some cstr -> Some cstr
-      | None ->
-        let x = EConstr.Unsafe.to_constr x in
-        let y = EConstr.Unsafe.to_constr y in
-        let env = Environ.set_universes (Evd.universes sigma) env in
-        match
-          Conversion.generic_conv pb ~l2r:false ~evars:(Evd.evar_handler sigma) ts
-            env (UnivProblem.Set.empty, univproblem_univ_state) x y
-        with
-        | Result.Ok cstr -> Some cstr
-        | Result.Error None -> None
-        | Result.Error (Some e) -> Empty.abort e
-  with
-  | UGraph.UniverseInconsistency _ when catch_incon -> None
-  | e ->
-    let e = Exninfo.capture e in
-    report_anomaly e
-
 let evars_of_evar_map sigma =
   { Genlambda.evars_val = Evd.evar_handler sigma }
 

pretyping/reductionops.mli

@@ -255,6 +255,8 @@ val is_conv : ?reds:TransparentState.t -> env -> evar_map -> constr -> constr ->
 val is_conv_leq : ?reds:TransparentState.t -> env -> evar_map -> constr -> constr -> bool
 val is_fconv : ?reds:TransparentState.t -> conv_pb -> env -> evar_map -> constr -> constr -> bool
 
+val is_conv_nounivs : ?reds:TransparentState.t -> env -> evar_map -> constr -> constr -> bool
+
 (** [infer_conv] Adds necessary universe constraints to the evar map.
     pb defaults to CUMUL and ts to a full transparent state.
     @raise UniverseInconsistency iff catch_incon is set to false,
@@ -263,9 +265,6 @@ val is_fconv : ?reds:TransparentState.t -> conv_pb -> env -> evar_map -> constr
 val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TransparentState.t ->
   env -> evar_map -> constr -> constr -> evar_map option
 
-val infer_conv_ustate : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TransparentState.t ->
-  env -> evar_map -> constr -> constr -> UnivProblem.Set.t option
-
 (** Conversion with inference of universe constraints *)
 val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
   evar_map option

pretyping/unification.ml

@@ -1009,19 +1009,18 @@ let check_compatibility env pbty flags subst tyM tyN =
       | None -> error_cannot_unify env sigma (m,n)
     else sigma
 
-let check_compatibility_ustate env pbty flags subst tyM tyN =
+let check_compatibility_nounivs env flags subst tyM tyN =
   let sigma = subst.subst_sigma in
   match subst_defined_metas_evars sigma (subst.subst_metam, subst.subst_metas, []) tyM with
-  | None -> UnivProblem.Set.empty
+  | None -> ()
   | Some m ->
   match subst_defined_metas_evars sigma (subst.subst_metam, subst.subst_metas, []) tyN with
-  | None -> UnivProblem.Set.empty
+  | None -> ()
   | Some n ->
     if is_ground_term sigma m && is_ground_term sigma n then
-      match infer_conv_ustate ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n with
-      | Some uprob -> uprob
-      | None -> error_cannot_unify env sigma (m,n)
-    else UnivProblem.Set.empty
+      if is_conv_nounivs ~reds:flags.modulo_delta_types env sigma m n then ()
+      else error_cannot_unify env sigma (m,n)
+    else ()
 
 let rec is_neutral env sigma ts t =
   let (f, l) = decompose_app sigma t in
@@ -1473,22 +1472,18 @@ let rec unify_0_with_initial_metas (subst : subst0) conv_at_top env pb flags m n
         (* No subterm restriction there, too much incompatibilities
            don't care about universes from comparing the types
         *)
-         let _ : UnivProblem.Set.t =
-           if opt.with_types then
-             try (* Ensure we call conversion on terms of the same type *)
-               let tyM = get_type_of curenv ~lax:true sigma m1 in
-               let tyN = get_type_of curenv ~lax:true sigma n1 in
-               check_compatibility_ustate curenv CUMUL flags substn tyM tyN
-             with RetypeError _ ->
-               (* Renounce, maybe metas/evars prevents typing *) UnivProblem.Set.empty
-           else UnivProblem.Set.empty
-         in
-        match infer_conv_ustate ~pb ~ts:convflags curenv sigma m1 n1 with
-        | Some uprob ->
-          begin match Evd.add_constraints sigma uprob with
-          | sigma -> Some (push_sigma sigma substn)
-          | exception (UGraph.UniverseInconsistency _ | UniversesDiffer) -> None
-          end
+        let () =
+          if opt.with_types then
+            try (* Ensure we call conversion on terms of the same type *)
+              let tyM = get_type_of curenv ~lax:true sigma m1 in
+              let tyN = get_type_of curenv ~lax:true sigma n1 in
+              check_compatibility_nounivs curenv flags substn tyM tyN
+            with RetypeError _ ->
+              (* Renounce, maybe metas/evars prevents typing *) ()
+          else ()
+        in
+        match infer_conv ~pb ~ts:convflags curenv sigma m1 n1 with
+        | Some sigma -> Some (push_sigma sigma substn)
         | None ->
           if is_ground_term sigma m1 && is_ground_term sigma n1 then
             error_cannot_unify curenv sigma (cM,cN)

test-suite/bugs/bug_21674.v

@@ -0,0 +1,28 @@
+Polymorphic Axiom foo@{u} : nat -> Prop.
+
+Axiom bar : forall n, foo n.
+
+Goal foo 0.
+  Succeed simple apply bar.
+  apply bar.
+Qed.
+
+
+Require Import Corelib.Array.PrimArray.
+
+
+Axiom P : forall A t i (a:A), get t i = a.
+Axiom Q : forall A a i, @length@{length.u0} A a = i.
+
+Lemma test : forall A a i, @length@{P.u0} A a = i.
+Proof.
+  intros A a i.
+  Succeed refine (Q _ _ _).
+  Succeed simple eapply Q.
+  eapply Q.
+Qed.
+
+(* future work: make this succeed *)
+Fail Definition should_work@{u v|} : length@{u} [| | 0 |] = length@{v} [| | 0 |]
+  := eq_refl.
+(* Universe constraints are not implied by the ones declared: u = v *)