fixing r11433 again:

- backtrack on kernel modifications: the monomorphic instance of an inductive
  type is constrained to live in an universe higher (or equal) than all the
  instances
- improved support for polymorphic inductive types at the refiner level:
  introduced type_of_inductive_knowing_conclusion that computes the
  instance to match the current conclusion universe.



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

6 files changed, 77 insertions, 13 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 93d0d96b20..918a32c956 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -147,17 +147,15 @@ let rec make_subst env = function
       let args = match args with _::args -> args | [] -> [] in
       let ctx,subst = make_subst env (sign, exp, args) in
       d::ctx, subst
-  | (na,None,t as d)::sign, Some u::exp, a::args ->
+  | d::sign, Some u::exp, a::args ->
       (* We recover the level of the argument, but we don't change the *)
       (* level in the corresponding type in the arity; this level in the *)
       (* arity is a global level which, at typing time, will be enforce *)
       (* to be greater than the level of the argument; this is probably *)
       (* a useless extra constraint *)
-      let _,ars = dest_arity env a in
-      let s = sort_as_univ ars in
+      let s = sort_as_univ (snd (dest_arity env a)) in
       let ctx,subst = make_subst env (sign, exp, args) in
-      let t = actualize_decl_level env ars t in
-      (na,None,t)::ctx, cons_subst u s subst
+      d::ctx, cons_subst u s subst
   | (na,None,t as d)::sign, Some u::exp, [] ->
       (* No more argument here: we instantiate the type with a fresh level *)
       (* which is first propagated to the corresponding premise in the arity *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index d4290c7641..d161ce612b 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -393,6 +393,58 @@ let arity_of_case_predicate env (ind,params) dep k =
   it_mkProd_or_LetIn concl arsign
 
 (***********************************************)
+(* Inferring the sort of parameters of a polymorphic inductive type
+   knowing the sort of the conclusion *)
+
+(* Check if u (sort of a parameter) appears in the sort of the
+   inductive (is). This is done by trying to enforce u > u' >= is
+   in the empty univ graph. If an inconsistency appears, then
+   is depends on u. *)  
+let is_constrained is u =
+  try
+    let u' = fresh_local_univ() in
+    let _ =
+      merge_constraints
+        (enforce_geq u (super u')
+          (enforce_geq u' is Constraint.empty))
+        initial_universes in
+    false
+  with UniverseInconsistency _ -> true
+
+(* Compute the inductive argument types: replace the sorts
+   that appear in the type of the inductive by the sort of the
+   conclusion, and the other ones by fresh universes. *)
+let rec instantiate_universes env scl is = function
+  | (_,Some _,_ as d)::sign, exp ->
+      d :: instantiate_universes env scl is (sign, exp)
+  | d::sign, None::exp ->
+      d :: instantiate_universes env scl is (sign, exp)
+  | (na,None,ty)::sign, Some u::exp ->
+      let ctx,_ = Reduction.dest_arity env ty in
+      let s =
+        if is_constrained is u then
+          scl (* constrained sort: replace by scl *)
+        else
+          (* unconstriained sort: replace by fresh universe *)
+          new_Type_sort() in
+      (na,None,mkArity(ctx,s)):: instantiate_universes env scl is (sign, exp)
+  | sign, [] -> sign (* Uniform parameters are exhausted *)
+  | [], _ -> assert false
+
+(* Does not deal with universes, but only with Set/Type distinction *)
+let type_of_inductive_knowing_conclusion env mip conclty =
+  match mip.mind_arity with
+  | Monomorphic s ->
+      s.mind_user_arity
+  | Polymorphic ar ->
+      let _,scl = Reduction.dest_arity env conclty in
+      let ctx = List.rev mip.mind_arity_ctxt in
+      let ctx =
+        instantiate_universes
+          env scl ar.poly_level (ctx,ar.poly_param_levels) in
+      mkArity (List.rev ctx,scl)
+
+(***********************************************)
 (* Guard condition *)
 
 (* A function which checks that a term well typed verifies both
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 46692b33b3..7e7b49d263 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -113,6 +113,11 @@ val make_default_case_info : env -> case_style -> inductive -> case_info
 i*)
 
 (********************)
+
+val type_of_inductive_knowing_conclusion :
+  env -> one_inductive_body -> types -> types
+
+(********************)
 val control_only_guard : env -> types -> unit
 
 val subst_inductive : Mod_subst.substitution -> inductive -> inductive
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 8b32224d2d..03afe0a179 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -139,6 +139,20 @@ let get_sort_family_of env sigma c = let _,_,f,_ = retype sigma [] in f env c
 let type_of_global_reference_knowing_parameters env sigma c args =
   let _,_,_,f = retype sigma [] in f env c args
 
+let type_of_global_reference_knowing_conclusion env sigma c conclty =
+  let conclty = nf_evar sigma conclty in
+  match kind_of_term c with
+    | Ind ind ->
+        let (_,mip) = Inductive.lookup_mind_specif env ind in
+        type_of_inductive_knowing_conclusion env mip conclty
+    | Const cst ->
+        let t = constant_type env cst in
+        (* TODO *)
+        Typeops.type_of_constant_knowing_parameters env t [||]
+    | Var id -> type_of_var env id
+    | Construct cstr -> type_of_constructor env cstr
+    | _ -> assert false
+
 (* We are outside the kernel: we take fresh universes *)
 (* to avoid tactics and co to refresh universes themselves *)
 let get_type_of env sigma c =
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 6dbd426b24..c7901e9498 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -37,3 +37,5 @@ val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
 val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> 
   constr array -> types
  
+val type_of_global_reference_knowing_conclusion :
+  env -> evar_map -> constr -> types -> types
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 15f8b8a731..eb879d977a 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -237,12 +237,6 @@ let check_conv_leq_goal env sigma arg ty conclty =
 let goal_type_of env sigma c =
   (if !check then type_of else Retyping.get_type_of) env sigma c
 
-let refresh_poly_universes c =
-  let (ctx,t) = decompose_prod_assum c in
-  let ctx' = List.map (fun (na,b,ty) -> (na,b,refresh_universes ty)) ctx in
-  let t' = refresh_universes t in
-  it_mkProd_or_LetIn t' ctx'
-
 let rec mk_refgoals sigma goal goalacc conclty trm =
   let env = evar_env goal in
   let hyps = goal.evar_hyps in
@@ -272,8 +266,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 		when (isInd f or has_polymorphic_type (destConst f)) ->
 		(* Sort-polymorphism of definition and inductive types *)
 		goalacc, 
-		refresh_poly_universes
-                  (type_of_global_reference_knowing_parameters env sigma f [||])
+                type_of_global_reference_knowing_conclusion env sigma f conclty
 	    | _ -> 
 		mk_hdgoals sigma goal goalacc f
 	in