Fix bug #4254 with the help of J.H. Jourdan

1) We now _assign_ the smallest possible arities to mutual inductive types
and eventually add leq constraints on the user given arities. Remove
useless limitation on instantiating algebraic universe variables with
their least upper bound if they have upper constraints as well.

2) Do not remove non-recursive variables when computing minimal levels of inductives.

3) Avoid modifying user-given arities if not necessary to compute the
minimal level of an inductive.

4) We correctly solve the recursive equations taking into account the
user-declared level.

6 files changed, 84 insertions, 56 deletions

diff --git a/library/universes.ml b/library/universes.ml
index 16e6ebb029..a3926bc6f2 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -757,7 +757,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	if alg then
 	  (* u is algebraic: we instantiate it with it's lower bound, if any, 
               or enforce the constraints if it is bounded from the top. *)
-	  instantiate_with_lbound u lbound true (not (Option.is_empty right)) acc
+	  instantiate_with_lbound u lbound true false acc
 	else (* u is non algebraic *)
 	  match Universe.level lbound with
 	  | Some l -> (* The lowerbound is directly a level *) 
@@ -767,7 +767,8 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	     if not (Level.equal l u) then
 	       (* Should check that u does not 
   	          have upper constraints that are not already in right *)
-	       instantiate_with_lbound u lbound false (LSet.mem l algs) acc
+	       let acc' = (ctx', us, LSet.remove l algs, insts, cstrs) in
+		 instantiate_with_lbound u lbound false false acc
 	     else acc, (true, false, lbound)
 	| None -> 
 	  try 
@@ -1017,13 +1018,14 @@ let solve_constraints_system levels level_bounds level_min =
   for i=0 to nind-1 do
     for j=0 to nind-1 do
       if not (Int.equal i j) && Int.Set.mem j clos.(i) then
-	(v.(i) <- Universe.sup v.(i) level_bounds.(j);
-	 level_min.(i) <- Universe.sup level_min.(i) level_min.(j))
+	(v.(i) <- Universe.sup v.(i) level_bounds.(j));
+	 (* level_min.(i) <- Universe.sup level_min.(i) level_min.(j)) *)
     done;
-    for j=0 to nind-1 do
-      match levels.(j) with
-      | Some u -> v.(i) <- univ_level_rem u v.(i) level_min.(i)
-      | None -> ()
-    done
+    (* for j=0 to nind-1 do *)
+    (*   match levels.(j) with *)
+    (*   | Some u when not (Univ.Level.is_small u) -> *)
+    (* 	 v.(i) <- univ_level_rem u v.(i) level_min.(i) *)
+    (*   | _ -> () *)
+    (* done *)
   done;
   v
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 60b1da7049..168a10df93 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -351,10 +351,7 @@ let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local
 let evar_universe_context_subst ctx = ctx.uctx_univ_variables
 
 let instantiate_variable l b v =
-  (* let b = Univ.subst_large_constraint (Univ.Universe.make l) Univ.type0m_univ b in *)
-  (* if Univ.univ_depends (Univ.Universe.make l) b then  *)
-  (*   error ("Occur-check in universe variable instantiation") *)
-  (* else *) v := Univ.LMap.add l (Some b) !v
+  v := Univ.LMap.add l (Some b) !v
 
 exception UniversesDiffer
 
@@ -420,7 +417,16 @@ let process_universe_constraints univs vars alg cstrs =
 		      raise UniversesDiffer
 	      in
 	        Univ.enforce_eq_level l' r' local
-           | _, _ (* One of the two is algebraic or global *) -> 
+	    | Inr (l, loc, alg), Inl r
+	    | Inl r, Inr (l, loc, alg) ->
+	       let inst = Univ.univ_level_rem l r r in
+		 if alg then (instantiate_variable l inst vars; local)
+		 else
+		   let lu = Univ.Universe.make l in
+		   if Univ.univ_level_mem l r then
+		     Univ.enforce_leq inst lu local
+		   else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
+            | _, _ (* One of the two is algebraic or global *) -> 
 	     if Univ.check_eq univs l r then local
 	     else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
   in
diff --git a/test-suite/bugs/closed/3446.v b/test-suite/bugs/closed/3446.v
index 4f29b76c6e..dce73e1a50 100644
--- a/test-suite/bugs/closed/3446.v
+++ b/test-suite/bugs/closed/3446.v
@@ -1,28 +1,32 @@
 (* File reduced by coq-bug-finder from original input, then from 7372 lines to 539 lines, then from 531 lines to 107 lines, then from 76 lines to 46 lines *)
-(* Set Asymmetric Patterns. *)
-(* Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). *)
-(* Notation "A -> B" := (forall (_ : A), B). *)
+Module First.
+Set Asymmetric Patterns.
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Notation "A -> B" := (forall (_ : A), B).
+Set Universe Polymorphism.
+
 
-(* Notation "x → y" := (x -> y) *)
-(*   (at level 99, y at level 200, right associativity): type_scope. *)
-(* Record sigT A (P : A -> Type) := *)
-(*   { projT1 : A ; projT2 : P projT1 }. *)
-(* Arguments projT1 {A P} s. *)
-(* Arguments projT2 {A P} s. *)
-(* Set Universe Polymorphism. *)
-(* Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). *)
-(* Reserved Notation "x = y" (at level 70, no associativity). *)
-(* Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y). *)
-(* Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. *)
-(* Reserved Notation "{ x : A  & P }" (at level 0, x at level 99). *)
-(* Notation "{ x : A  & P }" := (sigT A (fun x => P)) : type_scope. *)
+Notation "x → y" := (x -> y)
+  (at level 99, y at level 200, right associativity): type_scope.
+Record sigT A (P : A -> Type) :=
+  { projT1 : A ; projT2 : P projT1 }.
+Arguments projT1 {A P} s.
+Arguments projT2 {A P} s.
+Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
+Reserved Notation "x = y" (at level 70, no associativity).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y).
+Notation " x = y " := (paths x y) : type_scope.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end.
+Reserved Notation "{ x : A  & P }" (at level 0, x at level 99).
+Notation "{ x : A  & P }" := (sigT A (fun x => P)) : type_scope.
 
 
-(* Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v &  transport _ p (projT2 u) = projT2 v}), u = v. *)
-(* Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}). *)
+Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v &  transport _ p (projT2 u) = projT2 v}), u = v.
+Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}).
 
-(* Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) := *)
-(*   @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _). *)
+Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) :=
+  @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _).
+End First.
 
 Set Asymmetric Patterns.
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v
index 9320848910..0ccc92067d 100644
--- a/test-suite/bugs/closed/3922.v
+++ b/test-suite/bugs/closed/3922.v
@@ -43,7 +43,7 @@ Notation IsHProp := (IsTrunc -1).
 Monomorphic Axiom dummy_funext_type : Type0.
 Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }.
 
-Inductive Unit : Type1 :=
+Inductive Unit : Set :=
     tt : Unit.
 
 Record TruncType (n : trunc_index) := BuildTruncType {
diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v
index 1449f242b4..c6cb9c35e6 100644
--- a/test-suite/bugs/closed/4089.v
+++ b/test-suite/bugs/closed/4089.v
@@ -163,7 +163,7 @@ Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope.
 
 Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope.
 
-Inductive Unit : Type1 :=
+Inductive Unit : Set :=
     tt : Unit.
 
 Ltac done :=
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1b396d57ba..77339aef44 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -402,20 +402,33 @@ let extract_level env evd min tys =
       sign_level env evd ((Anonymous, None, concl) :: ctx)) tys 
   in sup_list min sorts
 
+let is_flexible_sort evd u =
+  match Univ.Universe.level u with
+  | Some l -> Evd.is_flexible_level evd l
+  | None -> false
+
 let inductive_levels env evdref poly arities inds =
-  let destarities = List.map (Reduction.dest_arity env) arities in
-  let levels = List.map (fun (ctx,a) -> 
+  let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
+  let levels = List.map (fun (x,(ctx,a)) -> 
     if a = Prop Null then None
     else Some (univ_of_sort a)) destarities
   in
   let cstrs_levels, min_levels, sizes = 
     CList.split3
-      (List.map2 (fun (_,tys,_) (ctx,du) -> 
+      (List.map2 (fun (_,tys,_) (arity,(ctx,du)) -> 
 	let len = List.length tys in
+	let minlev = Sorts.univ_of_sort du in
 	let minlev =
 	  if len > 1 && not (is_impredicative env du) then
-	    Univ.type0_univ
-	  else Univ.type0m_univ
+	    Univ.sup minlev Univ.type0_univ
+	  else minlev
+	in
+	let minlev =
+	  (** Indices contribute. *)
+	  if Indtypes.is_indices_matter () && List.length ctx > 0 then (
+	    let ilev = sign_level env !evdref ctx in
+	      Univ.sup ilev minlev)
+	  else minlev
 	in
 	let clev = extract_level env !evdref minlev tys in
 	  (clev, minlev, len)) inds destarities)
@@ -425,32 +438,25 @@ let inductive_levels env evdref poly arities inds =
   let levels' = Universes.solve_constraints_system (Array.of_list levels)
     (Array.of_list cstrs_levels) (Array.of_list min_levels)
   in
-  let evd =
-    CList.fold_left3 (fun evd cu (ctx,du) len ->
+  let evd, arities =
+    CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len ->
       if is_impredicative env du then
 	(** Any product is allowed here. *)
-	evd
+	evd, arity :: arities
       else (** If in a predicative sort, or asked to infer the type,
 	       we take the max of:
 	       - indices (if in indices-matter mode)
 	       - constructors
 	       - Type(1) if there is more than 1 constructor
 	   *)
-	let evd = 
-	  (** Indices contribute. *)
-	  if Indtypes.is_indices_matter () && List.length ctx > 0 then (
-	    let ilev = sign_level env !evdref ctx in
-	      Evd.set_leq_sort env evd (Type ilev) du)
-	  else evd
-	in
         (** Constructors contribute. *)
 	let evd = 
 	  if Sorts.is_set du then
 	    if not (Evd.check_leq evd cu Univ.type0_univ) then 
 	      raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType)
 	    else evd
-	  else
-	    Evd.set_leq_sort env evd (Type cu) du
+	  else evd
+	    (* Evd.set_leq_sort env evd (Type cu) du *)
 	in
 	let evd = 
 	  if len >= 2 && Univ.is_type0m_univ cu then 
@@ -459,9 +465,19 @@ let inductive_levels env evdref poly arities inds =
 	       land in Prop directly (no informative arguments as well). *)
 	    Evd.set_leq_sort env evd (Prop Pos) du
 	  else evd
-	in evd)
-    !evdref (Array.to_list levels') destarities sizes
-  in evdref := evd; arities
+	in
+	  (* let arity = it_mkProd_or_LetIn (mkType cu) ctx in *\) *)
+	  let duu = Sorts.univ_of_sort du in
+	  let evd =
+	    if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then
+	      if is_flexible_sort evd duu then
+		Evd.set_eq_sort env evd (Prop Null) du
+	      else evd
+	    else Evd.set_eq_sort env evd (Type cu) du
+	  in
+	    (evd, arity :: arities))
+    (!evdref,[]) (Array.to_list levels') destarities sizes
+  in evdref := evd; List.rev arities
 
 let check_named (loc, na) = match na with
 | Name _ -> ()