Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).

Use two ways to solve it:
- added a whd_betaiota in solve_simple_eqn (since evarconv itself
  refuses beta to preserve the opportunities of first-order-matching
  expressions of the form "(fun x => P) t"; an advantage of this
  whd_betaiota is also that it may simplify K-redexes.
- also added a last-chance test in case of failing occur-check by
  trying to fully head-normalize (with delta) the right-hand-side
  (allows to solve for instance "?n = id ?n" where id is a constant
  (a bridled form of solve_refl that use fconv instead of evar_conv_x).
Incidentally improved a bit the rendering of the type of generalized
terms in pattern-matching by using whd_betaiota.

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

3 files changed, 50 insertions, 23 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 64ad1801f0..540db1c815 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1024,6 +1024,7 @@ let rec generalize_problem names pb = function
   | [] -> pb
   | i::l ->
       let d = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in
+      let d = on_pi3 (whd_betaiota !(pb.evdref)) d in (* for better rendering *)
       let pb' = generalize_problem names pb l in
       let tomatch = lift_tomatch_stack 1 pb'.tomatch in
       let tomatch = regeneralize_index_tomatch (i+1) tomatch in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index f63c01a3ef..19b05682f2 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -922,6 +922,25 @@ let solve_evar_evar f env evd ev1 ev2 =
   with CannotProject projs2 ->
   postpone_evar_evar env evd projs1 ev1 projs2 ev2
 
+(* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint
+ * definitions. We try to unify the xi with the yi pairwise. The pairs
+ * that don't unify are discarded (i.e. ?i is redefined so that it does not
+ * depend on these args). *)
+
+let solve_refl conv_algo env evd evk argsv1 argsv2 =
+  if argsv1 = argsv2 then evd else
+  let evi = Evd.find_undefined evd evk in
+  (* Filter and restrict if needed *)
+  let evd,evk,args =
+    restrict_upon_filter evd evi evk
+      (fun (a1,a2) -> snd (conv_algo env evd Reduction.CONV a1 a2))
+      (List.combine (Array.to_list argsv1) (Array.to_list argsv2)) in
+  (* Leave a unification problem *)
+  let args1,args2 = List.split args in
+  let argsv1 = Array.of_list args1 and argsv2 = Array.of_list args2 in
+  let pb = (Reduction.CONV,env,mkEvar(evk,argsv1),mkEvar(evk,argsv2)) in
+  Evd.add_conv_pb pb evd
+
 (* We try to instantiate the evar assuming the body won't depend
  * on arguments that are not Rels or Vars, or appearing several times
  * (i.e. we tackle a generalization of Miller-Pfenning patterns unification)
@@ -947,6 +966,7 @@ let solve_evar_evar f env evd ev1 ev2 =
 
 exception NotInvertibleUsingOurAlgorithm of constr
 exception NotEnoughInformationToProgress
+exception OccurCheckIn of evar_map * constr
 
 let rec invert_definition choose env evd (evk,argsv as ev) rhs =
   let aliases = make_alias_map env in
@@ -993,7 +1013,7 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs =
     | Rel i when i>k -> project_variable (mkRel (i-k))
     | Var id -> project_variable t
     | Evar (evk',args' as ev') ->
-        if evk = evk' then error_occur_check env evd evk rhs;
+        if evk = evk' then raise (OccurCheckIn (evd,rhs));
 	(* Evar/Evar problem (but left evar is virtual) *)
 	let projs' =
 	  array_map_to_list
@@ -1043,13 +1063,13 @@ and occur_existential evm c =
     | _ -> iter_constr occrec c
   in try occrec c; false with Occur -> true
 
-and evar_define ?(choose=false) env (evk,_ as ev) rhs evd =
+and evar_define ?(choose=false) env (evk,argsv as ev) rhs evd =
   try
     let (evd',body) = invert_definition choose env evd ev rhs in
     if occur_meta body then error "Meta cannot occur in evar body.";
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
-    if occur_evar evk body then error_occur_check env evd evk body;
+    if occur_evar evk body then raise (OccurCheckIn (evd',body));
     (* needed only if an inferred type *)
     let body = refresh_universes body in
 (* Cannot strictly type instantiations since the unification algorithm
@@ -1074,6 +1094,16 @@ and evar_define ?(choose=false) env (evk,_ as ev) rhs evd =
 	postpone_evar_term env evd ev rhs
     | NotInvertibleUsingOurAlgorithm t ->
 	error_not_clean env evd evk t (evar_source evk evd)
+    | OccurCheckIn (evd,rhs) ->
+	(* last chance: rhs actually reduces to ev *)
+	let c = whd_betadeltaiota env evd rhs in
+	match kind_of_term c with
+	| Evar (evk',argsv2) when evk = evk' ->
+	    solve_refl
+	      (fun env sigma pb c c' -> (evd,is_fconv pb env sigma c c'))
+	      env evd evk argsv argsv2
+	| _ ->
+	    error_occur_check env evd evk rhs
 
 (*-------------------*)
 (* Auxiliary functions for the conversion algorithms modulo evars
@@ -1219,25 +1249,6 @@ let status_changed lev (pbty,_,t1,t2) =
   (try ExistentialSet.mem (head_evar t1) lev with NoHeadEvar -> false) or
   (try ExistentialSet.mem (head_evar t2) lev with NoHeadEvar -> false)
 
-(* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint
- * definitions. We try to unify the xi with the yi pairwise. The pairs
- * that don't unify are discarded (i.e. ?i is redefined so that it does not
- * depend on these args). *)
-
-let solve_refl conv_algo env evd evk argsv1 argsv2 =
-  if argsv1 = argsv2 then evd else
-  let evi = Evd.find_undefined evd evk in
-  (* Filter and restrict if needed *)
-  let evd,evk,args =
-    restrict_upon_filter evd evi evk
-      (fun (a1,a2) -> snd (conv_algo env evd Reduction.CONV a1 a2))
-      (List.combine (Array.to_list argsv1) (Array.to_list argsv2)) in
-  (* Leave a unification problem *)
-  let args1,args2 = List.split args in
-  let argsv1 = Array.of_list args1 and argsv2 = Array.of_list args2 in
-  let pb = (Reduction.CONV,env,mkEvar(evk,argsv1),mkEvar(evk,argsv2)) in
-  Evd.add_conv_pb pb evd
-
 (* Util *)
 
 let check_instance_type conv_algo env evd ev1 t2 =
@@ -1264,7 +1275,7 @@ let check_instance_type conv_algo env evd ev1 t2 =
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
 let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
   try
-    let t2 = whd_evar evd t2 in
+    let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
     let evd = match kind_of_term t2 with
       | Evar (evk2,args2 as ev2) ->
 	  if evk1 = evk2 then
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index a8cc7f745a..4aa00e689f 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -52,3 +52,18 @@ Hint Resolve -> a.
 Goal forall n, n=0 -> n<=0.
 auto.
 Qed.
+
+
+(* This example comes from Chlipala's ltamer *)
+(* It used to fail from r12902 to r13112 since type_of started to call *)
+(* e_cumul (instead of conv_leq) which was not able to unify "?id" and *)
+(* "(fun x => x) ?id" *)
+
+Notation "e :? pf" := (eq_rect _ (fun X : Set => X) e _ pf)
+  (no associativity, at level 90).
+
+Axiom cast_coalesce :
+  forall (T1 T2 T3 : Set) (e : T1) (pf1 : T1 = T2) (pf2 : T2 = T3),
+  ((e :? pf1) :? pf2) = (e :? trans_eq pf1 pf2).
+
+Hint Rewrite cast_coalesce : ltamer.