Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).

6 files changed, 48 insertions, 12 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 7e4d37b2e..0b7cd89f2 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -451,9 +451,44 @@ let arity_of_case_predicate env (ind,params) dep k =
 (* Inferring the sort of parameters of a polymorphic inductive type
    knowing the sort of the conclusion *)
 
-let type_of_inductive_knowing_conclusion env ((mib,mip),u) conclty =
-  let subst = Inductive.make_inductive_subst mib u in
-    subst_univs_constr subst mip.mind_arity.mind_user_arity
+
+(* 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 evdref scl is = function
+  | (_,Some _,_ as d)::sign, exp ->
+      d :: instantiate_universes env evdref scl is (sign, exp)
+  | d::sign, None::exp ->
+      d :: instantiate_universes env evdref scl is (sign, exp)
+  | (na,None,ty)::sign, Some u::exp ->
+      let ctx,_ = Reduction.dest_arity env ty in
+      let s =
+	(* Does the sort of parameter [u] appear in (or equal)
+           the sort of inductive [is] ? *)
+        if univ_depends u is then
+          scl (* constrained sort: replace by scl *)
+        else
+          (* unconstriained sort: replace by fresh universe *)
+          let evm, s = Evd.new_sort_variable Evd.univ_flexible !evdref in
+	    evdref := evm; s
+      in
+      (na,None,mkArity(ctx,s)):: instantiate_universes env evdref scl is (sign, exp)
+  | sign, [] -> sign (* Uniform parameters are exhausted *)
+  | [], _ -> assert false
+
+let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
+  match mip.mind_arity with
+  | RegularArity s ->
+    let subst = Inductive.make_inductive_subst mib u in
+      sigma, subst_univs_constr subst s.mind_user_arity
+  | TemplateArity ar ->
+    let _,scl = Reduction.dest_arity env conclty in
+    let ctx = List.rev mip.mind_arity_ctxt in
+    let evdref = ref sigma in
+    let ctx =
+      instantiate_universes
+        env evdref scl ar.template_level (ctx,ar.template_param_levels) in
+      !evdref, mkArity (List.rev ctx,scl)
 
 (***********************************************)
 (* Guard condition *)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 39451ec05..34ddce72b 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -142,7 +142,7 @@ i*)
 (********************)
 
 val type_of_inductive_knowing_conclusion :
-  env -> Inductive.mind_specif puniverses -> types -> types
+  env -> evar_map -> Inductive.mind_specif puniverses -> types -> evar_map * types
 
 (********************)
 val control_only_guard : env -> types -> unit
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 31487125a..ccb9420fd 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -190,7 +190,7 @@ let retype ?(polyprop=true) sigma =
 	 with Reduction.NotArity -> retype_error NotAnArity)
     | Const cst ->
       let t = constant_type_in env cst in
-	(try Typeops.type_of_constant_knowing_parameters env t argtyps
+	(try Typeops.type_of_constant_type_knowing_parameters env t argtyps
 	 with Reduction.NotArity -> retype_error NotAnArity)
     | Var id -> type_of_var env id
     | Construct cstr -> type_of_constructor env cstr
@@ -211,13 +211,13 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
   match kind_of_term c with
     | Ind (ind,u) ->
         let spec = Inductive.lookup_mind_specif env ind in
-        type_of_inductive_knowing_conclusion env (spec,u) conclty
+          type_of_inductive_knowing_conclusion env sigma (spec,u) conclty
     | Const cst ->
         let t = constant_type_in 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
+          sigma, Typeops.type_of_constant_type_knowing_parameters env t [||]
+    | Var id -> sigma, type_of_var env id
+    | Construct cstr -> sigma, type_of_constructor env cstr
     | _ -> assert false
 
 (* Profiling *)
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index fc1dd3564..b8b458555 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -41,4 +41,4 @@ 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
+  env -> evar_map -> constr -> types -> evar_map * types
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index bd559ddd5..cc473bd86 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -27,7 +27,7 @@ let meta_type evd mv =
 
 let constant_type_knowing_parameters env cst jl =
   let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
-  type_of_constant_knowing_parameters env (constant_type_in env cst) paramstyp
+  type_of_constant_type_knowing_parameters env (constant_type_in env cst) paramstyp
 
 let inductive_type_knowing_parameters env (ind,u) jl =
   let mspec = lookup_mind_specif env ind in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 16eeaa293..2cf730f11 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -98,7 +98,8 @@ let construct_of_constr_block = construct_of_constr false
 let constr_type_of_idkey env idkey =
   match idkey with
   | ConstKey cst ->
-      mkConst cst, (Environ.lookup_constant cst env).const_type
+    let const_type = (Environ.lookup_constant cst env).const_type in
+      mkConst cst, Typeops.type_of_constant_type env const_type
   | VarKey id ->
       let (_,_,ty) = lookup_named id env in
       mkVar id, ty