Nouvelle stratégie d'unification des types des with-bindings dans

apply afin de reculer au plus tard les décisions irréversibles et en
particulier de pouvoir typer les with-bindings modulo coercions :

  - l'unification des types des métas données en with-bindings est
    retardé à après l'unification (unify_0) de telle sorte que les
    instances trouvées par unify_0 soient prioritaires et que la
    décision d'insérer éventuellement des coercions autour des valeurs
    données en with-bindings se fasse au dernier moment;
  - toujours pour permettre d'insérer ultimement des coercions, 
    l'instantiation des with-bindings ne se fait plus
    l'appel unify_0 (cf clenv_unique_resolver);
  - pour permettre ce retardement sans limiter le test de conversion
    que unify_0 fait sur les termes clos, on transmet à unify_0 les
    métas données en with-bindings (ainsi l'instantiation de ces métas
    peut être faite dynamiquement au moment du test de clôture);
  - parce que les métas données en with-bindings qui sont en position
    de rédex (cas d'un "apply f_equal with (f:=fun ...)" peuvent
    simplifier le problème d'unification (et elles ne sont pas de
    toutes façons pas réinférables au premier ordre), on continue à
    les substituer avant l'appel à unify_0 (cf meta_reducible_instance);
  - pour l'unification du second-ordre, on continue d'instancier les
    with-bindings et d'unifier les types des with-bindings avant
    unification;
  - reste à régler un problème de compatibilité lorsque le résultat de
    l'unification des types des with-bindings est utilisé pour rendre
    un terme clos et pour permettre à unify_0 d'utiliser la conversion.

+ meilleure compatibilité de apply, split, left, right pour le code
  qui l'utilise avec des bindings clos
+ nettoyage et uniformisation des clenv_match_args, clenv_missing, et assimilés



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

9 files changed, 224 insertions, 153 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index c563688a8b..96facdef2a 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -30,10 +30,13 @@ open Coercion.Default
 
 (* *)
 let w_coerce env c ctyp target evd =
-  let j = make_judge c ctyp in
-  let tycon = mk_tycon_type target in
-  let (evd',j') = inh_conv_coerce_to dummy_loc env evd j tycon in
-  (evd',j'.uj_val)
+  try
+    let j = make_judge c ctyp in
+    let tycon = mk_tycon_type target in
+    let (evd',j') = inh_conv_coerce_to dummy_loc env evd j tycon in
+    (evd',j'.uj_val)
+  with e when precatchable_exception e ->
+    evd,c
 
 let pf_env gls = Global.env_of_context gls.it.evar_hyps
 let pf_type_of gls c  = Typing.type_of (pf_env gls) gls.sigma c
@@ -209,17 +212,6 @@ let clenv_wtactic f clenv = {clenv with evd = f clenv.evd }
  * type of clenv.
  * If [hyps_only] then metavariables occurring in the type are _excluded_ *)
 
-(* collects all metavar occurences, in left-to-right order, preserving
- * repetitions and all. *)
-
-let collect_metas c = 
-  let rec collrec acc c =
-    match kind_of_term c with
-      | Meta mv -> mv::acc
-      | _         -> fold_constr collrec acc c
-  in
-  List.rev (collrec [] c)
-
 (* [clenv_metavars clenv mv]
  * returns a list of the metavars which appear in the type of
  * the metavar mv.  The list is unordered. *)
@@ -248,12 +240,34 @@ let clenv_missing ce = clenv_dependent true ce
 let clenv_unify allow_K cv_pb t1 t2 clenv =
   { clenv with evd = w_unify allow_K clenv.env cv_pb t1 t2 clenv.evd }
 
+let clenv_unify_meta_types clenv =
+  List.fold_left (fun clenv (k,m) ->
+    match m with
+    | Cltyp _ -> clenv
+    | Clval (na,(c,s),k_typ) ->
+	let k_typ = clenv_hnf_constr clenv k_typ.rebus in
+	match s with
+        | Coercible c_typ when not (occur_meta k_typ) -> 
+	    let evd,c' = w_coerce (cl_env clenv) c.rebus c_typ k_typ clenv.evd in
+	    {clenv with evd = meta_reassign k (c',ConvUpToEta 0) clenv.evd}
+	| _ -> 
+	    (* nf_betaiota was before in type_of - useful to reduce
+	       types like (x:A)([x]P u) *)
+	    let c_typ = nf_betaiota (clenv_get_type_of clenv c.rebus) in
+	    let c_typ = clenv_hnf_constr clenv c_typ in
+	    (* Try to infer some Meta/Evar from the type of [c] *)
+	    try clenv_unify true CUMUL c_typ k_typ clenv
+	    with e when precatchable_exception e -> clenv)
+    clenv (meta_list clenv.evd)
+
+
 let clenv_unique_resolver allow_K clenv gl =
   if isMeta (fst (whd_stack clenv.templtyp.rebus)) then
-    clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl) clenv
+    clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl)
+      (clenv_unify_meta_types clenv)
   else
-    try clenv_unify allow_K CUMUL clenv.templtyp.rebus (pf_concl gl) clenv
-    with _ -> clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl) clenv
+    clenv_unify allow_K CUMUL 
+      (meta_reducible_instance clenv.evd clenv.templtyp) (pf_concl gl) clenv
 
 (* [clenv_pose_dependent_evars clenv]
  * For each dependent evar in the clause-env which does not have a value,
@@ -326,7 +340,7 @@ let clenv_fchain mv clenv nextclenv =
 (***************************************************************)
 (* Bindings *)
 
-type arg_bindings = (int * open_constr) list
+type arg_bindings = open_constr explicit_bindings
 
 (* [clenv_independent clenv]
  * returns a list of metavariables which appear in the term cval,
@@ -340,22 +354,24 @@ let clenv_independent clenv =
   let deps = dependent_metas clenv mvs ctyp_mvs in
   List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
 
-let meta_of_binder clause loc b t mvs =
-  match b with
-    | NamedHyp s ->
-	if List.exists (fun (_,b',_) -> b=b') t then 
-	  errorlabstrm ""
-	    (str "The variable " ++ pr_id s ++ 
-	     str " occurs more than once in binding");
-        meta_with_name clause.evd s
-    | AnonHyp n ->
-	if List.exists (fun (_,b',_) -> b=b') t then
-	  errorlabstrm ""
-	    (str "The position " ++ int n ++
-	    str " occurs more than once in binding");
-	try List.nth mvs (n-1)
-	with (Failure _|Invalid_argument _) ->
-          errorlabstrm "" (str "No such binder")
+let check_bindings bl =
+  match list_duplicates (List.map pi2 bl) with
+    | NamedHyp s :: _ -> 
+	errorlabstrm ""
+	  (str "The variable " ++ pr_id s ++ 
+	   str " occurs more than once in binding list");
+    | AnonHyp n :: _ ->
+	errorlabstrm ""
+	  (str "The position " ++ int n ++
+	   str " occurs more than once in binding list")
+    | [] -> ()
+
+let meta_of_binder clause loc mvs = function
+  | NamedHyp s -> meta_with_name clause.evd s
+  | AnonHyp n ->
+      try List.nth mvs (n-1)
+      with (Failure _|Invalid_argument _) ->
+        errorlabstrm "" (str "No such binder")
 
 let error_already_defined b =
   match b with
@@ -367,92 +383,49 @@ let error_already_defined b =
         anomalylabstrm ""
           (str "Position " ++ int n ++ str" already defined")
 
-let clenv_match_args s clause =
-  let mvs = clenv_independent clause in 
-  let rec matchrec clenv = function
-    | [] -> clenv
-    | (loc,b,(sigma,c))::t ->
-	let k = meta_of_binder clenv loc b t mvs in
+let clenv_match_args bl clenv =
+  if bl = [] then
+    clenv
+  else
+    let mvs = clenv_independent clenv in
+    check_bindings bl;
+    List.fold_left
+      (fun clenv (loc,b,(sigma,c)) ->
+	let k = meta_of_binder clenv loc mvs b in
         if meta_defined clenv.evd k then
-          if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then
-            matchrec clenv t
+          if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
           else error_already_defined b
         else
-	  let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
-	    (* nf_betaiota was before in type_of - useful to reduce
-               types like (x:A)([x]P u) *)
-	  let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
-	  let c_typ = nf_betaiota (clenv_get_type_of clenv' c) in
-	  let c_typ = clenv_hnf_constr clenv' c_typ in
-	  let clenv'' =
-	    (* Try to infer some Meta/Evar from the type of [c] *)
-	    try clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clenv')
-	    with e when precatchable_exception e ->
-	    (* Try to coerce to the type of [k]; cannot merge with the
-	       previous case because Coercion does not handle Meta *)
-            let (evd,c') = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in
-	    try clenv_unify true CONV (mkMeta k) c' { clenv' with evd = evd }
-	    with PretypeError (env,CannotUnify (m,n)) ->
-	      Stdpp.raise_with_loc loc
- 	        (PretypeError (env,CannotUnifyBindingType (m,n)))
-	  in matchrec clenv'' t
-  in 
-  matchrec clause s
-
-
-let clenv_constrain_with_bindings bl clause =
-  if bl = [] then 
-    clause 
-  else 
-    let all_mvs = collect_metas clause.templval.rebus in
-    let rec matchrec clause = function
-      | []       -> clause
-      | (n,(sigma,c))::t ->
-          let k = 
-            (try
-              if n > 0 then 
-		List.nth all_mvs (n-1)
-              else if n < 0 then 
-		List.nth (List.rev all_mvs) (-n-1)
-              else error "clenv_constrain_with_bindings" 
-            with Failure _ ->
-              errorlabstrm "clenv_constrain_with_bindings"
-                (str"Clause did not have " ++ int n ++ str"-th" ++
-                str" absolute argument")) in
-	  let k_typ = nf_betaiota (clenv_meta_type clause k) in
-	  let cl = { clause with evd = evar_merge clause.evd sigma} in
-	  let c_typ = nf_betaiota (clenv_get_type_of cl c) in 
-	  matchrec
-            (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t
-    in 
-    matchrec clause bl
-
-
-(* not exported: maybe useful ? *)
-let clenv_constrain_dep_args hyps_only clause = function
-  | [] -> clause 
-  | mlist ->
-      let occlist = clenv_dependent hyps_only clause in
-      if List.length occlist = List.length mlist then
-	List.fold_left2
-          (fun clenv k (sigma,c) ->
-	    let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
-	    let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
-	    let c_typ = clenv_hnf_constr clenv' (clenv_get_type_of clenv' c) in
-	    try
-              (* faire quelque chose avec le sigma retourne ? *)
-	      let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in
-	      clenv_unify true CONV (mkMeta k) c' { clenv' with evd = evd }
-	    with _ ->
-              clenv_unify true CONV (mkMeta k) c clenv')
-          clause occlist mlist
-      else 
-	error ("Not the right number of missing arguments (expected "
-	       ^(string_of_int (List.length occlist))^")")
-
-let clenv_constrain_missing_args mlist clause =
-  clenv_constrain_dep_args true clause mlist
-
+	  let c_typ = nf_betaiota (clenv_get_type_of clenv c) in
+	  let c_typ = clenv_hnf_constr clenv c_typ in
+	  let clenv = { clenv with evd = evar_merge clenv.evd sigma} in
+	  {clenv with evd = meta_assign k (c,Coercible c_typ) clenv.evd})
+      clenv bl
+
+let clenv_assign_binding clenv k (sigma,c) =
+  let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
+  let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
+  let c_typ = clenv_hnf_constr clenv' (clenv_get_type_of clenv' c) in
+  let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in
+  { clenv' with evd = meta_assign k (c',Coercible c_typ) evd }
+
+let clenv_constrain_last_binding c clenv =
+  let all_mvs = collect_metas clenv.templval.rebus in
+  let k =
+    try list_last all_mvs 
+    with Failure _ -> error "clenv_constrain_with_bindings" in
+  clenv_assign_binding clenv k (Evd.empty,c)
+
+let clenv_constrain_dep_args hyps_only bl clenv =
+  if bl = [] then
+    clenv
+  else
+    let occlist = clenv_dependent hyps_only clenv in
+    if List.length occlist = List.length bl then
+      List.fold_left2 clenv_assign_binding clenv occlist bl
+    else 
+      error ("Not the right number of missing arguments (expected "
+	     ^(string_of_int (List.length occlist))^")")
 
 (****************************************************************)
 (* Clausal environment for an application *)
@@ -460,7 +433,7 @@ let clenv_constrain_missing_args mlist clause =
 let make_clenv_binding_gen hyps_only n gls (c,t) = function
   | ImplicitBindings largs ->
       let clause = mk_clenv_from_n gls n (c,t) in
-      clenv_constrain_dep_args hyps_only clause largs
+      clenv_constrain_dep_args hyps_only largs clause
   | ExplicitBindings lbind ->
       let clause = mk_clenv_rename_from_n gls n (c,t) in
       clenv_match_args lbind clause
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index b9ee5dde4d..ccaa22f5e9 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -84,18 +84,20 @@ val clenv_pose_dependent_evars : clausenv -> clausenv
 (***************************************************************)
 (* Bindings *)
 
+type arg_bindings = open_constr explicit_bindings
+
 (* bindings where the key is the position in the template of the
    clenv (dependent or not). Positions can be negative meaning to
    start from the rightmost argument of the template. *)
-type arg_bindings = (int * open_constr) list
-
 val clenv_independent : clausenv -> metavariable list
 val clenv_missing : clausenv -> metavariable list
 
+val clenv_constrain_last_binding : constr -> clausenv -> clausenv
+
 (* defines metas corresponding to the name of the bindings *)
-val clenv_match_args :
-  open_constr explicit_bindings -> clausenv -> clausenv
-val clenv_constrain_with_bindings : arg_bindings -> clausenv -> clausenv
+val clenv_match_args : arg_bindings -> clausenv -> clausenv
+
+val clenv_unify_meta_types : clausenv -> clausenv
 
 (* start with a clenv to refine with a given term with bindings *)
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 1ff0c633a0..ebd635b807 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -334,7 +334,8 @@ let map_fl f cfl = { cfl with rebus=f cfl.rebus }
     (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice)
 *)
 
-type instance_status = IsSuperType | IsSubType | ConvUpToEta of int
+type instance_status =
+    IsSuperType | IsSubType | ConvUpToEta of int | Coercible of types
 
 (* Clausal environments *)
 
@@ -535,6 +536,28 @@ let meta_merge evd1 evd2 =
     metas = List.fold_left (fun m (n,v) -> Metamap.add n v m) 
       evd2.metas (metamap_to_list evd1.metas) }
 
+type metabinding = metavariable * constr * instance_status
+
+let retract_defined_metas evd =
+  let mc,ml = 
+    Metamap.fold (fun n v (mc,ml) -> 
+      match v with
+	| Clval (na,(b,s),typ) ->
+	    (n,b.rebus,s)::mc, Metamap.add n (Cltyp (na,typ)) ml
+	| Cltyp _ as v ->
+	    mc, Metamap.add n v ml)
+      evd.metas ([],Metamap.empty) in
+  mc, { evd with metas = ml }
+
+let rec list_assoc_in_triple x = function
+    [] -> raise Not_found
+  | (a,b,_)::l -> if compare a x = 0 then b else list_assoc_in_triple x l
+
+let subst_defined_metas bl c = 
+  let rec substrec c = match kind_of_term c with
+    | Meta i -> list_assoc_in_triple i bl
+    | _ -> map_constr substrec c
+  in try Some (substrec c) with Not_found -> None
 
 (**********************************************************)
 (* Pretty-printing *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index a1323e501c..784e066b71 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -111,7 +111,8 @@ val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
     (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice)
 *)
 
-type instance_status = IsSuperType | IsSubType | ConvUpToEta of int
+type instance_status =
+    IsSuperType | IsSubType | ConvUpToEta of int | Coercible of types
 
 type clbinding =
   | Cltyp of name * constr freelisted
@@ -177,6 +178,11 @@ val meta_merge : evar_defs -> evar_defs -> evar_defs
 
 val metas_of : evar_defs -> metamap
 
+type metabinding = metavariable * constr * instance_status
+
+val retract_defined_metas : evar_defs -> metabinding list * evar_defs
+val subst_defined_metas : metabinding list -> constr -> constr option
+
 (**********************************************************)
 (* Sort variables *)
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 481fa16eea..3e9b08beb4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -879,3 +879,31 @@ let meta_instance env b =
   instance c_sigma b.rebus
 
 let nf_meta env c = meta_instance env (mk_freelisted c)
+
+(* Instantiate metas that create beta/iota redexes *)
+
+let meta_reducible_instance env b =
+  let s =
+    List.map (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas)
+  in 
+  let rec irec u =
+    let u = whd_betaiota u in
+    match kind_of_term u with
+    | Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) ->
+        let bl' = Array.map irec bl in
+        let p' = irec p in
+	let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in
+	let g = List.assoc m s in
+	(match kind_of_term g with
+           | Construct _ -> whd_betaiota (mkCase (ci,p',g,bl'))
+           | _ -> mkCase (ci,p',c,bl'))
+    | App (f,l) when isMeta f or isCast f & isMeta (pi1 (destCast f)) ->
+        let l' = Array.map irec l in
+	let m = try destMeta f with _ -> destMeta (pi1 (destCast f)) in
+	let g = List.assoc m s in
+	(match kind_of_term g with
+           | Lambda _ -> beta_appvect g l'
+           | _ -> mkApp (f,l'))
+    | _ -> map_constr irec u
+  in 
+  if s = [] then b.rebus else irec b.rebus
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 8c792dc805..2dbf60a422 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -217,3 +217,4 @@ val apprec :  state_reduction_function
 (*s Meta-related reduction functions *)
 val meta_instance : evar_defs -> constr freelisted -> constr
 val nf_meta       : evar_defs -> constr -> constr
+val meta_reducible_instance : evar_defs -> constr freelisted -> constr
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 6597ce5a3b..668b3a1eb4 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -514,6 +514,16 @@ let free_rels m =
   in 
   frec 1 Intset.empty m
 
+(* collects all metavar occurences, in left-to-right order, preserving
+ * repetitions and all. *)
+
+let collect_metas c = 
+  let rec collrec acc c =
+    match kind_of_term c with
+      | Meta mv -> mv::acc
+      | _         -> fold_constr collrec acc c
+  in
+  List.rev (collrec [] c)
 
 (* (dependent M N) is true iff M is eq_term with a subterm of N 
    M is appropriately lifted through abstractions of N *)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 7fbd130ca4..27e86a6ca5 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -102,7 +102,7 @@ val occur_var_in_decl :
 val occur_term : constr -> constr -> bool
 val free_rels : constr -> Intset.t
 val dependent : constr -> constr -> bool
-
+val collect_metas : constr -> int list
 (* Substitution of metavariables *)
 type metamap = (metavariable * constr) list 
 val subst_meta : metamap -> constr -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5231cce429..e296737f25 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -65,7 +65,7 @@ let prod_pb = function ConvUnderApp _ -> topconv | pb -> pb
 let opp_status = function
   | IsSuperType -> IsSubType
   | IsSubType -> IsSuperType
-  | ConvUpToEta _ as x -> x
+  | ConvUpToEta _ | Coercible _ as x -> x
 
 let extract_instance_status = function
   | Cumul -> (IsSubType,IsSuperType)
@@ -110,13 +110,13 @@ let unify_r2l x = x
 let sort_eqns = unify_r2l
 *)
 
-let unify_0 env sigma cv_pb mod_delta m n =
-  let trivial_unify pb substn m n =
-    if (not(occur_meta m)) && 
-      (if mod_delta then is_fconv (conv_pb_of pb) env sigma m n
-       else eq_constr m n)
-    then substn
-    else error_cannot_unify env sigma (m,n) in
+let unify_0_with_initial_metas metas env sigma cv_pb mod_delta m n =
+  let trivial_unify pb (metasubst,_ as substn) m n =
+    match subst_defined_metas (* too strong: metasubst *) metas m with
+      | Some m when
+	  (if mod_delta then is_fconv (conv_pb_of pb) env sigma m n
+	  else eq_constr m n) -> substn
+      | _ -> error_cannot_unify env sigma (m,n) in
   let rec unirec_rec curenv pb ((metasubst,evarsubst) as substn) curm curn =
     let cM = Evarutil.whd_castappevar sigma curm
     and cN = Evarutil.whd_castappevar sigma curn in 
@@ -183,11 +183,13 @@ let unify_0 env sigma cv_pb mod_delta m n =
       (if mod_delta then is_fconv (conv_pb_of cv_pb) env sigma m n
        else eq_constr m n)
     then 
-      ([],[])
+      (metas,[])
     else 
-      let (mc,ec) = unirec_rec env cv_pb ([],[]) m n in
+      let (mc,ec) = unirec_rec env cv_pb (metas,[]) m n in
 	((*sort_eqns*) mc, (*sort_eqns*) ec)
 
+let unify_0 = unify_0_with_initial_metas []
+
 let left = true
 let right = false
 
@@ -229,11 +231,13 @@ let merge_instances env sigma mod_delta st1 st2 c1 c2 =
   | (ConvUpToEta n1, ConvUpToEta n2) ->
       let side = left (* arbitrary choice, but agrees with compatibility *) in
       unify_with_eta side mod_delta env sigma n1 n2 c1 c2
-  | ((IsSubType  |ConvUpToEta _ as oppst1),(IsSubType  |ConvUpToEta _)) ->
+  | ((IsSubType | ConvUpToEta _ | Coercible _ as oppst1),
+     (IsSubType | ConvUpToEta _ | Coercible _)) ->
       let res = unify_0 env sigma Cumul mod_delta c2 c1 in
       if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
       else (st2=IsSubType, ConvUpToEta 0, res)
-  | ((IsSuperType|ConvUpToEta _ as oppst1),(IsSuperType|ConvUpToEta _)) ->
+  | ((IsSuperType | ConvUpToEta _ | Coercible _ as oppst1),
+     (IsSuperType | ConvUpToEta _ | Coercible _)) ->
       let res = unify_0 env sigma Cumul mod_delta c1 c2 in
       if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
       else (st2=IsSuperType, ConvUpToEta 0, res)
@@ -310,6 +314,15 @@ let is_mimick_head f =
   match kind_of_term f with
       (Const _|Var _|Rel _|Construct _|Ind _) -> true
     | _ -> false
+
+let w_coerce env c ctyp target evd =
+  try
+    let j = make_judge c ctyp in
+    let tycon = mk_tycon_type target in
+    let (evd',j') = Coercion.Default.inh_conv_coerce_to dummy_loc env evd j tycon in
+    (evd',j'.uj_val)
+  with e when precatchable_exception e ->
+    evd,c
  
 (* [w_merge env sigma b metas evars] merges common instances in metas
    or in evars, possibly generating new unification problems; if [b]
@@ -365,19 +378,32 @@ let w_merge env with_types mod_delta metas evars evd =
             w_merge_rec evd' (metas'@t) evars'
     	  else
 	    begin
+	      let evd,n =
+		if with_types (* or occur_meta mvty *) then
+                  let sigma = evars_of evd in
+		  let metas = metas_of evd in
+	          let mvty = Typing.meta_type evd mv in
+		  let mvty = Tacred.hnf_constr env sigma mvty in
+		  (* nf_betaiota was before in type_of - useful to reduce
+		     types like (x:A)([x]P u) *)
+		  let n = refresh_universes n in
+		  let nty = get_type_of_with_meta env sigma metas n in
+		  let nty = Tacred.hnf_constr env sigma (nf_betaiota nty) in
+		  if occur_meta mvty then
+		    (try 
+		      let (mc,ec) = unify_0 env sigma Cumul mod_delta nty mvty
+		      in
+		      ty_metas := mc @ !ty_metas;
+		      ty_evars := ec @ !ty_evars;
+		      evd,n
+		    with e when precatchable_exception e -> evd,n)
+		  else
+		    (* Try to coerce to the type of [k]; cannot merge with the
+		       previous case because Coercion does not handle Meta *)
+		    w_coerce env n nty mvty evd
+		else
+		  evd,n in
 	      let evd' = meta_assign mv (n,status) evd in
-	      if with_types (* or occur_meta mvty *) then
-		begin
-	          let mvty = Typing.meta_type evd' mv in
-		  try 
-                    let sigma = evars_of evd' in
-		    let metas = metas_of evd' in
-		    let nty = get_type_of_with_meta env sigma metas (nf_meta evd' n) in
-		    let (mc,ec) = unify_0 env sigma Cumul mod_delta nty mvty in
-                    ty_metas := mc @ !ty_metas;
-                    ty_evars := ec @ !ty_evars
-		  with e when precatchable_exception e -> ()
-		end;
 	      w_merge_rec evd' t []
 	    end
 		
@@ -413,8 +439,10 @@ let w_merge env with_types mod_delta metas evars evd =
    types of metavars are unifiable with the types of their instances    *)
 
 let w_unify_core_0 env with_types cv_pb mod_delta m n evd =
-  let (mc,ec) = unify_0 env (evars_of evd) cv_pb mod_delta m n in 
-  w_merge env with_types mod_delta mc ec evd
+  let (mc1,evd') = retract_defined_metas evd in
+  let (mc2,ec) = 
+    unify_0_with_initial_metas mc1 env (evars_of evd') cv_pb mod_delta m n in 
+  w_merge env with_types mod_delta mc2 ec evd'
 
 let w_unify_0 env = w_unify_core_0 env false
 let w_typed_unify env = w_unify_core_0 env true