Put type-in-type flag in ugraph.

Fix #13086.

9 files changed, 79 insertions, 32 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index 8d1584cd95..2cb88c7fff 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -286,6 +286,10 @@ let process_universe_constraints ctx cstrs =
             if not (drop_weak_constraints ()) then weak := UPairSet.add (l,r) !weak; local
           | UEq (l, r) -> equalize_universes l r local
   in
+  let unify_universes cst local =
+    if not (UGraph.type_in_type univs) then unify_universes cst local
+    else try unify_universes cst local with UniverseInconsistency _ -> local
+  in
   let local =
     UnivProblem.Set.fold unify_universes cstrs Constraint.empty
   in
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 1c7e716fc2..c5854e27f3 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -306,8 +306,9 @@ let normalize_context_set ~lbound g ctx us algs weak =
   let csts, partition =
     (* We first put constraints in a normal-form: all self-loops are collapsed
        to equalities. *)
+    let g = UGraph.initial_universes_with g in
     let g = LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g)
-                           ctx UGraph.initial_universes
+                           ctx g
     in
     let add_soft u g =
       if not (Level.is_small u || LSet.mem u ctx)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 03c9cb4be6..e497b7904a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -467,14 +467,22 @@ let same_flags {
 [@warning "+9"]
 
 let set_cumulative_sprop b = map_universes (UGraph.set_cumulative_sprop b)
+let set_type_in_type b = map_universes (UGraph.set_type_in_type b)
 
 let set_typing_flags c env =
   if same_flags env.env_typing_flags c then env
-  else set_cumulative_sprop c.cumulative_sprop { env with env_typing_flags = c }
+  else
+    let env = { env with env_typing_flags = c } in
+    let env = set_cumulative_sprop c.cumulative_sprop env in
+    let env = set_type_in_type (not c.check_universes) env in
+    env
 
 let set_cumulative_sprop b env =
   set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env
 
+let set_type_in_type b env =
+  set_typing_flags {env.env_typing_flags with check_universes=not b} env
+
 let set_allow_sprop b env =
   { env with env_stratification =
     { env.env_stratification with env_sprop_allowed = b } }
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 974e794c6b..47a118aa42 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -320,6 +320,7 @@ val push_subgraph : Univ.ContextSet.t -> env -> env
 val set_engagement : engagement -> env -> env
 val set_typing_flags : typing_flags -> env -> env
 val set_cumulative_sprop : bool -> env -> env
+val set_type_in_type : bool -> env -> env
 val set_allow_sprop : bool -> env -> env
 val sprop_allowed : env -> bool
 
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 179353d3f0..b2520b780f 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -77,7 +77,7 @@ let check_univ_leq ?(is_real_arg=false) env u info =
     else info
   in
   (* Inductive types provide explicit lifting from SProp to other universes, so allow SProp <= any. *)
-  if type_in_type env || Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ
+  if Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ
   then { info with ind_min_univ = Option.map (Universe.sup u) info.ind_min_univ }
   else if is_impredicative_univ env ind_univ
        && Option.is_empty info.ind_min_univ then { info with ind_squashed = true }
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 52e93a9e22..096e458ec4 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -29,7 +29,12 @@ module G = AcyclicGraph.Make(struct
    code (eg add_universe with a constraint vs G.add with no
    constraint) *)
 
-type t = { graph: G.t; sprop_cumulative : bool }
+type t = {
+  graph: G.t;
+  sprop_cumulative : bool;
+  type_in_type : bool;
+}
+
 type 'a check_function = t -> 'a -> 'a -> bool
 
 let g_map f g =
@@ -39,6 +44,10 @@ let g_map f g =
 
 let set_cumulative_sprop b g = {g with sprop_cumulative=b}
 
+let set_type_in_type b g = {g with type_in_type=b}
+
+let type_in_type g = g.type_in_type
+
 let check_smaller_expr g (u,n) (v,m) =
   let diff = n - m in
     match diff with
@@ -55,28 +64,33 @@ let real_check_leq g u v =
   Universe.for_all (fun ul -> exists_bigger g ul v) u
 
 let check_leq g u v =
+  type_in_type g ||
   Universe.equal u v || (g.sprop_cumulative && Universe.is_sprop u) ||
   (not (Universe.is_sprop u) && not (Universe.is_sprop v) &&
     (is_type0m_univ u ||
      real_check_leq g u v))
 
 let check_eq g u v =
+  type_in_type g ||
   Universe.equal u v ||
   (not (Universe.is_sprop u || Universe.is_sprop v) &&
    (real_check_leq g u v && real_check_leq g v u))
 
 let check_eq_level g u v =
   u == v ||
+  type_in_type g ||
   (not (Level.is_sprop u || Level.is_sprop v) && G.check_eq g.graph u v)
 
-let empty_universes = {graph=G.empty; sprop_cumulative=false}
+let empty_universes = {graph=G.empty; sprop_cumulative=false; type_in_type=false}
 
 let initial_universes =
   let big_rank = 1000000 in
   let g = G.empty in
   let g = G.add ~rank:big_rank Level.prop g in
   let g = G.add ~rank:big_rank Level.set g in
-  {graph=G.enforce_lt Level.prop Level.set g; sprop_cumulative=false}
+  {empty_universes with graph=G.enforce_lt Level.prop Level.set g}
+
+let initial_universes_with g = {g with graph=initial_universes.graph}
 
 let enforce_constraint (u,d,v) g =
   match d with
@@ -91,6 +105,10 @@ let enforce_constraint (u,d,v as cst) g =
   | true, Le, false when g.sprop_cumulative -> g
   | _ ->  raise (UniverseInconsistency (d,Universe.make u, Universe.make v, None))
 
+let enforce_constraint cst g =
+  if not (type_in_type g) then enforce_constraint cst g
+  else try enforce_constraint cst g with UniverseInconsistency _ -> g
+
 let merge_constraints csts g = Constraint.fold enforce_constraint csts g
 
 let check_constraint g (u,d,v) =
@@ -103,8 +121,8 @@ let check_constraint g (u,d,v as cst) =
   match Level.is_sprop u, d, Level.is_sprop v with
   | false, _, false -> check_constraint g.graph cst
   | true, (Eq|Le), true -> true
-  | true, Le, false -> g.sprop_cumulative
-  | _ -> false
+  | true, Le, false -> g.sprop_cumulative || type_in_type g
+  | _ -> type_in_type g
 
 let check_constraints csts g = Constraint.for_all (check_constraint g) csts
 
@@ -145,8 +163,10 @@ let enforce_leq_alg u v g =
 let enforce_leq_alg u v g =
   match Universe.is_sprop u, Universe.is_sprop v with
   | true, true -> Constraint.empty, g
-  | true, false | false, true -> raise (UniverseInconsistency (Le, u, v, None))
   | false, false -> enforce_leq_alg u v g
+  | left, _ ->
+    if left && g.sprop_cumulative then Constraint.empty, g
+    else raise (UniverseInconsistency (Le, u, v, None))
 
 (* sanity check wrapper *)
 let enforce_leq_alg u v g =
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index c9fbd7f694..87b3634e28 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -16,6 +16,15 @@ type t
 val set_cumulative_sprop : bool -> t -> t
 (** Makes the system incomplete. *)
 
+val set_type_in_type : bool -> t -> t
+
+(** When [type_in_type], functions adding constraints do not fail and
+   may instead ignore inconsistent constraints.
+
+    Checking functions such as [check_leq] always return [true].
+*)
+val type_in_type : t -> bool
+
 type 'a check_function = t -> 'a -> 'a -> bool
 
 val check_leq : Universe.t check_function
@@ -25,6 +34,9 @@ val check_eq_level : Level.t check_function
 (** The initial graph of universes: Prop < Set *)
 val initial_universes : t
 
+(** Initial universes, but keeping options such as type in type from the argument. *)
+val initial_universes_with : t -> t
+
 (** Check equality of instances w.r.t. a universe graph *)
 val check_eq_instances : Instance.t check_function
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 6d8aa02dff..d2fb04bc38 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -205,12 +205,6 @@ module Level = struct
 
   let pr u = str (to_string u)
 
-  let apart u v =
-    match data u, data v with
-    | SProp, _ | _, SProp
-    | Prop, Set | Set, Prop -> true
-    | _ -> false
-
   let vars = Array.init 20 (fun i -> make (Var i))
 
   let var n =
@@ -568,16 +562,6 @@ let constraint_type_ord c1 c2 = match c1, c2 with
 | Eq, Eq -> 0
 | Eq, _ -> 1
 
-(* Universe inconsistency: error raised when trying to enforce a relation
-   that would create a cycle in the graph of universes. *)
-
-type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option
-
-exception UniverseInconsistency of univ_inconsistency
-
-let error_inconsistency o u v p =
-  raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p))
-
 (* Constraints and sets of constraints. *)
 
 type univ_constraint = Level.t * constraint_type * Level.t
@@ -660,8 +644,6 @@ type 'a constraint_function = 'a -> 'a -> constraints -> constraints
 let enforce_eq_level u v c =
   (* We discard trivial constraints like u=u *)
   if Level.equal u v then c
-  else if Level.apart u v then
-    error_inconsistency Eq u v None
   else Constraint.add (u,Eq,v) c
 
 let enforce_eq u v c =
@@ -684,9 +666,9 @@ let constraint_add_leq v u c =
     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, None))
+      else if j <= -1 (* n = m+k, v+k <= u and k>0 *) then
+        if Level.equal x y then (* u+k <= u with k>0 *)
+          Constraint.add (x,Lt,x) c
         else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.")
       else if j = 0 then
         Constraint.add (x,Le,y) c
@@ -703,8 +685,8 @@ let check_univ_leq u v =
 let enforce_leq u v c =
   match Universe.is_sprop u, Universe.is_sprop v with
   | true, true -> c
-  | true, false | false, true ->
-    raise (UniverseInconsistency (Le, u, v, None))
+  | true, false -> Constraint.add (Level.sprop,Le,Level.prop) c
+  | false, true -> Constraint.add (Level.prop,Le,Level.sprop) c
   | false, false ->
     List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v
 
@@ -1232,6 +1214,14 @@ let hcons_universe_context_set (v, c) =
 
 let hcons_univ x = Universe.hcons x
 
+(* Universe inconsistency: error raised when trying to enforce a relation
+   that would create a cycle in the graph of universes. *)
+
+type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option
+
+(* Do not use in this file as we may be type-in-type *)
+exception UniverseInconsistency of univ_inconsistency
+
 let explain_universe_inconsistency prl (o,u,v,p : univ_inconsistency) =
   let pr_uni = Universe.pr_with prl in
   let pr_rel = function
diff --git a/test-suite/bugs/closed/bug_13086.v b/test-suite/bugs/closed/bug_13086.v
new file mode 100644
index 0000000000..75f842b1cf
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13086.v
@@ -0,0 +1,11 @@
+Unset Universe Checking.
+
+Definition bad1@{|Set < Set} := Prop.
+
+Set Universe Polymorphism.
+Axiom ax : Type.
+Inductive I@{u} : Prop := foo : ax@{u} -> I.
+
+Definition bad2@{v} (x:I@{v}) : I@{Set} := x.
+
+Definition vsdvds (f : (Prop -> Prop) -> Prop) (x : Set -> Prop) := f x.