Change interface of refresh universes to get a pbty argument instead of

the computed direction argument. In case pbty is conv, no refreshing is done
as the evar body must be convertible with the given term, however refreshing
of template application evar arguments can still happen.
(Re)-Closing bug #2966.

7 files changed, 23 insertions, 16 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 50396d854..3f1bead36 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1559,7 +1559,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
         map_constr_with_full_binders push_binder aux x t
     | Evar ev ->
         let ty = get_type_of env sigma t in
-	let ty = Evarutil.evd_comb1 (refresh_universes false env) evdref ty in
+	let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in
         let inst =
 	  List.map_i
 	    (fun i _ ->
@@ -1577,7 +1577,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
       let vl = List.map pi1 good in
       let ty = 
 	let ty = get_type_of env !evdref t in
-	  Evarutil.evd_comb1 (refresh_universes false env) evdref ty
+	  Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty
       in
       let ty = lift (-k) (aux x ty) in
       let depvl = free_rels ty in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 9522f9c24..13421bcde 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -42,7 +42,12 @@ let get_polymorphic_positions f =
         templ.template_param_levels)
   | _ -> assert false
 
-let refresh_universes ?(onlyalg=false) dir env evd t =
+(**
+   forall A (l : list A) -> typeof A = Type i <= Datatypes.j -> i not refreshed
+   hd ?A (l : list t) -> A = t
+
+*)
+let refresh_universes ?(onlyalg=false) pbty env evd t =
   let evdref = ref evd in
   let modified = ref false in
   let rec refresh dir t = 
@@ -88,7 +93,10 @@ let refresh_universes ?(onlyalg=false) dir env evd t =
     in aux 0 pos
   in
   let t' = 
-    if isArity t then refresh dir t 
+    if isArity t then
+      (match pbty with
+      | None -> t
+      | Some dir -> refresh dir t)
     else (refresh_term_evars false t; t)
   in
     if !modified then !evdref, t' else !evdref, t
@@ -553,7 +561,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
       let id = next_name_away na avoid in
       let evd,t_in_sign =
         let s = Retyping.get_sort_of env evd t_in_env in
-        let evd,ty_t_in_sign = refresh_universes false env evd (mkSort s) in
+        let evd,ty_t_in_sign = refresh_universes (Some false) env evd (mkSort s) in
         define_evar_from_virtual_equation define_fun env evd t_in_env 
           ty_t_in_sign sign filter inst_in_env in
       let evd,b_in_sign = match b with
@@ -572,7 +580,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   in
   let evd,ev2ty_in_sign =
     let s = Retyping.get_sort_of env evd ty_in_env in
-    let evd,ty_t_in_sign = refresh_universes false env evd (mkSort s) in
+    let evd,ty_t_in_sign = refresh_universes (Some false) env evd (mkSort s) in
     define_evar_from_virtual_equation define_fun env evd ty_in_env
       ty_t_in_sign sign2 filter2 inst2_in_env in
   let evd,ev2_in_sign =
@@ -1417,7 +1425,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
  * context "hyps" and not referring to itself.
  *)
 
-and evar_define conv_algo ?(choose=false) ?(dir=false) env evd pbty (evk,argsv as ev) rhs =
+and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
   match kind_of_term rhs with
   | Evar (evk2,argsv2 as ev2) ->
       if Evar.equal evk evk2 then
@@ -1436,7 +1444,7 @@ and evar_define conv_algo ?(choose=false) ?(dir=false) env evd pbty (evk,argsv a
     (* so we recheck acyclicity *)
     if occur_evar evk body then raise (OccurCheckIn (evd',body));
     (* needed only if an inferred type *)
-    let evd', body = refresh_universes dir env evd' body in
+    let evd', body = refresh_universes pbty env evd' body in
 (* Cannot strictly type instantiations since the unification algorithm
  * does not unify applications from left to right.
  * e.g problem f x == g y yields x==y and f==g (in that order)
@@ -1520,8 +1528,7 @@ let reconsider_conv_pbs conv_algo evd =
 let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
   try
     let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
-    let dir = match pbty with Some d -> d | None -> false in
-    let evd = evar_define conv_algo ~choose ~dir env evd pbty ev1 t2 in
+    let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in
       reconsider_conv_pbs conv_algo evd
   with
     | NotInvertibleUsingOurAlgorithm t ->
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 6de8f5c8d..16a4aff5b 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -31,11 +31,11 @@ type conv_fun =
 type conv_fun_bool =
   env ->  evar_map -> conv_pb -> constr -> constr -> bool
 
-val evar_define : conv_fun -> ?choose:bool -> ?dir:bool -> env -> evar_map -> 
+val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> 
   bool option -> existential -> constr -> evar_map
 
 val refresh_universes : ?onlyalg:bool (* Only algebraic universes *) ->
-  bool (* direction: true for levels lower than the existing levels *) ->
+  bool option (* direction: true for levels lower than the existing levels *) ->
   env -> evar_map -> types -> evar_map * types
 
 val solve_refl : ?can_drop:bool -> conv_fun_bool -> env ->  evar_map ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 27abdbade..6d7403031 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -595,7 +595,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 	       refreshed right away. *)
 	    let sigma = !evdref in
 	    let c = mkApp (f,Array.map (whd_evar sigma) args) in
-	    let c = evd_comb1 (Evarsolve.refresh_universes true env) evdref c in
+	    let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env) evdref c in
 	    let t = Retyping.get_type_of env !evdref c in
 	      make_judge c (* use this for keeping evars: resj.uj_val *) t
 	  else resj
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 1c41a5bb3..92bdd35ec 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -290,7 +290,7 @@ let e_type_of ?(refresh=false) env evd c =
   let j = execute env evdref c in
   (* side-effect on evdref *)
     if refresh then
-      Evarsolve.refresh_universes ~onlyalg:true false env !evdref j.uj_type
+      Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type
     else !evdref, j.uj_type
 
 let solve_evars env evdref c =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 300eb6dc6..219d03b9e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -936,7 +936,7 @@ let w_coerce env evd mv c =
   w_coerce_to_type env evd c cty mvty
 
 let unify_to_type env sigma flags c status u =
-  let sigma, c = refresh_universes false env sigma c in
+  let sigma, c = refresh_universes (Some false) env sigma c in
   let t = get_type_of env sigma (nf_meta sigma c) in
   let t = nf_betaiota sigma (nf_meta sigma t) in
     unify_0 env sigma CUMUL flags t u
diff --git a/test-suite/bugs/closed/2966.v b/test-suite/bugs/closed/2966.v
index e1c8d0047..debada853 100644
--- a/test-suite/bugs/closed/2966.v
+++ b/test-suite/bugs/closed/2966.v
@@ -7,7 +7,7 @@ Set Asymmetric Patterns.
 Module MemSig.
   Definition t: Type := list Type.
   
-  Definition Nth (sig: t) (n: nat): Type :=
+  Definition Nth (sig: t) (n: nat) :=
     nth n sig unit.
 End MemSig.