Find a more efficient fix for dealing with template universes:

eagerly solve l <= k constraints as k := l when k is a fresh variable coming
from a template type. This has the effect of fixing the variable at the first
instantiation of the parameters of template polymorphic inductive and avoiding
to generate useless <= constraints that need to be minimized afterwards.

7 files changed, 54 insertions, 24 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index d931626e4..a9b511588 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -755,6 +755,10 @@ struct
 
     let pr x = str(to_string x)
 
+    let is_level = function
+      | (v, 0) -> true
+      | _ -> false
+
     let level = function
       | (v,0) -> Some v
       | _ -> None
@@ -809,6 +813,10 @@ struct
     | Cons (l, n) when is_nil n -> Some l
     | _ -> None
 
+  let is_level l = match node l with
+    | Cons (l, n) when is_nil n -> Expr.is_level l
+    | _ -> false
+
   let level l = match node l with
     | Cons (l, n) when is_nil n -> Expr.level l
     | _ -> None
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 20ee554f1..cc5eedefb 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -118,6 +118,9 @@ sig
   val pr : t -> Pp.std_ppcmds
   (** Pretty-printing *)
 
+  val is_level : t -> bool
+  (** Test if the universe is a level or an algebraic universe. *)
+
   val level : t -> Level.t option
   (** Try to get a level out of a universe, returns [None] if it
       is an algebraic universe. *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 16a044528..8f696b84c 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -26,7 +26,7 @@ let normalize_evar evd ev =
   | Evar (evk,args) -> (evk,args)
   | _ -> assert false
 
-let refresh_universes ?(all=false) ?(with_globals=false) dir evd t =
+let refresh_universes ?(all=false) ?(template=false) ?(with_globals=false) dir evd t =
   let evdref = ref evd in
   let modified = ref false in
   let rec refresh dir t = match kind_of_term t with
@@ -34,7 +34,7 @@ let refresh_universes ?(all=false) ?(with_globals=false) dir evd t =
 			 || (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
+       let s' = evd_comb0 (new_sort_variable ~template Evd.univ_flexible) evdref in
 	 evdref :=
 	   (if dir then set_leq_sort !evdref s' s else
 	     set_leq_sort !evdref s s');
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index ca03f9853..23ed6a2ef 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -35,6 +35,7 @@ val evar_define : conv_fun -> ?choose:bool -> ?dir:bool -> env -> evar_map ->
   bool option -> existential -> constr -> evar_map
 
 val refresh_universes : ?all:bool (* Include domains of products *) -> 
+  ?template:bool -> (* Generate template fresh universe variables, to be instantiated eagerly *) 
   ?with_globals:bool -> bool -> evar_map -> types -> evar_map * types
 
 val solve_refl : ?can_drop:bool -> conv_fun_bool -> env ->  evar_map ->
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 652bed5a3..1bd995d5d 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -268,6 +268,7 @@ type evar_universe_context =
     uctx_univ_variables : Universes.universe_opt_subst;
       (** The local universes that are unification variables *)
     uctx_univ_algebraic : Univ.universe_set; 
+    uctx_univ_template : Univ.universe_set; 
     (** The subset of unification variables that
 	can be instantiated with algebraic universes as they appear in types 
 	and universe instances only. *)
@@ -279,6 +280,7 @@ let empty_evar_universe_context =
   { uctx_local = Univ.ContextSet.empty;
     uctx_univ_variables = Univ.LMap.empty;
     uctx_univ_algebraic = Univ.LSet.empty;
+    uctx_univ_template = Univ.LSet.empty;
     uctx_universes = Univ.initial_universes;
     uctx_initial_universes = Univ.initial_universes }
 
@@ -305,6 +307,8 @@ let union_evar_universe_context ctx ctx' =
 	  Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
 	uctx_univ_algebraic = 
 	  Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic;
+	uctx_univ_template = 
+	  Univ.LSet.union ctx.uctx_univ_template ctx'.uctx_univ_template;
 	uctx_initial_universes = ctx.uctx_initial_universes;
 	uctx_universes = 
 	  if local == ctx.uctx_local then ctx.uctx_universes
@@ -325,6 +329,8 @@ let diff_evar_universe_context ctx' ctx  =
 	  Univ.LMap.diff ctx'.uctx_univ_variables ctx.uctx_univ_variables;
 	uctx_univ_algebraic = 
 	  Univ.LSet.diff ctx'.uctx_univ_algebraic ctx.uctx_univ_algebraic;
+	uctx_univ_template = 
+	  Univ.LSet.diff ctx'.uctx_univ_template ctx.uctx_univ_template;
 	uctx_universes = Univ.empty_universes;
 	uctx_initial_universes = ctx.uctx_initial_universes }
 
@@ -348,7 +354,7 @@ let instantiate_variable l b v =
 
 exception UniversesDiffer
 
-let process_universe_constraints univs vars alg local cstrs =
+let process_universe_constraints univs vars alg templ local cstrs =
   let vars = ref vars in
   let normalize = Universes.normalize_universe_opt_subst vars in
   let rec unify_universes fo l d r local =
@@ -372,13 +378,17 @@ let process_universe_constraints univs vars alg local cstrs =
 	    else
 	      match Univ.Universe.level r with
 	      | None -> error ("Algebraic universe on the right")
-	      | Some rl when Univ.Level.is_small rl -> 
-		(if Univ.LSet.for_all (fun l -> 
-		  Univ.Level.is_small l || Univ.LMap.mem l !vars) 
-		    (Univ.Universe.levels l) then
-		    Univ.enforce_leq l r local
-		 else raise (Univ.UniverseInconsistency (Univ.Le, l, r, [])))
-	      | _ -> Univ.enforce_leq l r local
+	      | Some rl ->
+		if Univ.Level.is_small rl then
+		  (if Univ.LSet.for_all (fun l -> 
+		    Univ.Level.is_small l || Univ.LMap.mem l !vars) 
+		      (Univ.Universe.levels l) then
+		      Univ.enforce_leq l r local
+		   else raise (Univ.UniverseInconsistency (Univ.Le, l, r, [])))
+		else if Univ.LSet.mem rl templ && Univ.Universe.is_level l then
+		  unify_universes fo l Univ.UEq r local
+		else
+		  Univ.enforce_leq l r local
 	  else if d == Univ.ULub then
 	    match varinfo l, varinfo r with
 	    | (Inr (l, true, _), Inr (r, _, _)) 
@@ -393,9 +403,9 @@ let process_universe_constraints univs vars alg local cstrs =
 	    | Inr (l', lloc, _), Inr (r', rloc, _) ->
 	      let () = 
 		if lloc then
-		  instantiate_variable l' (Univ.Universe.make r') vars
+		  instantiate_variable l' r vars
 		else if rloc then 
-		  instantiate_variable r' (Univ.Universe.make l') vars
+		  instantiate_variable r' l vars
 		else if not (Univ.check_eq univs l r) then
 		  (* Two rigid/global levels, none of them being local,
 		     one of them being Prop/Set, disallow *)
@@ -430,7 +440,7 @@ let add_constraints_context ctx cstrs =
   let vars, local' =
     process_universe_constraints ctx.uctx_universes
       ctx.uctx_univ_variables ctx.uctx_univ_algebraic
-      local cstrs'
+      ctx.uctx_univ_template local cstrs'
   in
     { ctx with uctx_local = (univs, Univ.Constraint.union local local');
       uctx_univ_variables = vars;
@@ -443,7 +453,8 @@ let add_universe_constraints_context ctx cstrs =
   let univs, local = ctx.uctx_local in
   let vars, local' = 
     process_universe_constraints ctx.uctx_universes 
-      ctx.uctx_univ_variables ctx.uctx_univ_algebraic local cstrs 
+      ctx.uctx_univ_variables ctx.uctx_univ_algebraic 
+      ctx.uctx_univ_template local cstrs 
   in
     { ctx with uctx_local = (univs, Univ.Constraint.union local local');
       uctx_univ_variables = vars;
@@ -948,7 +959,7 @@ let merge_universe_subst evd subst =
 let with_context_set rigid d (a, ctx) = 
   (merge_context_set rigid d ctx, a)
 
-let uctx_new_univ_variable rigid 
+let uctx_new_univ_variable template rigid 
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
   let u = Universes.new_univ_level (Global.current_dirpath ()) in
   let ctx' = Univ.ContextSet.union ctx (Univ.ContextSet.singleton u) in
@@ -960,14 +971,18 @@ let uctx_new_univ_variable rigid
 	if b then {uctx with uctx_univ_variables = uvars';
 	  uctx_univ_algebraic = Univ.LSet.add u avars}
 	else {uctx with uctx_univ_variables = Univ.LMap.add u None uvars} in
-    {uctx' with uctx_local = ctx'}, u
+  let uctx'' = if template then 
+      {uctx' with uctx_univ_template = Univ.LSet.add u uctx'.uctx_univ_template}
+    else uctx'
+  in
+    {uctx'' with uctx_local = ctx'}, u
 
-let new_univ_variable rigid evd =
-  let uctx', u = uctx_new_univ_variable rigid evd.universes in
+let new_univ_variable ?(template=false) rigid evd =
+  let uctx', u = uctx_new_univ_variable template rigid evd.universes in
     ({evd with universes = uctx'}, Univ.Universe.make u)
 
-let new_sort_variable rigid d =
-  let (d', u) = new_univ_variable rigid d in
+let new_sort_variable ?(template=false) rigid d =
+  let (d', u) = new_univ_variable ~template rigid d in
     (d', Type u)
 
 let make_flexible_variable evd b u =
@@ -1189,6 +1204,7 @@ let refresh_undefined_univ_variables uctx =
   in 
   let uctx' = {uctx_local = ctx'; 
 	       uctx_univ_variables = vars; uctx_univ_algebraic = alg;
+	       uctx_univ_template = uctx.uctx_univ_template;
 	       uctx_universes = Univ.initial_universes;
 	       uctx_initial_universes = uctx.uctx_initial_universes } in
     uctx', subst
@@ -1222,6 +1238,7 @@ let normalize_evar_universe_context uctx =
 	  { uctx_local = us'; 
 	    uctx_univ_variables = vars'; 
 	    uctx_univ_algebraic = algs';
+	    uctx_univ_template = uctx.uctx_univ_template;
 	    uctx_universes = universes;
 	    uctx_initial_universes = uctx.uctx_initial_universes }
 	in fixpoint uctx'
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 5cc554c26..fb348ae22 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -435,8 +435,8 @@ val normalize_evar_universe_context_variables : evar_universe_context ->
 val normalize_evar_universe_context : evar_universe_context -> 
   evar_universe_context
 
-val new_univ_variable : rigid -> evar_map -> evar_map * Univ.universe
-val new_sort_variable : rigid -> evar_map -> evar_map * sorts
+val new_univ_variable : ?template:bool -> rigid -> evar_map -> evar_map * Univ.universe
+val new_sort_variable : ?template:bool -> rigid -> evar_map -> evar_map * sorts
 val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
 val is_sort_variable : evar_map -> sorts -> (Univ.universe_level * bool) option 
 (** [is_sort_variable evm s] returns [Some (u, is_rigid)] or [None] if [s] is 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7cb3fa1a8..add47e5b7 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -554,8 +554,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 	      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
+		  l, Some (evd_comb1 (Evarsolve.refresh_universes ~template:true
+					~with_globals:true true) evdref c1)
+		else l, Some c1
 	      | (None :: l) | l -> l, Some c1
 	    in
 	    let hj = pretype tycon env evdref lvar c in