Merge PR #7798: Remove hack skipping comparison of algebraic universes in subtyping.

16 files changed, 94 insertions, 242 deletions

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index ca9581167..6b2af71f3 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -2,7 +2,6 @@ open Pp
 open Util
 open Names
 open Cic
-open Term
 open Reduction
 open Typeops
 open Indtypes
@@ -13,17 +12,6 @@ open Environ
 
 (** {6 Checking constants } *)
 
-let refresh_arity ar =
-  let ctxt, hd = decompose_prod_assum ar in
-  match hd with
-      Sort (Type u) when not (Univ.is_univ_variable u) ->
-      let ul = Univ.Level.make DirPath.empty 1 in
-      let u' = Univ.Universe.make ul in
-      let cst = Univ.enforce_leq u u' Univ.empty_constraint in
-      let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in
-        mkArity (ctxt,Prop Null), ctx
-    | _ -> ar, Univ.ContextSet.empty
-
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ prcon kn);
   (** Locally set the oracle for further typechecking *)
@@ -37,18 +25,13 @@ let check_constant_declaration env kn cb =
       let ctx = Univ.AUContext.repr auctx in
       push_context ~strict:false ctx env
   in
-  let envty, ty = 
-    let ty = cb.const_type in
-    let ty', cu = refresh_arity ty in
-    let envty = push_context_set cu env' in
-    let _ = infer_type envty ty' in
-    envty, ty
-  in
-  let () = 
+  let ty = cb.const_type in
+  let _ = infer_type env' ty in
+  let () =
     match body_of_constant cb with
     | Some bd ->
-      let j = infer envty bd in
-      conv_leq envty j ty
+      let j = infer env' bd in
+      conv_leq env' j ty
     | None -> ()
   in
   let env =
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index a22af4e0f..6d0d6f6c6 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 (*i*)
-open CErrors
 open Util
 open Names
 open Cic
@@ -132,40 +131,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     check (eq_constr) (fun x -> x.proj_type);
     true
   in
-  let check_inductive_type t1 t2 =
-
-    (* Due to template polymorphism, the conclusions of
-       t1 and t2, if in Type, are generated as the least upper bounds
-       of the types of the constructors.
-
-       By monotonicity of the infered l.u.b.  wrt subtyping (i.e.  if X:U
-       |- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each
-       universe in the conclusion of t1 has an bounding universe in
-       the conclusion of t2, so that we don't need to check the
-       subtyping of the conclusions of t1 and t2.
-
-       Even if we'd like to recheck it, the inference of constraints
-       is not designed to deal with algebraic constraints of the form
-       max-univ(u1..un) <= max-univ(u'1..u'n), so that it is not easy
-       to recheck it (in short, we would need the actual graph of
-       constraints as input while type checking is currently designed
-       to output a set of constraints instead) *)
-
-    (* So we cheat and replace the subtyping problem on algebraic
-       constraints of the form max-univ(u1..un) <= max-univ(u'1..u'n)
-       (that we know are necessary true) by trivial constraints that
-       the constraint generator knows how to deal with *)
-
-    let (ctx1,s1) = dest_arity env t1 in
-    let (ctx2,s2) = dest_arity env t2 in
-    let s1,s2 =
-      match s1, s2 with
-      | Type _, Type _ -> (* shortcut here *) Prop Null, Prop Null
-      | (Prop _, Type _) | (Type _,Prop _) -> error ()
-      | _ -> (s1, s2) in
-    check_conv conv_leq env
-      (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
-  in
+  let check_inductive_type t1 t2 = check_conv conv_leq env t1 t2 in
 
   let check_packet p1 p2 =
     let check eq f = if not (eq (f p1) (f p2)) then error () in
@@ -254,52 +220,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
 let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
   let error () = error_not_match l spec2 in
   let check_conv f = check_conv_error error f in
-  let check_type env t1 t2 =
-
-    (* If the type of a constant is generated, it may mention
-       non-variable algebraic universes that the general conversion
-       algorithm is not ready to handle. Anyway, generated types of
-       constants are functions of the body of the constant. If the
-       bodies are the same in environments that are subtypes one of
-       the other, the types are subtypes too (i.e. if Gamma <= Gamma',
-       Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T').
-       Hence they don't have to be checked again *)
-
-    let t1,t2 =
-      if isArity t2 then
-        let (ctx2,s2) = destArity t2 in
-        match s2 with
-        | Type v when not (Univ.is_univ_variable v) ->
-          (* The type in the interface is inferred and is made of algebraic
-             universes *)
-          begin try
-            let (ctx1,s1) = dest_arity env t1 in
-            match s1 with
-            | Type u when not (Univ.is_univ_variable u) ->
-              (* Both types are inferred, no need to recheck them. We
-                 cheat and collapse the types to Prop *)
-                mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
-            | Prop _ ->
-              (* The type in the interface is inferred, it may be the case
-                 that the type in the implementation is smaller because
-                 the body is more reduced. We safely collapse the upper
-                 type to Prop *)
-                mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
-            | Type _ ->
-              (* The type in the interface is inferred and the type in the
-                 implementation is not inferred or is inferred but from a
-                 more reduced body so that it is just a variable. Since
-                 constraints of the form "univ <= max(...)" are not
-                 expressible in the system of algebraic universes: we fail
-                 (the user has to use an explicit type in the interface *)
-                error ()
-          with UserError _ (* "not an arity" *) ->
-            error () end
-        | _ -> t1,t2
-      else
-        (t1,t2) in
-    check_conv conv_leq env t1 t2
-  in
+  let check_type env t1 t2 = check_conv conv_leq env t1 t2 in
     match info1 with
       | Constant cb1 ->
 	let cb1 = subst_const_body subst1 cb1 in
diff --git a/checker/univ.ml b/checker/univ.ml
index 15673736f..e50e883ad 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -190,13 +190,6 @@ struct
       (let (u,n) = x and (v,n') = y in
 	 Int.equal n n' && Level.equal u v)
 
-    let leq (u,n) (v,n') =
-      let cmp = Level.compare u v in
-	if Int.equal cmp 0 then n <= n'
-	else if n <= n' then 
-	  (Level.is_prop u && Level.is_small v)
-	else false
-
     let successor (u,n) =
       if Level.is_prop u then type1
       else (u, n + 1)
@@ -833,41 +826,6 @@ type 'a constrained = 'a * constraints
 
 type 'a constraint_function = 'a -> 'a -> constraints -> constraints
 
-let constraint_add_leq v u c =
-  (* We just discard trivial constraints like u<=u *)
-  if Expr.equal v u then c
-  else 
-    match v, u with
-    | (x,n), (y,m) -> 
-    let j = m - n in
-      if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then
-	Constraint.add (x,Lt,y) c
-      else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
-	if Level.equal x y then (* u+(k+1) <= u *)
-	  raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u))
-	else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.")
-      else if j = 0 then
-	Constraint.add (x,Le,y) c
-      else (* j >= 1 *) (* m = n + k, u <= v+k *)
-	if Level.equal x y then c (* u <= u+k, trivial *)
-	else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
-	else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.")
-	  
-let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
-
-let check_univ_leq u v = 
-  Universe.for_all (fun u -> check_univ_leq_one u v) u
-
-let enforce_leq u v c =
-  match v with
-  | [v] ->
-    List.fold_right (fun u -> constraint_add_leq u v) u c
-  | _ -> anomaly (Pp.str"A universe bound can only be a variable.")
-
-let enforce_leq u v c =
-  if check_univ_leq u v then c
-  else enforce_leq u v c
-
 let check_constraint g (l,d,r) =
   match d with
   | Eq -> check_equal g l r
diff --git a/checker/univ.mli b/checker/univ.mli
index 6cd3b3638..3b29b158f 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -109,8 +109,6 @@ type 'a constrained = 'a * constraints
 
 type 'a constraint_function = 'a -> 'a -> constraints -> constraints
 
-val enforce_leq : universe constraint_function
-
 (** {6 ... } *)
 (** Merge of constraints in a universes graph.
   The function [merge_constraints] merges a set of constraints in a given
diff --git a/clib/cList.ml b/clib/cList.ml
index 2b627f745..de42886dc 100644
--- a/clib/cList.ml
+++ b/clib/cList.ml
@@ -122,6 +122,7 @@ sig
   val duplicates : 'a eq -> 'a list -> 'a list
   val uniquize : 'a list -> 'a list
   val sort_uniquize : 'a cmp -> 'a list -> 'a list
+  val min : 'a cmp -> 'a list -> 'a
   val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
   val combinations : 'a list list -> 'a list list
@@ -971,6 +972,15 @@ let rec uniquize_sorted cmp = function
 let sort_uniquize cmp l =
   uniquize_sorted cmp (List.sort cmp l)
 
+let min cmp l =
+  let rec aux cur = function
+    | [] -> cur
+    | x :: l -> if cmp x cur < 0 then aux x l else aux cur l
+  in
+  match l with
+  | x :: l -> aux x l
+  | [] -> raise Not_found
+
 let rec duplicates cmp = function
   | [] -> []
   | x :: l ->
diff --git a/clib/cList.mli b/clib/cList.mli
index 13e069e94..42fae5ed3 100644
--- a/clib/cList.mli
+++ b/clib/cList.mli
@@ -376,6 +376,11 @@ sig
   (** Return a sorted version of a list without duplicates
       according to some comparison function. *)
 
+  val min : 'a cmp -> 'a list -> 'a
+  (** Return minimum element according to some comparison function.
+
+      @raise Not_found on an empty list. *)
+
   (** {6 Cartesian product} *)
 
   val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 418229330..e68f906ec 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -828,8 +828,10 @@ let leq_constr_univs_infer univs m n =
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
 	if UGraph.check_leq univs u1 u2 then true
 	else
-	  (cstrs := Univ.enforce_leq u1 u2 !cstrs; 
-	   true)
+          (try let c, _ = UGraph.enforce_leq_alg u1 u2 univs in
+            cstrs := Univ.Constraint.union c !cstrs;
+            true
+          with Univ.UniverseInconsistency _ -> false)
     in
     let rec eq_constr' nargs m n =
       m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 22f523a9a..02bab581a 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -47,7 +47,6 @@ type signature_mismatch_error =
   | RecordFieldExpected of bool
   | RecordProjectionsExpected of Name.t list
   | NotEqualInductiveAliases
-  | NoTypeConstraintExpected
   | IncompatibleInstances
   | IncompatibleUniverses of Univ.univ_inconsistency
   | IncompatiblePolymorphism of env * types * types
diff --git a/kernel/modops.mli b/kernel/modops.mli
index ac76d28cf..8e7e618fc 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -106,7 +106,6 @@ type signature_mismatch_error =
   | RecordFieldExpected of bool
   | RecordProjectionsExpected of Name.t list
   | NotEqualInductiveAliases
-  | NoTypeConstraintExpected
   | IncompatibleInstances
   | IncompatibleUniverses of Univ.univ_inconsistency
   | IncompatiblePolymorphism of env * types * types
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index f4af31386..2c61b7a01 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -693,8 +693,8 @@ let infer_eq (univs, cstrs as cuniv) u u' =
 let infer_leq (univs, cstrs as cuniv) u u' =
   if UGraph.check_leq univs u u' then cuniv
   else
-    let cstrs' = Univ.enforce_leq u u' cstrs in
-      univs, cstrs'
+    let cstrs', _ = UGraph.enforce_leq_alg u u' univs in
+      univs, Univ.Constraint.union cstrs cstrs'
 
 let infer_cmp_universes env pb s0 s1 univs =
   let open Sorts in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 13701d489..1e58f5c24 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -17,7 +17,6 @@
 open Names
 open Univ
 open Util
-open Term
 open Constr
 open Declarations
 open Declareops
@@ -138,39 +137,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   in
   let mib2 =  Declareops.subst_mind_body subst2 mib2 in
   let check_inductive_type cst name t1 t2 =
-
-    (* Due to template polymorphism, the conclusions of
-       t1 and t2, if in Type, are generated as the least upper bounds
-       of the types of the constructors.
-
-       By monotonicity of the infered l.u.b.  wrt subtyping (i.e.  if X:U
-       |- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each
-       universe in the conclusion of t1 has an bounding universe in
-       the conclusion of t2, so that we don't need to check the
-       subtyping of the conclusions of t1 and t2.
-
-       Even if we'd like to recheck it, the inference of constraints
-       is not designed to deal with algebraic constraints of the form
-       max-univ(u1..un) <= max-univ(u'1..u'n), so that it is not easy
-       to recheck it (in short, we would need the actual graph of
-       constraints as input while type checking is currently designed
-       to output a set of constraints instead) *)
-
-    (* So we cheat and replace the subtyping problem on algebraic
-       constraints of the form max-univ(u1..un) <= max-univ(u'1..u'n)
-       (that we know are necessary true) by trivial constraints that
-       the constraint generator knows how to deal with *)
-
-    let (ctx1,s1) = dest_arity env t1 in
-    let (ctx2,s2) = dest_arity env t2 in
-    let s1,s2 =
-      match s1, s2 with
-      | Type _, Type _ -> (* shortcut here *) Sorts.prop, Sorts.prop
-      | (Prop _, Type _) | (Type _,Prop _) ->
-	error (NotConvertibleInductiveField name)
-      | _ -> (s1, s2) in
     check_conv (NotConvertibleInductiveField name)
-      cst (inductive_is_polymorphic mib1) infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
+      cst (inductive_is_polymorphic mib1) infer_conv_leq env t1 t2
   in
 
   let check_packet cst p1 p2 =
@@ -260,53 +228,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
   let error why = error_signature_mismatch l spec2 why in
   let check_conv cst poly f = check_conv_error error cst poly f in
   let check_type poly cst env t1 t2 =
-
     let err = NotConvertibleTypeField (env, t1, t2) in
-
-    (* If the type of a constant is generated, it may mention
-       non-variable algebraic universes that the general conversion
-       algorithm is not ready to handle. Anyway, generated types of
-       constants are functions of the body of the constant. If the
-       bodies are the same in environments that are subtypes one of
-       the other, the types are subtypes too (i.e. if Gamma <= Gamma',
-       Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T').
-       Hence they don't have to be checked again *)
-
-    let t1,t2 =
-      if isArity t2 then
-        let (ctx2,s2) = destArity t2 in
-        match s2 with
-        | Type v when not (is_univ_variable v) ->
-          (* The type in the interface is inferred and is made of algebraic
-             universes *)
-          begin try
-            let (ctx1,s1) = dest_arity env t1 in
-            match s1 with
-            | Type u when not (is_univ_variable u) ->
-              (* Both types are inferred, no need to recheck them. We
-                 cheat and collapse the types to Prop *)
-                mkArity (ctx1,Sorts.prop), mkArity (ctx2,Sorts.prop)
-            | Prop _ ->
-              (* The type in the interface is inferred, it may be the case
-                 that the type in the implementation is smaller because
-                 the body is more reduced. We safely collapse the upper
-                 type to Prop *)
-                mkArity (ctx1,Sorts.prop), mkArity (ctx2,Sorts.prop)
-            | Type _ ->
-              (* The type in the interface is inferred and the type in the
-                 implementation is not inferred or is inferred but from a
-                 more reduced body so that it is just a variable. Since
-                 constraints of the form "univ <= max(...)" are not
-                 expressible in the system of algebraic universes: we fail
-                 (the user has to use an explicit type in the interface *)
-                error NoTypeConstraintExpected
-          with NotArity ->
-            error err end
-        | _ ->
-	  t1,t2
-      else
-        (t1,t2) in
-      check_conv err cst poly infer_conv_leq env t1 t2
+    check_conv err cst poly infer_conv_leq env t1 t2
   in
   match info1 with
     | Constant cb1 ->
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 4a9467de5..bc624ba56 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -747,6 +747,45 @@ let check_constraint g (l,d,r) =
 let check_constraints c g =
   Constraint.for_all (check_constraint g) c
 
+let leq_expr (u,m) (v,n) =
+  let d = match m - n with
+    | 1 -> Lt
+    | diff -> assert (diff <= 0); Le
+  in
+  (u,d,v)
+
+let enforce_leq_alg u v g =
+  let enforce_one (u,v) = function
+    | Inr _ as orig -> orig
+    | Inl (cstrs,g) as orig ->
+      if check_smaller_expr g u v then orig
+      else
+        (let c = leq_expr u v in
+         match enforce_constraint c g with
+         | g -> Inl (Constraint.add c cstrs,g)
+         | exception (UniverseInconsistency _ as e) -> Inr e)
+  in
+  (* max(us) <= max(vs) <-> forall u in us, exists v in vs, u <= v *)
+  let c = Universe.map (fun u -> Universe.map (fun v -> (u,v)) v) u in
+  let c = List.cartesians enforce_one (Inl (Constraint.empty,g)) c in
+  (* We pick a best constraint: smallest number of constraints, not an error if possible. *)
+  let order x y = match x, y with
+    | Inr _, Inr _ -> 0
+    | Inl _, Inr _ -> -1
+    | Inr _, Inl _ -> 1
+    | Inl (c,_), Inl (c',_) ->
+      Int.compare (Constraint.cardinal c) (Constraint.cardinal c')
+  in
+  match List.min order c with
+  | Inl x -> x
+  | Inr e -> raise e
+
+(* sanity check wrapper *)
+let enforce_leq_alg u v g =
+  let _,g as cg = enforce_leq_alg u v g in
+  assert (check_leq g u v);
+  cg
+
 (* Normalization *)
 
 (** [normalize_universes g] returns a graph where all edges point
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index e6dd629e4..8c2d877b0 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -42,6 +42,9 @@ val merge_constraints : Constraint.t -> t -> t
 val check_constraint  : t -> univ_constraint -> bool
 val check_constraints : Constraint.t -> t -> bool
 
+(** Picks an arbitrary set of constraints sufficient to ensure [u <= v]. *)
+val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t
+
 (** Adds a universe to the graph, ensuring it is >= or > Set.
    @raise AlreadyDeclared if the level is already declared in the graph. *)
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 9782312ca..311477dac 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -666,7 +666,7 @@ let constraint_add_leq v u c =
       else (* j >= 1 *) (* m = n + k, u <= v+k *)
 	if Level.equal x y then c (* u <= u+k, trivial *)
 	else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
-	else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.")
+        else Constraint.add (x,Le,y) c (* u <= v implies u <= v+k *)
 	  
 let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
 
@@ -674,12 +674,7 @@ let check_univ_leq u v =
   Universe.for_all (fun u -> check_univ_leq_one u v) u
 
 let enforce_leq u v c =
-  let rec aux acc v =
-  match v with
-  | v :: l ->
-    aux (List.fold_right (fun u -> constraint_add_leq u v) u c) l
-  | [] -> acc
-  in aux c v
+  List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v
 
 let enforce_leq u v c =
   if check_univ_leq u v then c
diff --git a/test-suite/bugs/closed/7695.v b/test-suite/bugs/closed/7695.v
new file mode 100644
index 000000000..42bdb076b
--- /dev/null
+++ b/test-suite/bugs/closed/7695.v
@@ -0,0 +1,20 @@
+Require Import Hurkens.
+
+Universes i j k.
+Module Type T.
+  Parameter T1 : Type@{i+1}.
+  Parameter e : Type@{j} = T1 : Type@{k}.
+End T.
+
+Module M.
+  Definition T1 := Type@{j}.
+  Definition e : Type@{j} = T1 : Type@{k} := eq_refl.
+End M.
+
+Module F (A:T).
+  Definition bad := TypeNeqSmallType.paradox _ A.e.
+End F.
+
+Set Printing Universes.
+Fail Module X := F M.
+(* Universe inconsistency. Cannot enforce j <= i because i < Coq.Logic.Hurkens.105 = j. *)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 5d671ef52..534e58f9c 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -871,9 +871,6 @@ let explain_not_match_error = function
     pr_enum (function Name id -> Id.print id | _ -> str "_") nal
   | NotEqualInductiveAliases ->
     str "Aliases to inductive types do not match"
-  | NoTypeConstraintExpected ->
-    strbrk "a definition whose type is constrained can only be subtype " ++
-    strbrk "of a definition whose type is itself constrained"
   | CumulativeStatusExpected b ->
     let status b = if b then str"cumulative" else str"non-cumulative" in
       str "a " ++ status b ++ str" declaration was expected, but a " ++