Fixes for new unification, not used in default version as it really changes unification.

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

4 files changed, 69 insertions, 62 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index b1b02ffd01..aa4a200e74 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -228,39 +228,39 @@ module Default = struct
 		error_actual_type_loc loc env sigma cj t
 	  in
 	  let val' = match val' with Some v -> v | None -> assert(false) in
-	    (evd',{ uj_val = val'; uj_type = t })
+	  let nf = nf_isevar evd' in
+	    (evd',{ uj_val = nf val'; uj_type = nf t })
       | Some (init, cur) -> (isevars, cj)
       
-      
-
-  open Pp
-  let inh_conv_coerces_to loc env isevars t (abs, t') = isevars
-  (* Still bugguy 
-(*     (try *)
-(*        msgnl (str "inh_conv_coerces_to called for " ++ *)
-(* 	      Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
-(* 	      Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++ *)
-(* 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
-(* 	      Termops.print_env env); *)
-(*      with _ -> ()); *)
-    try let (rels, rng) = 
-      (* a little more effort to get products is needed *) 
-      try decompose_prod_n abs t
-      with _ -> 
-	raise (Invalid_argument "Coercion.inh_conv_coerces_to")
-    in
-      if noccur_between 0 (succ abs) rng then (
-	(* msgnl (str "No occur between 0 and " ++ int (succ abs)); *)
-	let env', t, t' = 
-	  let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
-	    env', rng, lift abs t'
-	in
-	  try 
-	    pi1 (inh_conv_coerce_to_fail loc env' isevars None t t')
-	  with NoCoercion ->
-	    isevars) (* Maybe not enough information to unify *)
-	    (*let sigma = evars_of isevars in
-	      error_cannot_coerce env' sigma (t, t'))*)
-      else isevars
-    with Invalid_argument _ -> isevars *)
+    let inh_conv_coerces_to loc env (isevars : evar_defs) t (abs, t') = isevars
+      (* Still problematic, as it changes unification 
+      let nabsinit, nabs = 
+	match abs with
+	    None -> 0, 0
+	  | Some (init, cur) -> init, cur
+      in
+	try 
+	  let (rels, rng) = 
+	    (* a little more effort to get products is needed *) 
+	    try decompose_prod_n nabs t
+	    with _ -> 
+	      if !Options.debug then
+		msg_warning (str "decompose_prod_n failed");
+	      raise (Invalid_argument "Coercion.inh_conv_coerces_to")
+	  in
+	    (* The final range free variables must have been replaced by evars, we accept only that evars
+	       in rng are applied to free vars. *)
+	    if noccur_with_meta 0 (succ nabsinit) rng then (
+	      let env', t, t' = 
+		let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
+		  env', rng, lift nabs t'
+	      in
+		try 
+		  pi1 (inh_conv_coerce_to_fail loc env' isevars None t t')
+		with NoCoercion ->
+		  isevars) (* Maybe not enough information to unify *)
+	      (*let sigma = evars_of isevars in
+		error_cannot_coerce env' sigma (t, t'))*)
+	    else isevars
+	with Invalid_argument _ -> isevars	  *)
 end
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 79e25a5afc..0e3b8f62b3 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -642,38 +642,43 @@ let split_tycon loc env isevars tycon =
     let sigma = evars_of isevars in
     let t = whd_betadeltaiota env sigma c in
       match kind_of_term t with
-	| Prod (na,dom,rng) -> isevars, (na, mk_tycon dom, mk_tycon rng)
+	| Prod (na,dom,rng) -> isevars, (na, dom, rng)
 	| Evar ev when not (Evd.is_defined_evar isevars ev) ->
 	    let (isevars',prod) = define_evar_as_arrow isevars ev in
 	    let (_,dom,rng) = destProd prod in
-	      isevars',(Anonymous, mk_tycon dom, mk_tycon rng)
+	      isevars',(Anonymous, dom, rng)
 	| _ -> error_not_product_loc loc env sigma c
   in
     match tycon with
       | None -> isevars,(Anonymous,None,None)
       | Some (abs, c) ->
 	  (match abs with
-	       None -> real_split c
+	       None -> 
+		 let isevars', (n, dom, rng) = real_split c in
+		   isevars', (n, mk_tycon dom, mk_tycon rng)
 	     | Some (init, cur) ->
-	       if cur = 1 then isevars, (Anonymous, None, 
-					 Some (Some (init, 0), c))
-	       else
-		 isevars, (Anonymous, None, Some (Some (init, pred cur), c)))
+		 if cur = 0 then 
+		   let isevars', (x, dom, rng) = real_split c in
+		     isevars, (Anonymous, 
+			       Some (Some (init, 0), dom), 
+			       Some (Some (init, 0), rng))
+		 else
+		   isevars, (Anonymous, None, Some (Some (init, pred cur), c)))
 
 let valcon_of_tycon x = 
   match x with
     | Some (None, t) -> Some t
     | _ -> None
 	
-let lift_tycon_type n (abs, t) =
-  abs, lift n t
-(*  match abs with 
-      None -> (abs, lift n t)
+let lift_abstr_tycon_type n (abs, t) =
+  match abs with 
+      None -> raise (Invalid_argument "lift_abstr_tycon_type: not an abstraction")
     | Some (init, abs) ->
 	let abs' = abs + n in 
-	  if abs' < 0 then raise (Invalid_argument "lift_tycon_type")
-	  else (Some (init, abs'), lift n t)*)
+	  if abs' < 0 then raise (Invalid_argument "lift_abstr_tycon_type")
+	  else (Some (init, abs'), t)
 
+let lift_tycon_type n (abs, t) = (abs, lift n t)
 let lift_tycon n = option_app (lift_tycon_type n)
 
 let pr_tycon_type env (abs, t) =
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 8c5fe9c99b..6ce30ff79b 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -106,6 +106,8 @@ val split_tycon :
 
 val valcon_of_tycon : type_constraint -> val_constraint
 
+val lift_abstr_tycon_type : int -> type_constraint_type -> type_constraint_type
+
 val lift_tycon_type : int -> type_constraint_type -> type_constraint_type
 val lift_tycon : int -> type_constraint -> type_constraint
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b3590492ab..f48ec74624 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -352,9 +352,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	      None -> None
 	    | Some (None, ty) -> mk_abstr_tycon length ty
 	    | Some (Some (init, cur), ty) ->
-		Some (Some (length + init, cur), ty)
+		Some (Some (length + init, length + cur), ty)
 	in
-	let fj = pretype ftycon env isevars lvar f in
+	let fj = pretype empty_tycon env isevars lvar f in
  	let floc = loc_of_rawconstr f in
 	let rec apply_rec env n resj tycon = function
 	  | [] -> resj
@@ -368,23 +368,23 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
 		      let typ' = nf_isevar !isevars typ in
 		      let tycon = 
-			match tycon with			    
-			    Some (abs, ty) ->
-			      (match abs with
-				   None ->
-				     isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
-				       (abs, ty);
-				     Some (None, nf_isevar !isevars ty)
-				 | Some (init, cur) ->
-				     isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
-				       (abs, ty);
-				     Some (Some (init, pred cur), nf_isevar !isevars ty))
-			  | None -> None
+			option_app 
+			  (fun (abs, ty) ->
+			     match abs with
+				 None ->
+				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
+				     (abs, ty);
+				   (abs, ty)
+			       | Some (init, cur) ->
+				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
+				     (abs, ty);
+				   (Some (init, pred cur), ty))
+			  tycon
 		      in 
 			apply_rec env (n+1) 
 			  { uj_val = nf_isevar !isevars value;
 			    uj_type = nf_isevar !isevars typ' }
-			  tycon rest
+			  (option_app (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest
 
 		  | _ ->
 		      let hj = pretype empty_tycon env isevars lvar c in
@@ -392,7 +392,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 			  (join_loc floc argloc) env (evars_of !isevars)
 	      		  resj [hj]
 	in
-	let ftycon = lift_tycon (-1) ftycon in
+	let ftycon = option_app (lift_abstr_tycon_type (-1)) ftycon in
 	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
 	let resj =
 	  match kind_of_term resj.uj_val with