Try a new way of handling template universe levels

10 files changed, 153 insertions, 33 deletions

diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 85fd810264..10d54d2283 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -588,13 +588,13 @@ Qed.
 (** Smart constructors for polynomial expression,
     with reduction of constants *)
 
-Definition NPEadd e1 e2 :=
+Time Definition NPEadd e1 e2 :=
   match e1, e2 with
   | PEc c1, PEc c2 => PEc (c1 + c2)
   | PEc c, _ => if (c =? 0)%coef then e2 else e1 + e2
   |  _, PEc c => if (c =? 0)%coef then e1 else e1 + e2
     (* Peut t'on factoriser ici ??? *)
-  | _, _ => e1 + e2
+  | _, _ => (@PEadd C e1 e2)
   end%poly.
 Infix "++" := NPEadd (at level 60, right associativity).
 
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index 1d958d09b2..8bb44ecbc7 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -240,23 +240,23 @@ Ltac mkPolexpr C Cst CstPow rO rI radd rmul rsub ropp rpow t fv :=
         | (radd ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(PEadd e1 e2)
+          let e2 := mkP t2 in constr:(@PEadd C e1 e2)
         | (rmul ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(PEmul e1 e2)
+          let e2 := mkP t2 in constr:(@PEmul C e1 e2)
         | (rsub ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(PEsub e1 e2)
+          let e2 := mkP t2 in constr:(@PEsub C e1 e2)
         | (ropp ?t1) =>
           fun _ =>
-          let e1 := mkP t1 in constr:(PEopp e1)
+          let e1 := mkP t1 in constr:(@PEopp C e1)
         | (rpow ?t1 ?n) =>
           match CstPow n with
           | InitialRing.NotConstant =>
             fun _ => let p := Find_at t fv in constr:(PEX C p)
-          | ?c => fun _ => let e1 := mkP t1 in constr:(PEpow e1 c)
+          | ?c => fun _ => let e1 := mkP t1 in constr:(@PEpow C e1 c)
           end
         | _ =>
           fun _ => let p := Find_at t fv in constr:(PEX C p)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 761f11c115..16a044528f 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -26,12 +26,12 @@ let normalize_evar evd ev =
   | Evar (evk,args) -> (evk,args)
   | _ -> assert false
 
-let refresh_universes dir evd t =
+let refresh_universes ?(all=false) ?(with_globals=false) dir evd t =
   let evdref = ref evd in
   let modified = ref false in
-  let rec refresh t = match kind_of_term t with
+  let rec refresh dir t = match kind_of_term t with
     | Sort (Type u as s) when Univ.universe_level u = None
-			 (* || Evd.is_sort_variable evd s = None *) ->
+			 || (with_globals && Evd.is_sort_variable evd s = None) ->
       (modified := true;
        (* s' will appear in the term, it can't be algebraic *)
        let s' = evd_comb0 (new_sort_variable Evd.univ_flexible) evdref in
@@ -39,9 +39,9 @@ let refresh_universes dir evd t =
 	   (if dir then set_leq_sort !evdref s' s else
 	     set_leq_sort !evdref s s');
          mkSort s')
-    | Prod (na,u,v) -> mkProd (na,u,refresh v)
+    | Prod (na,u,v) -> mkProd (na,(if all then refresh true u else u),refresh dir v)
     | _ -> t in
-  let t' = refresh t in
+  let t' = refresh dir t in
   if !modified then !evdref, t' else evd, t
 
 (************************)
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 7276669bf5..ca03f9853f 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -34,7 +34,8 @@ type conv_fun_bool =
 val evar_define : conv_fun -> ?choose:bool -> ?dir:bool -> env -> evar_map -> 
   bool option -> existential -> constr -> evar_map
 
-val refresh_universes : bool -> evar_map -> types -> evar_map * types
+val refresh_universes : ?all:bool (* Include domains of products *) -> 
+  ?with_globals:bool -> bool -> evar_map -> types -> evar_map * types
 
 val solve_refl : ?can_drop:bool -> conv_fun_bool -> env ->  evar_map ->
   bool option -> existential_key -> constr array -> constr array -> evar_map
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index bca599305a..a4eae5fdff 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -817,3 +817,56 @@ let lift_tycon n = Option.map (lift n)
 let pr_tycon env = function
     None -> str "None"
   | Some t -> Termops.print_constr_env env t
+
+open Declarations
+
+let get_template_constructor_type evdref (ind, i) n =
+  let mib,oib = Global.lookup_inductive ind in
+  let ar =
+    match oib.mind_arity with
+    | RegularArity _ -> assert false
+    | TemplateArity templ -> templ
+  in
+  let ty = oib.mind_user_lc.(pred i) in
+  let subst = Inductive.ind_subst (fst ind) mib Univ.Instance.empty in
+  let ty = substl subst ty in
+  let rec aux l ty n =
+    match l, kind_of_term ty with
+    | None :: l, Prod (na, t, t') ->
+      mkProd (na, t, aux l t' (pred n))
+    | Some u :: l, Prod (na, t, t') ->
+      let u' = evd_comb0 (new_univ_variable Evd.univ_flexible) evdref in
+	(* evdref := set_leq_sort !evdref u'l (Type u); *)
+	let s = Univ.LMap.add (Option.get (Univ.Universe.level u))
+	  (Option.get (Univ.Universe.level u')) Univ.LMap.empty in
+	let dom = subst_univs_level_constr s t in
+	(* let codom = subst_univs_level_constr s t' in *)
+	  mkProd (na, dom, aux l t' (pred n))
+    | l, LetIn (na, t, b, t') ->
+      mkLetIn (na, t, b, aux l t' n)
+    | _ :: _, _ -> assert false (* All params should be abstracted by a forall or a let-in *)
+    | [], _ -> ty
+  in aux ar.template_param_levels ty n
+
+
+let get_template_constructor_type evdref (ind, i) n =
+  let mib,oib = Global.lookup_inductive ind in
+  let ar =
+    match oib.mind_arity with
+    | RegularArity _ -> assert false
+    | TemplateArity templ -> templ
+  in
+  let ty = oib.mind_user_lc.(pred i) in
+  let subst = Inductive.ind_subst (fst ind) mib Univ.Instance.empty in
+  let ty = substl subst ty in
+    ar.template_param_levels, ty
+
+let get_template_inductive_type evdref ind n =
+  let mib,oib = Global.lookup_inductive ind in
+  let ar =
+    match oib.mind_arity with
+    | RegularArity _ -> assert false
+    | TemplateArity templ -> templ
+  in
+  let ctx = oib.mind_arity_ctxt in
+    ar.template_param_levels, mkArity(ctx, Type ar.template_level)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index b860ce3370..d197ad2efe 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -216,3 +216,10 @@ val generalize_evar_over_rels : evar_map -> existential -> types * constr list
 val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
 val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
 val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
+
+(* val get_template_constructor_type : evar_map ref -> constructor -> int -> types *)
+val get_template_constructor_type : evar_map ref -> constructor -> int -> 
+  (Univ.universe option list * types)
+
+val get_template_inductive_type : evar_map ref -> inductive -> int -> 
+  (Univ.universe option list * types)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8e65cc480f..7cb3fa1a8b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -179,10 +179,10 @@ let process_inference_flags flags env initial_sigma (sigma,c) =
 (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
 let allow_anonymous_refs = ref false
 
-(* Utilisé pour inférer le prédicat des Cases *)
-(* Semble exagérement fort *)
-(* Faudra préférer une unification entre les types de toutes les clauses *)
-(* et autoriser des ? à rester dans le résultat de l'unification *)
+(* Utilisé pour inférer le prédicat des Cases *)
+(* Semble exagérement fort *)
+(* Faudra préférer une unification entre les types de toutes les clauses *)
+(* et autoriser des ? à rester dans le résultat de l'unification *)
 
 let evar_type_fixpoint loc env evdref lna lar vdefj =
   let lt = Array.length vdefj in
@@ -263,6 +263,16 @@ let evar_kind_of_term sigma c =
 (* Check with universe list? *)
 let pretype_global rigid env evd gr us = Evd.fresh_global ~rigid env evd gr
 
+let is_template_polymorphic_constructor env c =
+  match kind_of_term c with
+  | Construct ((ind, i), u) -> Environ.template_polymorphic_ind ind env
+  | _ -> false
+
+let is_template_polymorphic_constructor env c =
+  match kind_of_term c with
+  | Construct ((ind, i), u) -> Environ.template_polymorphic_ind ind env
+  | _ -> false
+
 let pretype_ref loc evdref env ref us =
   match ref with
   | VarRef id ->
@@ -277,9 +287,10 @@ let pretype_ref loc evdref env ref us =
             variables *)
          Pretype_errors.error_var_not_found_loc loc id)
   | ref ->
-      let evd, c = pretype_global univ_flexible env !evdref ref us in
-	evdref := evd;
-	make_judge c (Retyping.get_type_of env evd c)
+    let evd, c = pretype_global univ_flexible env !evdref ref us in
+    let () = evdref := evd in
+    let ty = Retyping.get_type_of env evd c in
+      make_judge c ty
 
 let pretype_sort evdref = function
   | GProp -> judge_of_prop
@@ -304,6 +315,10 @@ let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
 (* in environment [env], with existential variables [evdref] and *)
 (* the type constraint tycon *)
 
+let is_GHole = function
+  | GHole _ -> true
+  | _ -> false
+
 let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
   let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
   let pretype_type = pretype_type resolve_tc in
@@ -321,7 +336,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 
   | GEvar (loc, evk, instopt) ->
       (* Ne faudrait-il pas s'assurer que hyps est bien un
-	 sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
+	 sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
       let hyps = evar_filtered_context (Evd.find !evdref evk) in
       let args = match instopt with
         | None -> Array.of_list (instance_from_named_context hyps)
@@ -491,7 +506,20 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
       inh_conv_coerce_to_tycon loc env evdref j tycon
 
   | GApp (loc,f,args) ->
-    let fj = pretype empty_tycon env evdref lvar f in
+    let univs, fj = 
+      match f with
+      | GRef (loc, ConstructRef (ind, i as cstr), u')
+      	  when Environ.template_polymorphic_ind ind env ->
+       (** We refresh the universes so as to enforce using <= instead of instantiating
+      	   an unkwown ?X with the template polymorphic type variable and destroying
+      	   template polymorphism.
+      	   e.g. when typechecking nil : Π A : Type n, list A, we don't
+      	   want n to be used as the fixed carrier level of the list, so we
+      	   refresh it preemptively. *)
+      	let univs, ty = Evarutil.get_template_constructor_type evdref cstr (List.length args) in
+      	  univs, make_judge (mkConstruct cstr) ty
+      | _ -> [], pretype empty_tycon env evdref lvar f 
+    in
     let floc = loc_of_glob_constr f in
     let length = List.length args in
     let candargs =
@@ -514,7 +542,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 	      with Not_found -> []
       else []
     in
-    let rec apply_rec env n resj candargs = function
+    let rec apply_rec env n resj univs candargs = function
       | [] -> resj
       | c::rest ->
 	let argloc = loc_of_glob_constr c in
@@ -522,7 +550,15 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
         let resty = whd_betadeltaiota env !evdref resj.uj_type in
       	  match kind_of_term resty with
 	  | Prod (na,c1,c2) ->
-	    let hj = pretype (mk_tycon c1) env evdref lvar c in
+	    let univs, tycon = 
+	      match univs with
+	      | Some _ :: l -> 
+		if is_GHole c then
+		  l, Some (evd_comb1 (Evarsolve.refresh_universes ~with_globals:true true) evdref c1)
+		else l, (* Some c1 *) None
+	      | (None :: l) | l -> l, Some c1
+	    in
+	    let hj = pretype tycon env evdref lvar c in
 	    let candargs, ujval =
 	      match candargs with
 	      | [] -> [], j_val hj
@@ -535,15 +571,15 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 	      apply_rec env (n+1)
 		{ uj_val = value;
 		  uj_type = typ }
-		candargs rest
-
+		univs candargs rest
+		
 	  | _ ->
 	    let hj = pretype empty_tycon env evdref lvar c in
 	      error_cant_apply_not_functional_loc
 		(Loc.merge floc argloc) env !evdref
 	      	resj [hj]
     in
-    let resj = apply_rec env 1 fj candargs args in
+    let resj = apply_rec env 1 fj univs candargs args in
     let resj =
       match evar_kind_of_term !evdref resj.uj_val with
       | App (f,args) ->
@@ -553,7 +589,30 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 	    let c = mkApp (f,Array.map (whd_evar sigma) args) in
 	    let t = Retyping.get_type_of env sigma c in
 	      make_judge c (* use this for keeping evars: resj.uj_val *) t
-	  else resj
+	    (* else  *)
+	    (*   if is_template_polymorphic_constructor env f then *)
+	    (*     let ty = nf_evar !evdref resj.uj_type in *)
+	    (* 	if occur_existential resj.uj_type then *)
+	    (* 	(\* The type is not fully defined, e.g. list ?A where A : Type n  *)
+	    (* 	   for n the fixed template universe of lists. We don't want this *)
+	  (* 	   n to escape (e.g. by later taking typeof(list A) = Type n) when *)
+	  (* 	   instantiating other existentials. So we need to refresh the  *)
+	  (* 	   type of f and redo typechecking with this fresh type. *\) *)
+	  (* 	  match kind_of_term f with *)
+	  (* 	  | Construct ((ind, i as cstr,u)) -> *)
+	  (* 	  (\** We refresh the universes so as to enforce using <= instead of instantiating *)
+    	  (* 	      an unkwown ?X with the template polymorphic type variable and destroying *)
+    	  (* 	      template polymorphism. *)
+    	  (* 	      e.g. when typechecking nil : Π A : Type n, list A, we don't *)
+    	  (* 	      want n to be used as the fixed carrier level of the list, so we *)
+    	  (* 	      refresh it preemptively. *\) *)
+	  (* 	    evdref := initial_evd; *)
+	  (* 	    let ty = Evarutil.get_template_constructor_type evdref cstr in *)
+    	  (* 	    let fj = make_judge (mkConstruct cstr) ty in *)
+	  (* 	      typecheck_app fj *)
+	  (* 	  | _ -> assert false *)
+	  (* 	else make_judge resj.uj_val ty *)
+	    else resj
       | _ -> resj 
     in
       inh_conv_coerce_to_tycon loc env evdref resj tycon
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 9b5d7ffb08..c8d18f7661 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -153,10 +153,10 @@ Inductive option (A:Type) : Type :=
 
 Arguments None [A].
 
-Definition option_map (A B:Type) (f:A->B) o :=
+Definition option_map (A B:Type) (f:A->B) (o : option A) : option B :=
   match o with
-    | Some a => Some (f a)
-    | None => None
+    | Some a => @Some B (f a)
+    | None => @None B
   end.
 
 (** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *)
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 2062f38611..4850b3c4c9 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1892,7 +1892,7 @@ Inductive Forall2 A B (R:A->B->Prop) : list A -> list B -> Prop :=
 Hint Constructors Forall2.
 
 Theorem Forall2_refl : forall A B (R:A->B->Prop), Forall2 R [] [].
-Proof. exact Forall2_nil. Qed.
+Proof. intros; apply Forall2_nil. Qed.
 
 Theorem Forall2_app_inv_l : forall A B (R:A->B->Prop) l1 l2 l',
   Forall2 R (l1 ++ l2) l' ->
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index 5c232f3400..fb0d1ad9df 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -56,7 +56,7 @@ Module Ops (X:OrderedType) <: WOps X.
 
   Definition singleton (x : elt) := x :: nil.
 
-  Fixpoint remove x s :=
+  Fixpoint remove x s : t :=
     match s with
     | nil => nil
     | y :: l =>