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

4 files changed, 73 insertions, 0 deletions

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