Inductifs avec polymorphisme de sorte (version initiale)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8673 85f007b7-540e-0410-9357-904b9bb8a0f7

12 files changed, 378 insertions, 147 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 3adbd6e36..8d6c3d9ea 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -59,13 +59,10 @@ let ind_subst mind mib =
 (* Instantiate inductives in constructor type *)
 let constructor_instantiate mind mib c =
   let s = ind_subst mind mib in
-  type_app (substl s) c
+  substl s c
 
-(* Instantiate the parameters of the inductive type *)
-(* TODO: verify the arg of LetIn correspond to the value in the
-   signature ? *)
-let instantiate_params t args sign =
-  let fail () =
+let instantiate_params full t args sign =
+  let fail () = 
     anomaly "instantiate_params: type, ctxt and args mismatch" in
   let (rem_args, subs, ty) =
     Sign.fold_rel_context
@@ -73,26 +70,125 @@ let instantiate_params t args sign =
         match (copt, largs, kind_of_term ty) with
           | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
           | (Some b,_,LetIn(_,_,_,t))    -> (largs, (substl subs b)::subs, t)
-	  | _                            -> fail())
+	  | (_,[],_)                -> if full then fail() else ([], subs, ty)
+	  | _                       -> fail ())
       sign
       ~init:(args,[],t) 
   in
   if rem_args <> [] then fail();
-  type_app (substl subs) ty
+  substl subs ty
+
+let instantiate_partial_params = instantiate_params false
 
 let full_inductive_instantiate mib params t =
-  instantiate_params t params mib.mind_params_ctxt
+  instantiate_params true t params mib.mind_params_ctxt
 
 let full_constructor_instantiate (((mind,_),mib,_),params) =
   let inst_ind = constructor_instantiate mind mib in
   (fun t ->
-    instantiate_params (inst_ind t) params mib.mind_params_ctxt)
+    instantiate_params true (inst_ind t) params mib.mind_params_ctxt)
 
 (************************************************************************)
 (************************************************************************)
 
 (* Functions to build standard types related to inductive *)
 
+(* For each inductive type of a block that is of level u_i, we have
+   the constraints that u_i >= v_i where v_i is the type level of the
+   types of the constructors of this inductive type. Each v_i depends
+   of some of the u_i and of an extra (maybe non variable) universe,
+   say w_i. Typically, for three inductive types, we could have
+
+   u1,u2,u3,w1 <= u1
+   u1       w2 <= u2
+      u2,u3,w3 <= u3
+
+   From this system of inequations, we shall deduce
+
+   w1,w2,w3 <= u1
+   w1,w2 <= u2
+   w1,w2,w3 <= u3
+*)   
+
+let number_of_inductives mib = Array.length mib.mind_packets
+let number_of_constructors mip = Array.length mip.mind_consnames
+
+(* 
+Computing the actual sort of an applied or partially applied inductive type:
+
+I_i: forall uniformparams:utyps, forall otherparams:otyps, Type(a)
+uniformargs : utyps 
+otherargs : otyps
+I_1:forall ...,s_1;...I_n:forall ...,s_n |- sort(C_kj(uniformargs)) = s_kj
+s'_k = max(..s_kj..)
+merge(..s'_k..) = ..s''_k..
+--------------------------------------------------------------------
+Gamma |- I_i uniformargs otherargs : phi(s''_i)
+
+where
+
+- if p=0, phi() = Prop
+- if p=1, phi(s) = s
+- if p<>1, phi(s) = sup(Set,s)
+
+Remark: Set (predicative) is encoded as Type(0)
+*)
+
+let find_constraint levels level_bounds i nci =
+  if nci = 0 then mk_Prop
+  else
+    let level_bounds' = solve_constraints_system levels level_bounds in
+    let level = level_bounds'.(i) in
+    if nci = 1 & is_empty_universe level then mk_Prop
+    else if Univ.is_base level then mk_Set else Type level
+
+let find_inductive_level env (mib,mip) (_,i) levels level_bounds =
+  find_constraint levels level_bounds i (number_of_constructors mip)
+
+let set_inductive_level env s t = 
+  let sign,s' = dest_prod_assum env t in
+  if family_of_sort s <> family_of_sort (destSort s') then
+    (* This induces reductions if user_arity <> nf_arity *)
+    mkArity (sign,s)
+  else
+    t
+
+let constructor_instances env (mib,mip) (_,i) args =
+  let nargs = Array.length args in
+  let args = Array.to_list args in
+  let uargs = 
+    if nargs > mib.mind_nparams_rec then
+      fst (list_chop mib.mind_nparams_rec args)
+    else args in
+  let arities =
+    Array.map (fun mip -> destArity mip.mind_nf_arity) mib.mind_packets in
+  (* Compute the minimal type *)
+  let levels = Array.init 
+    (number_of_inductives mib) (fun _ -> fresh_local_univ ()) in
+  let arities = list_tabulate (fun i -> 
+    let ctx,s = arities.(i) in
+    let s = match s with Type _ -> Type (levels.(i)) | s -> s in
+    (Name mib.mind_packets.(i).mind_typename,None,mkArity (ctx,s)))
+    (number_of_inductives mib) in
+             (* Remark: all arities are closed hence no need for lift *)
+  let env_ar = push_rel_context (List.rev arities) env in
+  let uargs = List.map (lift (number_of_inductives mib)) uargs in
+  let lc =
+    Array.map (fun mip ->
+        Array.map (fun c -> 
+	    instantiate_partial_params c uargs mib.mind_params_ctxt)
+          mip.mind_nf_lc)
+      mib.mind_packets in
+  env_ar, lc, levels
+
+let is_small_inductive (mip,mib) = is_small (snd (destArity mib.mind_nf_arity))
+
+let max_inductive_sort v =
+  let v = Array.map (function
+    | Type u -> u
+    | _ -> anomaly "Only type levels when computing the minimal sort of an inductive type") v in
+  Univ.sup_array v
+
 (* Type of an inductive type *)
 
 let type_of_inductive (_,mip) = mip.mind_user_arity
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index f419bc3fa..a0ff0cefb 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -69,3 +69,17 @@ val scrape_mind : env -> mutual_inductive -> mutual_inductive
 (*s Guard conditions for fix and cofix-points. *)
 val check_fix : env -> fixpoint -> unit
 val check_cofix : env -> cofixpoint -> unit
+
+(*s Support for sort-polymorphic inductive types *)
+
+val constructor_instances : env -> mind_specif -> inductive -> 
+  constr array -> env * types array array * universe array
+
+val set_inductive_level : env -> sorts -> types -> types
+
+val find_inductive_level : env -> mind_specif -> inductive -> 
+  universe array -> universe array -> sorts
+
+val is_small_inductive : mind_specif -> bool
+
+val max_inductive_sort : sorts array -> universe
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 9e8d58fa8..7049a8afe 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -103,7 +103,7 @@ let error_cant_apply_not_functional env rator randl =
   raise (TypeError (env, CantApplyNonFunctional (rator,randl)))
 
 let error_cant_apply_bad_type env t rator randl =
-  raise(TypeError (env, CantApplyBadType (t,rator,randl)))
+  raise (TypeError (env, CantApplyBadType (t,rator,randl)))
 
 let error_ill_formed_rec_body env why lna i =
   raise (TypeError (env, IllFormedRecBody (why,lna,i)))
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 89a1c1982..29ec5007a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -36,7 +36,7 @@ let conv_leq_vecti env v1 v2 =
 
 (* This should be a type (a priori without intension to be an assumption) *)
 let type_judgment env j =
-  match kind_of_term(whd_betadeltaiota env (body_of_type j.uj_type)) with
+  match kind_of_term(whd_betadeltaiota env j.uj_type) with
     | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | _ -> error_not_type env j
 
@@ -47,11 +47,9 @@ let assumption_of_judgment env j =
   with TypeError _ ->
     error_assumption env j
 
-(*
-let aojkey = Profile.declare_profile "assumption_of_judgment";;
-let assumption_of_judgment env j
-  = Profile.profile2 aojkey assumption_of_judgment env j;;
-*)
+let sort_judgment env j = (type_judgment env j).utj_type
+
+let on_judgment_type f j = { j with uj_type = f j.uj_type }
 
 (************************************************)
 (* Incremental typing rules: builds a typing judgement given the *)
@@ -62,11 +60,11 @@ let assumption_of_judgment env j
 (* Prop and Set *)
 
 let judge_of_prop =
-  { uj_val = body_of_type mkProp;
+  { uj_val = mkProp;
     uj_type = mkSort type_0 }
 
 let judge_of_set =
-  { uj_val = body_of_type mkSet;
+  { uj_val = mkSet;
     uj_type = mkSort type_0 }
 
 let judge_of_prop_contents = function
@@ -77,7 +75,7 @@ let judge_of_prop_contents = function
 
 let judge_of_type u =
   let uu = super u in
-  { uj_val = body_of_type (mkType u);
+  { uj_val = mkType u;
     uj_type = mkType uu }
 
 (*s Type of a de Bruijn index. *)
@@ -90,12 +88,6 @@ let judge_of_relative env n =
   with Not_found -> 
     error_unbound_rel env n
 
-(*
-let relativekey = Profile.declare_profile "judge_of_relative";;
-let judge_of_relative env n =
-  Profile.profile2 relativekey judge_of_relative env n;;
-*)
-
 (* Type of variables *)
 let judge_of_variable env id =
   try
@@ -143,12 +135,6 @@ let judge_of_constant env cst =
     check_args env constr ce.const_hyps in 
   make_judge constr (constant_type env cst)
 
-(*
-let tockey = Profile.declare_profile "type_of_constant";;
-let type_of_constant env c 
-  = Profile.profile3 tockey type_of_constant env c;;
-*)
-
 (* Type of a lambda-abstraction. *)
 
 (* [judge_of_abstraction env name var j] implements the rule
@@ -214,9 +200,11 @@ let sort_of_product env domsort rangsort =
           rangsort
         else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
-          domsort
+          Type (sup u1 base_univ)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop _,  Type _)  -> rangsort
+    | (Prop Pos,  Type u2)  -> Type (sup base_univ u2)
+    (* Product rule (Prop,Type_i,Type_i) *)
+    | (Prop Null, Type _)  -> rangsort
     (* Product rule (Type_i,Type_i,Type_i) *) 
     | (Type u1, Type u2) -> Type (sup u1 u2)
 
@@ -266,12 +254,6 @@ let judge_of_inductive env i =
   let specif = lookup_mind_specif env i in
   make_judge constr (type_of_inductive specif)
 
-(*
-let toikey = Profile.declare_profile "judge_of_inductive";;
-let judge_of_inductive env i
-  = Profile.profile2 toikey judge_of_inductive env i;;
-*)
-
 (* Constructors. *)
 
 let judge_of_constructor env c =
@@ -283,12 +265,6 @@ let judge_of_constructor env c =
   let specif = lookup_mind_specif env (inductive_of_constructor c) in
   make_judge constr (type_of_constructor c specif)
 
-(*
-let tockey = Profile.declare_profile "judge_of_constructor";;
-let judge_of_constructor env cstr
-  = Profile.profile2 tockey judge_of_constructor env cstr;;
-*)
-
 (* Case. *)
 
 let check_branch_types env cj (lfj,explft) = 
@@ -312,12 +288,6 @@ let judge_of_case env ci pj cj lfj =
      uj_type = rslty },
   Constraint.union univ univ')
 
-(*
-let tocasekey = Profile.declare_profile "judge_of_case";;
-let judge_of_case env ci pj cj lfj
-  = Profile.profile6 tocasekey judge_of_case env ci pj cj lfj;;
-*)
-
 (* Fixpoints. *)
 
 (* Checks the type of a general (co)fixpoint, i.e. without checking *)
@@ -366,8 +336,12 @@ let rec execute env cstr cu =
     | App (f,args) ->
 	let (j,cu1) = execute env f cu in
         let (jl,cu2) = execute_array env args cu1 in
-	univ_combinator cu2
-	  (judge_of_apply env j jl)
+	let (j',cu) = univ_combinator cu2 (judge_of_apply env j jl) in
+	if isInd f then
+	  (* Sort-polymorphism of inductive types *)
+	  adjust_inductive_level env (destInd f) args (j',cu)
+	else
+	  (j',cu)
 	    
     | Lambda (name,c1,c2) -> 
         let (varj,cu1) = execute_type env c1 cu in
@@ -395,6 +369,7 @@ let rec execute env cstr cu =
         let (tj,cu2) = execute_type env t cu1 in
 	univ_combinator cu2
           (judge_of_cast env cj k tj)
+
     (* Inductive types *)
     | Ind ind ->
 	(judge_of_inductive env ind, cu)
@@ -442,18 +417,25 @@ and execute_recdef env (names,lar,vdef) i cu =
   univ_combinator cu2
     ((lara.(i),(names,lara,vdefv)),cst)
 
-and execute_array env v cu =
-  let (jl,cu1) = execute_list env (Array.to_list v) cu in
-  (Array.of_list jl, cu1)
-
-and execute_list env l cu =
-  match l with
-  | [] -> 
-      ([], cu)
-  | c::r -> 
-      let (j,cu1) = execute env c cu in 
-      let (jr,cu2) = execute_list env r cu1 in
-      (j::jr, cu2)
+and execute_array env = array_fold_map' (execute env)
+
+and execute_list env = list_fold_map' (execute env) 
+
+and adjust_inductive_level env ind args (j,cu) =
+  let specif = lookup_mind_specif env ind in
+  if is_small_inductive specif then
+    (* No polymorphism *)
+    (j,cu)
+  else
+    (* Retyping constructor with the actual arguments *)
+    let env',llc,ls0 = constructor_instances env specif ind args in
+    let (llj,cu1) = array_fold_map' (execute_array env') llc cu in
+    let ls =
+      Array.map (fun lj ->
+	max_inductive_sort (Array.map (sort_judgment env) lj)) llj
+    in
+    let s = find_inductive_level env specif ind ls0 ls in
+    (on_judgment_type (set_inductive_level env s) j, cu1)
 
 (* Derived functions *)
 let infer env constr =
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index ed90c393e..412998f6e 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -33,6 +33,8 @@ val infer_local_decls :
 
 val assumption_of_judgment :  env -> unsafe_judgment -> types
 val type_judgment          :  env -> unsafe_judgment -> unsafe_type_judgment
+val on_judgment_type       :  
+  (types -> types) -> unsafe_judgment -> unsafe_judgment
 
 (*s Type of sorts. *)
 val judge_of_prop_contents : contents -> unsafe_judgment
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 5f2f845aa..1e0991e3d 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -36,11 +36,11 @@ open Util
  *)
 
 type universe_level =
-    { u_mod : Names.dir_path;
-      u_num : int }
+  | Base
+  | Level of Names.dir_path * int
 
 type universe =
-  | Variable of universe_level
+  | Atom of universe_level
   | Max of universe_level list * universe_level list
   
 module UniverseOrdered = struct
@@ -48,30 +48,31 @@ module UniverseOrdered = struct
   let compare = Pervasives.compare
 end
 
-let string_of_univ_level u =
-  Names.string_of_dirpath u.u_mod^"."^string_of_int u.u_num
+let string_of_univ_level = function
+  | Base -> "0"
+  | Level (d,n) -> Names.string_of_dirpath d^"."^string_of_int n
 
-let make_univ (m,n) = Variable { u_mod=m; u_num=n }
+let make_univ (m,n) = Atom (Level (m,n))
 
 let pr_uni_level u = str (string_of_univ_level u)
 
 let pr_uni = function
-  | Variable u -> 
+  | Atom u -> 
       pr_uni_level u
-  | Max ([],[]) ->
+  | Max ([],[Base]) ->
       int 1
   | Max (gel,gtl) ->
-      str "max(" ++ 
-      prlist_with_sep pr_coma pr_uni_level gel ++
-      (if gel <> [] & gtl <> [] then pr_coma () else mt ()) ++
-      prlist_with_sep pr_coma
-	(fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl ++
+      str "max(" ++ hov 0
+       (prlist_with_sep pr_coma pr_uni_level gel ++
+	  (if gel <> [] & gtl <> [] then pr_coma () else mt ()) ++
+	prlist_with_sep pr_coma
+	  (fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl) ++
       str ")"
 
 (* Returns the formal universe that lies juste above the universe variable u.
    Used to type the sort u. *)
 let super = function
-  | Variable u -> 
+  | Atom u -> 
       Max ([],[u])
   | Max _ ->
       anomaly ("Cannot take the successor of a non variable universes:\n"^
@@ -79,13 +80,19 @@ let super = function
 
 (* Returns the formal universe that is greater than the universes u and v.
    Used to type the products. *)
-let sup u v = 
+let sup u v =
   match u,v with
-    | Variable u, Variable v -> Max ((if u = v then [u] else [u;v]),[])
-    | Variable u, Max (gel,gtl) -> Max (list_add_set u gel,gtl)
-    | Max (gel,gtl), Variable v -> Max (list_add_set v gel,gtl)
+    | Atom u, Atom v -> if u = v then Atom u else Max ([u;v],[])
+    | u, Max ([],[]) -> u
+    | Max ([],[]), v -> v
+    | Atom u, Max (gel,gtl) -> Max (list_add_set u gel,gtl)
+    | Max (gel,gtl), Atom v -> Max (list_add_set v gel,gtl)
     | Max (gel,gtl), Max (gel',gtl') ->
-	Max (list_union gel gel',list_union gtl gtl')
+	let gel'' = list_union gel gel' in
+	let gtl'' = list_union gtl gtl' in
+	Max (list_subtract gel'' gtl'',gtl'')
+
+let sup_array ls = Array.fold_right sup ls (Max ([],[]))
 
 (* Comparison on this type is pointer equality *)
 type canonical_arc =
@@ -115,11 +122,19 @@ let declare_univ u g =
   else
     g
 
-(* When typing Prop and Set, there is no constraint on the level,
-   hence the definition of prop_univ *)
+(* The level of Set *)
+let base_univ = Atom Base
+
+let is_base = function
+  | Atom Base -> true
+  | Max ([Base],[]) -> warning "Non canonical Set"; true
+  | u -> false
+
+(* When typing [Prop] and [Set], there is no constraint on the level,
+   hence the definition of [prop_univ], the type of [Prop] *)
 
 let initial_universes = UniverseMap.empty
-let prop_univ = Max ([],[])
+let prop_univ = Max ([],[Base])
 
 (* Every universe_level has a unique canonical arc representative *)
 
@@ -377,23 +392,84 @@ type constraints = Constraint.t
 type constraint_function = 
     universe -> universe -> constraints -> constraints
 
+let constraint_add_leq v u c =
+  if v = Base then c else Constraint.add (v,Leq,u) c
+
 let enforce_geq u v c =
-  match u with
-    | Variable u -> (match v with
-	| Variable v -> Constraint.add (v,Leq,u) c
-	| Max (l1, l2) ->
-	    let d = List.fold_right (fun v -> Constraint.add (v,Leq,u)) l1 c in
-	    List.fold_right (fun v -> Constraint.add (v,Lt,u)) l2 d) 
-    | Max _ -> anomaly "A universe bound can only be a variable"
+  match u, v with
+  | Atom u, Atom v -> constraint_add_leq v u c
+  | Atom u, Max (gel,gtl) ->
+      let d = List.fold_right (fun v -> constraint_add_leq v u) gel c in
+      List.fold_right (fun v -> Constraint.add (v,Lt,u)) gtl d
+  | _ -> anomaly "A universe bound can only be a variable"
 
 let enforce_eq u v c =
   match (u,v) with
-    | Variable u, Variable v -> Constraint.add (u,Eq,v) c
+    | Atom u, Atom v -> Constraint.add (u,Eq,v) c
     | _ -> anomaly "A universe comparison can only happen between variables"
 
 let merge_constraints c g =
   Constraint.fold enforce_constraint c g
 
+(**********************************************************************)
+(* Tools for sort-polymorphic inductive types                         *)
+
+(* Temporary inductive type levels *)
+
+let fresh_level =
+  let n = ref 0 in fun () -> incr n; Level (Names.make_dirpath [],!n)
+
+let fresh_local_univ () = Atom (fresh_level ())
+
+(* Miscellaneous functions to remove or test local univ assumed to
+   occur only in the le constraints *)
+
+let make_max = function
+  | ([u],[]) -> Atom u
+  | (le,lt) -> Max (le,lt)
+
+let remove_constraint u = function
+  | Atom u' as x -> if u = u' then Max ([],[]) else x
+  | Max (le,lt) -> make_max (list_remove u le,lt)
+
+let is_empty_universe = function
+  | Max ([],[]) -> true
+  | _ -> false
+
+let is_direct_constraint u = function
+  | Atom u' -> u = u'
+  | Max (le,lt) -> List.mem u le
+
+(* 
+   Solve a system of universe constraint of the form
+
+   u_s11, ..., u_s1p1, w1 <= u1
+   ...
+   u_sn1, ..., u_snpn, wn <= un
+
+where 
+
+  - the ui (1 <= i <= n) are universe variables,
+  - the sjk select subsets of the ui for each equations, 
+  - the wi are arbitrary complex universes that do not mention the ui.
+*)
+
+let solve_constraints_system levels level_bounds =
+  let levels = 
+    Array.map (function Atom u -> u | _ -> anomaly "expects Atom") levels in
+  let v = Array.copy level_bounds in
+  let nind = Array.length v in
+  for i=0 to nind-1 do
+    for j=0 to nind-1 do
+      if i<>j & is_direct_constraint levels.(j) v.(i) then
+	v.(i) <- sup v.(i) v.(j)
+    done;
+    for j=0 to nind-1 do
+      v.(i) <- remove_constraint levels.(j) v.(i)
+    done
+  done;
+  v
+
 (* Pretty-printing *)
 
 let num_universes g =
@@ -446,19 +522,23 @@ let dump_universes output g =
   in
     UniverseMap.iter dump_arc g 
 
+(* Hash-consing *)
+
 module Huniv =
   Hashcons.Make(
     struct
       type t = universe
       type u = Names.dir_path -> Names.dir_path
-      let hash_aux hdir u = { u with u_mod=hdir u.u_mod }
+      let hash_aux hdir = function
+	| Base -> Base
+	| Level (d,n) -> Level (hdir d,n)
       let hash_sub hdir = function
-	| Variable u -> Variable (hash_aux hdir u)
+	| Atom u -> Atom (hash_aux hdir u)
 	| Max (gel,gtl) ->
 	    Max (List.map (hash_aux hdir) gel, List.map (hash_aux hdir) gtl)
       let equal u v =
 	match u, v with
-	  | Variable u, Variable v -> u == v
+	  | Atom u, Atom v -> u == v
 	  | Max (gel,gtl), Max (gel',gtl') ->
 	      (list_for_all2eq (==) gel gel') &&
               (list_for_all2eq (==) gtl gtl')
@@ -469,4 +549,3 @@ module Huniv =
 let hcons1_univ u =
   let _,_,hdir,_,_,_ = Names.hcons_names() in
   Hashcons.simple_hcons Huniv.f hdir u
-
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 56442cbcc..0fb1a4ca8 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -12,14 +12,21 @@
 
 type universe
 
+val base_univ : universe
 val prop_univ : universe
 val make_univ : Names.dir_path * int -> universe
 
+val is_base : universe -> bool
+
 (* The type of a universe *)
 val super : universe -> universe
+
 (* The max of 2 universes *)
 val sup   : universe -> universe -> universe
 
+(* The max of an array of universes *)
+val sup_array : universe array -> universe
+
 (*s Graphs of universes. *)
 
 type universes
@@ -47,6 +54,15 @@ exception UniverseInconsistency
 
 val merge_constraints : constraints -> universes -> universes
 
+(*s Support for sort-polymorphic inductive types *)
+
+val fresh_local_univ : unit -> universe
+
+val solve_constraints_system : universe array -> universe array -> 
+  universe array
+
+val is_empty_universe : universe -> bool
+
 (*s Pretty-printing of universes. *)
 
 val pr_uni : universe -> Pp.std_ppcmds
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 68342e706..b99ada769 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -367,21 +367,18 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 			  (join_loc floc argloc) env (evars_of !isevars)
 	      		  resj [hj]
 
-	in let resj = apply_rec env 1 fj args in
-	  (*
-	    let apply_one_arg (floc,tycon,jl) c =
-	    let (dom,rng) = split_tycon floc env isevars tycon in
-	    let cj = pretype dom env isevars lvar c in
-	    let rng_tycon =
-	    option_app (subst1 cj.uj_val) rng in
-	    let argloc = loc_of_rawconstr c in
-	    (join_loc floc argloc,rng_tycon,(argloc,cj)::jl)  in
-	    let _,_,jl =
-	    List.fold_left apply_one_arg (floc,mk_tycon j.uj_type,[]) args in
-	    let jl = List.rev jl in
-	    let resj = inh_apply_rel_list loc env isevars jl (floc,j) tycon in
-	  *)
-	  inh_conv_coerce_to_tycon loc env isevars resj tycon
+	in 
+	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj args) in
+	let resj =
+	  match kind_of_term resj.uj_val with
+	  | App (f,args) when isInd f ->
+	      let sigma = evars_of !isevars in
+	      let t = Retyping.type_of_applied_inductive env sigma (destInd f) args in
+	      let s = snd (splay_arity env sigma t) in
+	      on_judgment_type (set_inductive_level env s) resj
+		(* Rem: no need to send sigma: no head evar, it's an arity *)
+	  | _ -> resj in
+	inh_conv_coerce_to_tycon loc env isevars resj tycon
 
     | RLambda(loc,name,c1,c2)      ->
 	let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 715f54731..776f1313f 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -18,11 +18,6 @@ open Environ
 open Typeops
 open Declarations
 
-let outsort env sigma t =
-  match kind_of_term (whd_betadeltaiota env sigma t) with
-    | Sort s -> s
-    | _ -> anomaly "Retyping: found a type of type which is not a sort"
-
 let rec subst_type env sigma typ = function
   | [] -> typ
   | h::rest ->
@@ -38,9 +33,9 @@ let rec subst_type env sigma typ = function
 let sort_of_atomic_type env sigma ft args =
   let rec concl_of_arity env ar =
     match kind_of_term (whd_betadeltaiota env sigma ar) with
-      | Prod (na, t, b) -> concl_of_arity (push_rel (na,None,t) env) b
-      | Sort s -> s
-      | _ -> outsort env sigma (subst_type env sigma ft (Array.to_list args))
+    | Prod (na, t, b) -> concl_of_arity (push_rel (na,None,t) env) b
+    | Sort s -> s
+    | _ -> decomp_sort env sigma (subst_type env sigma ft (Array.to_list args))
   in concl_of_arity env ft
 
 let typeur sigma metamap =
@@ -78,7 +73,10 @@ let typeur sigma metamap =
          subst1 b (type_of (push_rel (name,Some b,c1) env) c2)
     | Fix ((_,i),(_,tys,_)) -> tys.(i)
     | CoFix (i,(_,tys,_)) -> tys.(i)
-    | App(f,args)->
+    | App(f,args) when isInd f ->
+	let t = type_of_applied_inductive env (destInd f) args in
+        strip_outer_cast (subst_type env sigma t (Array.to_list args))
+    | App(f,args) ->
         strip_outer_cast
           (subst_type env sigma (type_of env f) (Array.to_list args))
     | Cast (c,_, t) -> t
@@ -95,12 +93,17 @@ let typeur sigma metamap =
           | Prop _, (Prop Pos as s) -> s
           | Type _, (Prop Pos as s) when
               Environ.engagement env = Some ImpredicativeSet -> s
-          | Type _ as s, Prop Pos -> s
-	  | _, (Type u2 as s) -> s (*Type Univ.dummy_univ*))
+          | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.base_univ)
+	  | Prop Pos, (Type u2) -> Type (Univ.sup Univ.base_univ u2)
+	  | Prop Null, (Type _ as s) -> s
+	  | Type u1, Type u2 -> Type (Univ.sup u1 u2))
+    | App(f,args) when isInd f ->
+	let t = type_of_applied_inductive env (destInd f) args in
+        sort_of_atomic_type env sigma t args
     | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
     | Lambda _ | Fix _ | Construct _ ->
         anomaly "sort_of: Not a type (1)"
-    | _ -> outsort env sigma (type_of env t)
+    | _ -> decomp_sort env sigma (type_of env t)
 
   and sort_family_of env t =
     match kind_of_term t with
@@ -112,16 +115,31 @@ let typeur sigma metamap =
        family_of_sort (sort_of_atomic_type env sigma (type_of env f) args)
     | Lambda _ | Fix _ | Construct _ ->
         anomaly "sort_of: Not a type (1)"
-    | _ -> family_of_sort (outsort env sigma (type_of env t))
+    | _ -> family_of_sort (decomp_sort env sigma (type_of env t))
+
+  and type_of_applied_inductive env ind args =
+    let specif = lookup_mind_specif env ind in
+    let t = Inductive.type_of_inductive specif in
+    if is_small_inductive specif then
+      (* No polymorphism *)
+      t
+    else
+      (* Retyping constructor with the actual arguments *)
+      let env',llc,ls0 = constructor_instances env specif ind args in
+      let lls = Array.map (Array.map (sort_of env')) llc in
+      let ls = Array.map max_inductive_sort lls in
+      set_inductive_level env (find_inductive_level env specif ind ls0 ls) t
 
-  in type_of, sort_of, sort_family_of
+  in type_of, sort_of, sort_family_of, type_of_applied_inductive
 
-let get_type_of env sigma c = let f,_,_ = typeur sigma [] in f env c
-let get_sort_of env sigma t = let _,f,_ = typeur sigma [] in f env t
-let get_sort_family_of env sigma c = let _,_,f = typeur sigma [] in f env c
+let get_type_of env sigma c = let f,_,_,_ = typeur sigma [] in f env c
+let get_sort_of env sigma t = let _,f,_,_ = typeur sigma [] in f env t
+let get_sort_family_of env sigma c = let _,_,f,_ = typeur sigma [] in f env c
+let type_of_applied_inductive env sigma ind args =
+  let _,_,_,f = typeur sigma [] in f env ind args
 
 let get_type_of_with_meta env sigma metamap = 
-  let f,_,_ = typeur sigma metamap in f env
+  let f,_,_,_ = typeur sigma metamap in f env
 
 (* Makes an assumption from a constr *)
 let get_assumption_of env evc c = c
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index f0c01a56e..8631f5545 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -9,6 +9,7 @@
 (*i $Id$ i*)
 
 (*i*)
+open Names
 open Term
 open Evd
 open Environ
@@ -32,3 +33,6 @@ val get_assumption_of : env -> evar_map -> constr -> types
 
 (* Makes an unsafe judgment from a constr *)
 val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
+
+val type_of_applied_inductive : env -> evar_map -> inductive -> 
+  constr array -> types
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 38febedaa..85e75586b 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -91,7 +91,11 @@ let rec execute env evd cstr =
 	let j = execute env evd f in
         let jl = execute_array env evd args in
 	let (j,_) = judge_of_apply env j jl in
-	j
+	if isInd f then
+	  (* Sort-polymorphism of inductive types *)
+	  adjust_inductive_level env evd (destInd f) args j
+	else
+	  j
 	    
     | Lambda (name,c1,c2) -> 
         let j = execute env evd c1 in
@@ -133,17 +137,28 @@ and execute_recdef env evd (names,lar,vdef) =
   let _ = type_fixpoint env1 names lara vdefj in
   (names,lara,vdefv)
 
-and execute_array env evd v =
-  let jl = execute_list env evd (Array.to_list v) in
-  Array.of_list jl
-
-and execute_list env evd = function
-  | [] -> 
-      []
-  | c::r -> 
-      let j = execute env evd c in 
-      let jr = execute_list env evd r in
-      j::jr
+and execute_array env evd = Array.map (execute env evd)
+
+and execute_list env evd = List.map (execute env evd)
+
+and adjust_inductive_level env evd ind args j =
+  let specif = lookup_mind_specif env ind in
+  if is_small_inductive specif then
+    (* No polymorphism *)
+    j
+  else
+    (* Retyping constructor with the actual arguments *)
+    let env',llc,ls0 = constructor_instances env specif ind args in
+    let llj = Array.map (execute_array env' evd) llc in
+    let ls =
+      Array.map (fun lj ->
+	let ls =
+	  Array.map (fun c -> decomp_sort env (evars_of evd) c.uj_type) lj
+	in
+	max_inductive_sort ls) llj
+    in
+    let s = find_inductive_level env specif ind ls0 ls in
+    on_judgment_type (set_inductive_level env s) j
 
 let mcheck env evd c t =
   let sigma = Evd.evars_of evd in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 59ff7a322..36409794c 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -283,7 +283,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	mk_refgoals sigma goal goalacc ty t
 
     | App (f,l) ->
-	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
+	let (acc',hdty) =
+	  if isInd f 
+	  then (goalacc,type_of_applied_inductive env sigma (destInd f) l)
+	  else mk_hdgoals sigma goal goalacc f
+	in
 	let (acc'',conclty') =
 	  mk_arggoals sigma goal acc' hdty (Array.to_list l) in
 	check_conv_leq_goal env sigma trm conclty' conclty;
@@ -321,7 +325,11 @@ and mk_hdgoals sigma goal goalacc trm =
 	mk_refgoals sigma goal goalacc ty t
 
     | App (f,l) ->
-	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
+	let (acc',hdty) = 
+	  if isInd f 
+	  then (goalacc,type_of_applied_inductive env sigma (destInd f) l)
+	  else mk_hdgoals sigma goal goalacc f
+	in
 	mk_arggoals sigma goal acc' hdty (Array.to_list l)
 
     | Case (_,p,c,lf) ->