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.

1 files changed, 36 insertions, 20 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1b396d57b..77339aef4 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 _ -> ()