Try a new way of handling template universe levels

1 files changed, 74 insertions, 15 deletions

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