diff options
| author | herbelin | 2013-05-05 22:47:39 +0000 |
|---|---|---|
| committer | herbelin | 2013-05-05 22:47:39 +0000 |
| commit | 742ef62fe8050a6865d06bd644e30cbec0e7eb02 (patch) | |
| tree | 7b8db9bbebcb92e59a68bbb7508184dc574dc643 /pretyping | |
| parent | df313cefbaddb57f89650171e59e3abcb168a273 (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/retyping.ml | 19 |
1 files changed, 18 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 |