A try at using sort variables during unification. Instead of refreshing

universes as usual, we add the new universes to the sort constraints and
do unification modulo those ([constr_unify_with_sorts]): this allows to
instanciate Type i with Prop for example and keep track of it. The sort 
constraints are thrown away at the end of unification for the moment, 
but we can detect inconsistencies during unification.
Make unification more symmetric as well w.r.t. substitution of defined
metas.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12137 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 170 insertions, 84 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index dd2af306c..695d93ca8 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -73,7 +73,8 @@ let clenv_push_prod cl =
 	let mv = new_meta () in
 	let dep = dependent (mkRel 1) u in
 	let na' = if dep then na else Anonymous in
-	let e' = meta_declare mv t ~name:na' cl.evd in
+	let evd,t' = Evd.universes_to_variables cl.evd t in
+	let e' = meta_declare mv t' ~name:na' evd in
 	let concl = if dep then subst1 (mkMeta mv) u else u in
 	let def = applist (cl.templval.rebus,[mkMeta mv]) in
 	{ templval = mk_freelisted def;
@@ -95,7 +96,8 @@ let clenv_environments evd bound t =
 	  let mv = new_meta () in
 	  let dep = dependent (mkRel 1) t2 in
 	  let na' = if dep then na else Anonymous in
-	  let e' = meta_declare mv t1 ~name:na' e in
+	  let e',t1' = Evd.universes_to_variables e t1 in
+	  let e' = meta_declare mv t1' ~name:na' e' in
 	  clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
 	    (if dep then (subst1 (mkMeta mv) t2) else t2)
       | (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t)
@@ -112,7 +114,8 @@ let clenv_environments_evars env evd bound t =
       | (Some 0, _) -> (e, List.rev ts, t)
       | (n, Cast (t,_,_)) -> clrec (e,ts) n t
       | (n, Prod (na,t1,t2)) ->
-          let e',constr = Evarutil.new_evar e env t1 in
+	  let e',t1' = Evd.universes_to_variables e t1 in
+          let e',constr = Evarutil.new_evar e' env t1' in
 	  let dep = dependent (mkRel 1) t2 in
 	  clrec (e', constr::ts) (Option.map ((+) (-1)) n)
 	    (if dep then (subst1 constr t2) else t2)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d6b10b7d0..352b76dd9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -24,6 +24,31 @@ open Evarutil
 open Libnames
 open Evd
 
+let base_sort_conv evd pb s0 s1 =
+  match (s0,s1) with
+    | (Prop c1, Prop c2) -> if c1 = Null or c2 = Pos then Some evd else None (* Prop <= Set *)
+    | (Prop c1, Type u)  -> if pb = Reduction.CUMUL then Some evd else None
+    | (Type u, Prop c)   -> 
+	if Evd.is_sort_variable evd s0 then
+	  Some (Evd.define_sort_variable evd s0 s1)
+	else None
+    | (Type u1, Type u2) -> Some evd
+
+let unify_constr_univ evd f cv_pb t1 t2 = 
+  match kind_of_term t1, kind_of_term t2 with
+      Sort s1, Sort s2 -> 
+	(match base_sort_conv !evd cv_pb s1 s2 with
+	| Some evd' -> evd := evd'; true
+	| None -> false)
+    | Prod (_,t1,c1), Prod (_,t2,c2) -> 
+	f Reduction.CONV t1 t2 & f cv_pb c1 c2
+    | _ -> compare_constr (f Reduction.CONV) t1 t2
+
+let constr_unify_with_sorts evd cv_pb t1 t2 = 
+  let evdref = ref evd in
+  let rec aux cv_pb t1 t2 = unify_constr_univ evdref aux cv_pb t1 t2 in
+    if aux cv_pb t1 t2 then true, !evdref else false, evd
+
 type flex_kind_of_term =
   | Rigid of constr 
   | MaybeFlexible of constr
@@ -376,8 +401,10 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	| _, Cast (c2,_,_) -> evar_eqappr_x env evd pbty appr1 (c2,l2)
 
 	| Sort s1, Sort s2 when l1=[] & l2=[] ->
-            (evd,base_sort_cmp pbty s1 s2)
-
+	    (match base_sort_conv evd pbty s1 s2 with
+	    | Some evd' -> evd',true
+	    | None -> evd, false)
+	      
 	| Lambda (na,c1,c'1), Lambda (_,c2,c'2) when l1=[] & l2=[] -> 
             ise_and evd
               [(fun i -> evar_conv_x env i CONV c1 c2);
@@ -542,11 +569,11 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 =
 
 let consider_remaining_unif_problems env evd =
   let (evd,pbs) = extract_all_conv_pbs evd in
-  List.fold_left
-    (fun (evd,b as p) (pbty,env,t1,t2) ->
-      if b then apply_conversion_problem_heuristic env evd pbty t1 t2 else p)
-    (evd,true)
-    pbs
+    List.fold_left
+      (fun (evd,b as p) (pbty,env,t1,t2) ->
+	if b then apply_conversion_problem_heuristic env evd pbty t1 t2 else p)
+      (evd,true)
+      pbs
 
 (* Main entry points *)
 
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index a281a3898..2a2cd5271 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -16,6 +16,10 @@ open Reductionops
 open Evd
 (*i*)
 
+(* Comparison function considering sort variables. *)
+val constr_unify_with_sorts : evar_defs -> conv_pb ->
+  types -> types -> bool * evar_defs
+
 (* returns exception Reduction.NotConvertible if not unifiable *)
 val the_conv_x     : env -> constr -> constr -> evar_defs -> evar_defs
 val the_conv_x_leq : env -> constr -> constr -> evar_defs -> evar_defs
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index e7682285b..8e9ddf1ba 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -947,22 +947,22 @@ and evar_define ?(choose=false) env (evk,_ as ev) rhs evd =
 (* Auxiliary functions for the conversion algorithms modulo evars
  *)
 
-let has_undefined_evars evd t =
-  let evm =  evd in
+let has_undefined_evars_or_sorts evd t =
   let rec has_ev t =
     match kind_of_term t with
-        Evar (ev,args) ->
-          (match evar_body (Evd.find evm ev) with
-            | Evar_defined c ->
-                has_ev c; Array.iter has_ev args
-            | Evar_empty ->
-	        raise NotInstantiatedEvar)
-      | _ -> iter_constr has_ev t in
+    | Evar (ev,args) ->
+        (match evar_body (Evd.find evd ev) with
+        | Evar_defined c ->
+            has_ev c; Array.iter has_ev args
+        | Evar_empty ->
+	    raise NotInstantiatedEvar)
+    | Sort s when is_sort_variable evd s -> raise Not_found
+    | _ -> iter_constr has_ev t in
   try let _ = has_ev t in false
   with (Not_found | NotInstantiatedEvar) -> true
 
 let is_ground_term evd t =
-  not (has_undefined_evars evd t)
+  not (has_undefined_evars_or_sorts evd t)
 
 let is_ground_env evd env =
   let is_ground_decl = function
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 500e19002..79cdc7da5 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -184,9 +184,13 @@ type sort_constraints = sort_constraint UniverseMap.t
 
 let rec canonical_find u scstr =
   match UniverseMap.find u scstr with
-      EqSort u' -> canonical_find u' scstr
-    | c -> (u,c)
+  | EqSort u' -> canonical_find u' scstr
+  | c -> (u,c)
 
+let find_univ u scstr =
+  try canonical_find u scstr
+  with Not_found -> u, DefinedSort (Type u)
+    
 let whd_sort_var scstr t =
   match kind_of_term t with
       Sort(Type u) ->
@@ -238,7 +242,6 @@ let new_sort_var cstr =
   let u = Termops.new_univ() in
   (u, UniverseMap.add u (SortVar([],[])) cstr)
 
-
 let set_leq_sort (u1,(leq1,geq1)) (u2,(leq2,geq2)) scstr =
   let rec search_rec (is_b, betw, not_betw) u1 =
     if List.mem u1 betw then (true, betw, not_betw)
@@ -264,8 +267,8 @@ let set_leq_sort (u1,(leq1,geq1)) (u2,(leq2,geq2)) scstr =
 let set_leq s1 s2 scstr =
   let u1 = var_of_sort s1 in
   let u2 = var_of_sort s2 in
-  let (cu1,c1) = canonical_find u1 scstr in
-  let (cu2,c2) = canonical_find u2 scstr in
+  let (cu1,c1) = find_univ u1 scstr in
+  let (cu2,c2) = find_univ u2 scstr in
   if cu1=cu2 then scstr
   else
     match c1,c2 with
@@ -315,8 +318,11 @@ module EvarMap = struct
   let eq_evar_map x y = x == y ||
     (EvarInfoMap.equal eq_evar_info (fst x) (fst y) &&
       UniverseMap.equal (=) (snd x) (snd y))
-
-  let merge e e' = fold (fun n v sigma -> add sigma n v) e' e
+  let constraints (sigma,sm) = sm
+  let merge (sigma,sm) (sigma',sm') = 
+    let ev = EvarInfoMap.fold (fun n v sigma -> EvarInfoMap.add sigma n v) sigma' sigma in
+    let sm = UniverseMap.fold (fun u cstr sm -> UniverseMap.add u cstr sm) sm' sm in
+      (ev,sm)
   
 end
  
@@ -479,11 +485,10 @@ let subst_evar_info s evi =
       evar_body = subst_evb evi.evar_body }
 
 let subst_evar_defs_light sub evd =
-  assert (UniverseMap.is_empty (snd evd.evars));
   assert (evd.conv_pbs = []);
   { evd with
-      metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
-      evars = ExistentialMap.map (subst_evar_info sub)  (fst evd.evars), snd evd.evars
+    metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
+    evars = ExistentialMap.map (subst_evar_info sub)  (fst evd.evars), (snd evd.evars);
   }
 
 let subst_evar_map = subst_evar_defs_light
@@ -572,6 +577,9 @@ let extract_changed_conv_pbs evd p =
 let extract_all_conv_pbs evd =
   extract_conv_pbs evd (fun _ -> true)
 
+let solve_sort_cstrs cstrs = (* TODO: Check validity *)
+  UniverseMap.empty
+
 (* spiwack: should it be replaced by Evd.merge? *)
 let evar_merge evd evars =
   { evd with evars = EvarMap.merge evd.evars evars.evars }
@@ -590,6 +598,30 @@ let set_leq_sort_variable ({evars=(sigma,sm)}as d) u1 u2 =
 let define_sort_variable ({evars=(sigma,sm)}as d) u s =
   { d with evars = (sigma, set_sort_variable u s sm) }
 let pr_sort_constraints {evars=(_,sm)} = pr_sort_cstrs sm
+let solve_sort_constraints ({evars=(sigma,sm)} as d) =
+  { d with evars = (sigma, solve_sort_cstrs sm) }
+
+(* This refreshes universes in types introducing sort variables;
+   works only for inferred types (i.e. for
+   types of the form (x1:A1)...(xn:An)B with B a sort or an atom in
+   head normal form) *)
+let universes_to_variables_gen strict evd t =
+  let modified = ref false in
+  let evdref = ref evd in
+  let rec refresh t = match kind_of_term t with
+    | Sort (Type u as us) when strict or u <> Univ.type0m_univ ->
+(* 	if Univ.is_univ_variable u then  *)
+	  let s', evd = new_sort_variable !evdref in
+	  let evd = set_leq_sort_variable evd s' us in
+	    evdref := evd; modified := true; mkSort s'
+(* 	else t *)
+    | Prod (na,u,v) -> mkProd (na,u,refresh v)
+    | _ -> t in
+  let t' = refresh t in
+  if !modified then !evdref, t' else evd, t
+
+let universes_to_variables = universes_to_variables_gen false
+let universes_to_variables_strict = universes_to_variables_gen true
 
 (**********************************************************)
 (* Accessing metas *)
@@ -764,10 +796,12 @@ let pr_meta_map mmap =
       	hov 0 
 	  (pr_meta mv ++ pr_name na ++ str " : " ++
            print_constr b.rebus ++ fnl ())
-    | (mv,Clval(na,(b,s),_)) ->
+    | (mv,Clval(na,(b,s),t)) ->
       	hov 0 
 	  (pr_meta mv ++ pr_name na ++ str " := " ++
-           print_constr b.rebus ++ spc () ++ pr_instance_status s ++ fnl ())
+           print_constr b.rebus ++ 
+	   str " : " ++ print_constr t.rebus ++
+	   spc () ++ pr_instance_status s ++ fnl ())
   in
   prlist pr_meta_binding (metamap_to_list mmap)
 
@@ -788,12 +822,19 @@ let pr_evar_info evi =
   in
   hov 2 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]")
 
-let pr_evar_defs_t sigma =
-  h 0 
-    (prlist_with_sep pr_fnl
-      (fun (ev,evi) ->
-        h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
-      (EvarMap.to_list sigma))
+let pr_evar_defs_t (evars,cstrs as sigma) =
+  let evs = 
+    if evars = EvarInfoMap.empty then mt ()
+    else
+      str"EVARS:"++brk(0,1)++
+	h 0 (prlist_with_sep pr_fnl
+		(fun (ev,evi) ->
+		  h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
+		(EvarMap.to_list sigma))++fnl()
+  and cs =
+    if cstrs = UniverseMap.empty then mt ()
+    else pr_sort_cstrs cstrs++fnl() 
+  in evs ++ cs
 
 let pr_constraints pbs =
   h 0
@@ -807,7 +848,7 @@ let pr_constraints pbs =
 let pr_evar_defs evd =
   let pp_evm =
     if evd.evars = EvarMap.empty then mt() else
-      str"EVARS:"++brk(0,1)++pr_evar_defs_t evd.evars++fnl() in
+      pr_evar_defs_t evd.evars++fnl() in
   let cstrs =
     if evd.conv_pbs = [] then mt() else
     str"CONSTRAINTS:"++brk(0,1)++pr_constraints evd.conv_pbs++fnl() in
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index e5cf8e269..a26c2dadc 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -241,6 +241,9 @@ val is_sort_variable : evar_defs -> sorts -> bool
 val whd_sort_variable : evar_defs -> constr -> constr
 val set_leq_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
 val define_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
+val solve_sort_constraints : evar_defs -> evar_defs
+
+val universes_to_variables : evar_defs -> types -> evar_defs * types
 
 (*********************************************************************)
 (* constr with holes *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index eeee0c313..b16508053 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -161,8 +161,10 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
 
 (* We are outside the kernel: we take fresh universes *)
 (* to avoid tactics and co to refresh universes themselves *)
-let get_type_of env sigma c =
-  let f,_,_,_ = retype sigma in refresh_universes (f env c)
+let get_type_of ?(refresh=true) env sigma c =
+  let f,_,_,_ = retype sigma in
+  let t = f env c in
+    if refresh then refresh_universes t else t
 
 (* Makes an assumption from a constr *)
 let get_assumption_of env evc c = c
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index be42fd858..9b65494c1 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -21,7 +21,7 @@ open Environ
    either produces a wrong result or raise an anomaly. Use with care.
    It doesn't handle predicative universes too. *)
 
-val get_type_of : env -> evar_map -> constr -> types
+val get_type_of : ?refresh:bool -> env -> evar_map -> constr -> types
 val get_sort_of : env -> evar_map -> types -> sorts
 val get_sort_family_of : env -> evar_map -> types -> sorts_family
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 83c7b8370..48c8d6584 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -55,6 +55,10 @@ let abstract_list_all env evd typ c l =
 
 (**)
 
+let get_type_of_with_variables env evd c =
+  let t = Retyping.get_type_of ~refresh:false env evd c in
+    Evd.universes_to_variables evd t
+
 (* A refinement of [conv_pb]: the integers tells how many arguments
    were applied in the context of the conversion problem; if the number
    is non zero, steps of eta-expansion will be allowed
@@ -170,19 +174,24 @@ let oracle_order env cf1 cf2 =
       match cf2 with
       | None -> Some true
       | Some k2 -> Some (Conv_oracle.oracle_order k1 k2)
-	    
+
+let is_trans_fconv_pb pb flags env sigma m n =
+  match pb with
+  | Cumul -> is_trans_fconv CUMUL flags env sigma m n
+  | ConvUnderApp _ -> is_trans_fconv CONV flags env sigma m n
+
 let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n =
   let trivial_unify curenv pb (sigma,metasubst,_) m n =
     let subst = if flags.use_metas_eagerly then metasubst else ms in
-    match subst_defined_metas subst m with
-    | Some m1 ->
+    match subst_defined_metas subst m, subst_defined_metas subst n with
+    | Some m1, Some n1 ->
 	if (match flags.modulo_conv_on_closed_terms with
 	    Some flags ->
-	      is_trans_fconv (conv_pb_of pb) flags env sigma m1 n
+	      is_trans_fconv_pb pb flags env sigma m1 n1
 	  | None -> false) then true else
-        if (not (is_ground_term (create_evar_defs sigma) m1))
-            || occur_meta_or_existential n then false else
-               error_cannot_unify curenv sigma (m, n)
+	  let evd = create_evar_defs sigma in
+            if not (is_ground_term evd m1) || not (is_ground_term evd n1)
+	    then false else error_cannot_unify curenv sigma (m, n)
     | _ -> false in
   let rec unirec_rec (curenv,nb as curenvnb) pb b ((sigma,metasubst,evarsubst) as substn) curm curn =
     let cM = Evarutil.whd_castappevar sigma curm
@@ -261,12 +270,14 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	| _ ->
 	    try canonical_projections curenvnb pb b cM cN substn
 	    with ex when precatchable_exception ex ->
-              if constr_cmp (conv_pb_of cv_pb) cM cN then substn else
-		let (f1,l1) = 
-		  match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in
-		let (f2,l2) =
-		  match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in
-		  expand curenvnb pb b substn cM f1 l1 cN f2 l2
+              let (unif,sigma') = Evarconv.constr_unify_with_sorts sigma (conv_pb_of cv_pb) cM cN in
+		if unif then (sigma',metasubst,evarsubst)
+		else
+		  let (f1,l1) = 
+		    match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in
+		  let (f2,l2) =
+		    match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in
+		    expand curenvnb pb b substn cM f1 l1 cN f2 l2
 
   and expand (curenv,_ as curenvnb) pb b (sigma, _, _ as substn) cM f1 l1 cN f2 l2 =
     if trivial_unify curenv pb substn cM cN then substn
@@ -350,19 +361,19 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
       unirec_rec curenvnb pb b substn c1 (applist (c,(List.rev ks)))
 
   in
-    if (if occur_meta m then false else
-       if (match flags.modulo_conv_on_closed_terms with
-	  Some flags ->
-	    is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n
-	| None -> constr_cmp (conv_pb_of cv_pb) m n) then true else
+    if (if occur_meta m || occur_meta n then false else
+      if (match flags.modulo_conv_on_closed_terms with
+      | Some flags ->
+	  is_trans_fconv_pb cv_pb flags env sigma m n
+      | None -> fst (Evarconv.constr_unify_with_sorts sigma (conv_pb_of cv_pb) m n)) then true else
       if (not (is_ground_term (create_evar_defs sigma) m))
-          || occur_meta_or_existential n then false else
-      if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
-            | Some (cv_id, cv_k), (dl_id, dl_k) ->
-                Idpred.subset dl_id cv_id && Cpred.subset dl_k cv_k
-            | None,(dl_id, dl_k) ->
-                Idpred.is_empty dl_id && Cpred.is_empty dl_k)
-      then error_cannot_unify env sigma (m, n) else false) 
+        || occur_meta_or_existential n then false else
+	if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
+        | Some (cv_id, cv_k), (dl_id, dl_k) ->
+            Idpred.subset dl_id cv_id && Cpred.subset dl_k cv_k
+        | None,(dl_id, dl_k) ->
+            Idpred.is_empty dl_id && Cpred.is_empty dl_k)
+	then error_cannot_unify env sigma (m, n) else false) 
     then subst
     else 
       unirec_rec (env,0) cv_pb conv_at_top subst m n
@@ -541,13 +552,12 @@ let w_coerce_to_type env evd c cty mvty =
     try_to_coerce env evd c cty tycon
 
 let w_coerce env evd mv c =
-  let cty = get_type_of env evd c in
+  let evd,cty = get_type_of_with_variables env evd c in
   let mvty = Typing.meta_type evd mv in
   w_coerce_to_type env evd c cty mvty
 
 let unify_to_type env sigma flags c status u =
-  let c = refresh_universes c in
-  let t = get_type_of env sigma c in
+  let sigma, t = get_type_of_with_variables env sigma c in
   let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta sigma t)) in
   let u = Tacred.hnf_constr env sigma u in
     if status = IsSuperType then
@@ -561,9 +571,9 @@ let unify_to_type env sigma flags c status u =
 
 let unify_type env sigma flags mv status c =
   let mvty = Typing.meta_type sigma mv in
-(*   if occur_meta_or_existential mvty or is_arity env sigma mvty then *)
+  if occur_meta_or_existential mvty or is_arity env sigma mvty then
     unify_to_type env sigma flags c status mvty
-(*   else (sigma,[],[]) *)
+  else (sigma,[],[])
 
 (* Move metas that may need coercion at the end of the list of instances *)
 
@@ -677,19 +687,15 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
    [clenv_typed_unify M N clenv] expects in addition that expected
    types of metavars are unifiable with the types of their instances    *)
 
-let check_types env flags (sigma,_,_ as subst) m n =
-  if isEvar_or_Meta (fst (whd_stack sigma m)) then
-    unify_0_with_initial_metas subst true env Cumul
-      flags
-      (Retyping.get_type_of env sigma n)
-      (Retyping.get_type_of env sigma m)
-  else if isEvar_or_Meta (fst (whd_stack sigma n)) then
-    unify_0_with_initial_metas subst true env Cumul
-      flags
-      (Retyping.get_type_of env sigma m)
-      (Retyping.get_type_of env sigma n)
+let check_types env flags (sigma,ms,es as subst) m n =
+  if isEvar_or_Meta (fst (whd_stack sigma m)) ||
+    isEvar_or_Meta (fst (whd_stack sigma n)) then
+    let sigma, mt = get_type_of_with_variables env sigma m in
+    let sigma, nt = get_type_of_with_variables env sigma n in
+      unify_0_with_initial_metas (sigma,ms,es) true env topconv
+	flags mt nt
   else subst
-
+    
 let w_unify_core_0 env with_types cv_pb flags m n evd =
   let (mc1,evd') = retract_coercible_metas evd in
   let (sigma,ms,es) = check_types env flags (evd,mc1,[]) m n in