Work around issues with FO unification trying to unify terms of

potentially different types, resulting in ill-typed terms due to eta.
Projection expansion now fails gracefully on retyping errors.
The proper fix to unification, checking that the heads for FO
have unifiable types, is currently too strong, adding unnecessary universe
constraints, so it is disabled for now. It might be quite expensive
too also it's not noticeable on the stdlib.

7 files changed, 90 insertions, 45 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2db31ccda..694627983 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -34,20 +34,18 @@ let _ = Goptions.declare_bool_option {
 }
 
 let unfold_projection env evd ts p c =
-  if Projection.unfolded p then assert false
-  else     
-    let cst = Projection.constant p in
-      if is_transparent_constant ts cst then
-	let unfold_app () =
-	  let t' = Retyping.expand_projection env evd p c [] in
-	    Some t'
-	in
-	  (match ReductionBehaviour.get (Globnames.ConstRef cst) with
-	  | None -> unfold_app ()
-	  | Some (recargs, nargs, flags) ->
-	    if (List.mem `ReductionNeverUnfold flags) then None
-	    else unfold_app ())
-      else None
+  let cst = Projection.constant p in
+    if is_transparent_constant ts cst then
+      let unfold_app () =
+	let t' = Retyping.expand_projection env evd p c [] in
+	  Some t'
+      in
+	(match ReductionBehaviour.get (Globnames.ConstRef cst) with
+	| None -> unfold_app ()
+	| Some (recargs, nargs, flags) ->
+	  if (List.mem `ReductionNeverUnfold flags) then None
+	  else unfold_app ())
+    else None
 
 let eval_flexible_term ts env evd c =
   match kind_of_term c with
@@ -66,7 +64,9 @@ let eval_flexible_term ts env evd c =
        with Not_found -> None)
   | LetIn (_,b,_,c) -> Some (subst1 b c)
   | Lambda _ -> Some c
-  | Proj (p, c) -> unfold_projection env evd ts p c
+  | Proj (p, c) -> 
+    if Projection.unfolded p then None
+    else unfold_projection env evd ts p c
   | _ -> assert false
 
 type flex_kind_of_term =
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index a41e0169a..94ec82029 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -101,6 +101,10 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
   in
     if !modified then !evdref, t' else !evdref, t
 
+let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c =
+  let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in
+    refresh_universes (Some false) env sigma ty
+
 (************************)
 (* Unification results  *)
 (************************)
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 0d0f3c0e5..fc9f25f96 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -69,3 +69,6 @@ val check_evar_instance :
 
 val remove_instance_local_defs :
   evar_map -> existential_key -> constr array -> constr list
+
+val get_type_of_refresh : 
+  ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * types
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 826fd59ba..95b7e044b 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1389,7 +1389,7 @@ let eq_constr_univs evd t u =
   let b, c = Universes.eq_constr_univs_infer evd.universes.uctx_universes t u in
     if b then 
       try let evd' = add_universe_constraints evd c in evd', b
-      with Univ.UniverseInconsistency _ -> evd, false
+      with Univ.UniverseInconsistency _ | UniversesDiffer -> evd, false
     else evd, b
 
 let e_eq_constr_univs evdref t u =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 8dc46b79b..69f2ba2d0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1488,13 +1488,11 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
 	  (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in
 	if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
-      |args, (Stack.Proj (n,m,p,_) :: stack'' as stack') ->
+      |args, (Stack.Proj (n,m,p,_) :: stack'') ->
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
 	  (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in
-	if isConstruct t_o then
-	  if Projection.unfolded p || Closure.is_transparent_constant ts (Projection.constant p)
-	  then whrec Cst_stack.empty (* csts_o *) (Stack.nth stack_o (n+m), stack'')
-	  else (* Won't unfold *) (whd_betaiota_state sigma (t_o, stack_o@stack'),csts')
+	if isConstruct t_o && Projection.unfolded p then
+	  whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'')
 	else s,csts'
       |_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts'
   in whrec csts s
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 23ad43a1c..653ce3b45 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -244,7 +244,10 @@ let sorts_of_context env evc ctxt =
   snd (aux ctxt)
 
 let expand_projection env sigma pr c args =
-  let ty = get_type_of env sigma c in
-  let (i,u), ind_args = Inductiveops.find_mrectype env sigma ty in
+  let ty = get_type_of ~lax:true env sigma c in
+  let (i,u), ind_args = 
+    try Inductiveops.find_mrectype env sigma ty 
+    with Not_found -> retype_error BadRecursiveType
+  in
     mkApp (mkConstU (Projection.constant pr,u), 
 	   Array.of_list (ind_args @ (c :: args)))
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 8d0d5394a..0b00b6ee3 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -397,9 +397,13 @@ let unfold_projection env p stk =
 let expand_key ts env sigma = function
   | Some (IsKey k) -> expand_table_key env k
   | Some (IsProj (p, c)) -> 
-    let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma 
-			  Cst_stack.empty (c, unfold_projection env p [])))
-    in if Term.eq_constr (mkProj (p, c)) red then None else Some red
+    if Projection.unfolded p then 
+      let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma 
+				  Cst_stack.empty (c, unfold_projection env (Projection.unfold p) [])))
+      in if Term.eq_constr (mkProj (p, c)) red then None else Some red
+    else 
+      (try Some (Retyping.expand_projection env sigma p c [])
+       with RetypeError _ -> None)
   | None -> None
 
 let subterm_restriction is_subterm flags =
@@ -442,9 +446,11 @@ let oracle_order env cf1 cf2 =
       | Some k2 ->
 	match k1, k2 with
 	| IsProj (p, _), IsKey (ConstKey (p',_)) 
-	  when eq_constant (Projection.constant p) p' -> Some false
+	  when eq_constant (Projection.constant p) p' -> 
+	  Some (not (Projection.unfolded p))
 	| IsKey (ConstKey (p,_)), IsProj (p', _) 
-	  when eq_constant p (Projection.constant p') -> Some true
+	  when eq_constant p (Projection.constant p') -> 
+	  Some (Projection.unfolded p')
 	| _ ->
           Some (Conv_oracle.oracle_order (Environ.oracle env) false
 		  (translate_key k1) (translate_key k2))
@@ -618,6 +624,27 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	| LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb b wt substn (subst1 a c) cN
 	| _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb b wt substn cM (subst1 a c)
 
+
+	| Proj (p1,c1), _ when not (Projection.unfolded p1) ->
+	  let cM' =
+	    try Retyping.expand_projection curenv sigma p1 c1 []
+	    with RetypeError _ ->
+	      (** Unification can be called on ill-typed terms, due
+		  to FO and eta in particular, fail gracefully in that case *)
+	      error_cannot_unify (fst curenvnb) sigma (cM,cN)
+	  in
+	    unirec_rec curenvnb CONV true false substn cM' cN
+
+	| _, Proj (p2,c2) when not (Projection.unfolded p2) ->
+	  let cN' =
+	    try Retyping.expand_projection curenv sigma p2 c2 []
+	    with RetypeError _ ->
+	      (** Unification can be called on ill-typed terms, due
+		  to FO and eta in particular, fail gracefully in that case *)
+	      error_cannot_unify (fst curenvnb) sigma (cM,cN)
+	  in
+	    unirec_rec curenvnb CONV true false substn cM cN'
+
         (* eta-expansion *)
 	| Lambda (na,t1,c1), _ when flags.modulo_eta ->
 	    unirec_rec (push (na,t1) curenvnb) CONV true wt substn
@@ -661,26 +688,18 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 		  try (* Force unification of the types to fill in parameters *)
 		    let ty1 = get_type_of curenv ~lax:true sigma c1 in
 		    let ty2 = get_type_of curenv ~lax:true sigma c2 in
-		      unify_0_with_initial_metas substn true curenv cv_pb 
-			{ flags with modulo_conv_on_closed_terms = Some full_transparent_state;
-			  modulo_delta = full_transparent_state;
-			  modulo_eta = true;
-			  modulo_betaiota = true }
-			ty1 ty2
+		      unify_0_with_initial_metas substn true curenv cv_pb
+		    	{ flags with modulo_conv_on_closed_terms = Some full_transparent_state;
+		    	  modulo_delta = full_transparent_state;
+		    	  modulo_eta = true;
+		    	  modulo_betaiota = true }
+		    	ty1 ty2
 		  with RetypeError _ -> substn
 	      with ex when precatchable_exception ex ->
 	        unify_not_same_head curenvnb pb b wt substn cM cN
 	    else
 	      unify_not_same_head curenvnb pb b wt substn cM cN
 
-	| Proj (p1,c1), _ when not (Projection.unfolded p1) ->
-	  let cM' = Retyping.expand_projection curenv sigma p1 c1 [] in
-	    unirec_rec curenvnb CONV true false substn cM' cN
-
-	| _, Proj (p2,c2) when not (Projection.unfolded p2) ->
-	  let cN' = Retyping.expand_projection curenv sigma p2 c2 [] in
-	    unirec_rec curenvnb CONV true false substn cM cN'
-
 	| App (f1,l1), _ when 
 	    (isMeta f1 && use_metas_pattern_unification flags nb l1
             || use_evars_pattern_unification flags && isAllowedEvar flags f1) ->
@@ -713,11 +732,29 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	| _ ->
             unify_not_same_head curenvnb pb b wt substn cM cN
 
-  and unify_app curenvnb pb b substn cM f1 l1 cN f2 l2 =
+  and unify_app (curenv, nb as curenvnb) pb b (sigma, metas, evars as substn) cM f1 l1 cN f2 l2 =
     try
       let (f1,l1,f2,l2) = adjust_app_array_size f1 l1 f2 l2 in
-      Array.fold_left2 (unirec_rec curenvnb CONV true false)
-	(unirec_rec curenvnb CONV true true substn f1 f2) l1 l2
+      (* let substn = *)
+      (* 	let sigma, b = Evd.eq_constr_univs sigma f1 f2 in *)
+      (* 	  if b then (sigma,metas,evars) *)
+      (* 	  else if isEvar_or_Meta f1 || isEvar_or_Meta f2 then (sigma,metas,evars) *)
+      (* 	  else *)
+      (* 	    try *)
+      (* 	      let sigma', ty1 = Evarsolve.get_type_of_refresh curenv ~lax:true sigma f1 in *)
+      (* 	      let sigma', ty2 = Evarsolve.get_type_of_refresh curenv ~lax:true sigma f2 in *)
+      (* 	      let substn = unify_0_with_initial_metas (sigma', metas, evars) true curenv CONV *)
+      (* 	      	{ flags with modulo_conv_on_closed_terms = Some full_transparent_state; *)
+      (* 	      	  modulo_delta = full_transparent_state; *)
+      (* 	      	  modulo_eta = true; *)
+      (* 	      	  modulo_betaiota = true } *)
+      (* 	      	ty1 ty2 *)
+      (* 	      in substn *)
+      (* 	    with RetypeError _ -> *)
+      (* 	      error_cannot_unify (fst curenvnb) sigma (cM,cN) *)
+      (* in *)
+	Array.fold_left2 (unirec_rec curenvnb CONV true false)
+	  (unirec_rec curenvnb CONV true true substn f1 f2) l1 l2
     with ex when precatchable_exception ex ->
     try reduce curenvnb pb b false substn cM cN
     with ex when precatchable_exception ex ->