Hack to solve a "Bad recursive type" anomaly.

Retyping expects its argument already well-typed. However, if
unification problems are not fully solved, a term to match can have an
evar type together with the constraint that this evar has to be
convertible to some given inductive type.

One could have tried to have a more eager resolution of unification
constraint but I'm afraid of the cost in comparing c=c' in general in
"?x[c] = c'" unification problems, so I instead added a hack in
retyping to recover the constraint.

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

2 files changed, 29 insertions, 1 deletions

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index a49e2026a1..bb1a366376 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -45,6 +45,18 @@ let anomaly_on_error f x =
  try f x
  with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e)
 
+let get_type_from_constraints env sigma t =
+  if isEvar (fst (decompose_app t)) then
+    match
+      List.map_filter (fun (pbty,env,t1,t2) ->
+        if is_fconv Reduction.CONV env sigma t t1 then Some t2
+        else if is_fconv Reduction.CONV env sigma t t2 then Some t1
+        else None)
+        (snd (Evd.extract_all_conv_pbs sigma))
+    with
+    | t::l -> t
+    | _ -> raise Not_found
+  else raise Not_found
 
 let rec subst_type env sigma typ = function
   | [] -> typ
@@ -88,7 +100,12 @@ let retype ?(polyprop=true) sigma =
     | Construct cstr -> type_of_constructor env cstr
     | Case (_,p,c,lf) ->
         let Inductiveops.IndType(_,realargs) =
-          try Inductiveops.find_rectype env sigma (type_of env c)
+          let t = type_of env c in
+          try Inductiveops.find_rectype env sigma t
+          with Not_found ->
+          try
+            let t = get_type_from_constraints env sigma t in
+            Inductiveops.find_rectype env sigma t
           with Not_found -> retype_error BadRecursiveType
         in
         let t = whd_beta sigma (applist (p, realargs)) in
diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v
index 9a6ed71a54..c29e529783 100644
--- a/test-suite/success/Case19.v
+++ b/test-suite/success/Case19.v
@@ -6,3 +6,14 @@ Variable T : Type.
 Variable x : nat*nat.
 
 Check let (_, _) := x in sigT (fun _ : T => nat).
+
+(* This used to raise an anomaly in V8.4, up to pl2 *)
+
+Goal {x: nat & x=x}.
+Fail exists (fun x =>
+        match
+          projT2 (projT2 x) as e in (_ = y)
+          return _ = existT _ (projT1 x) (existT _ y e)
+        with
+        | eq_refl => eq_refl
+        end).