diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-11 14:27:56 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-11 14:27:56 +0000 |
| commit | 0c0c605756d4c1f05b8ddf0d9ff7ad2f4926772a (patch) | |
| tree | 22e005f4426081d40f326ea8c2e65f84c8faa4e8 | |
| parent | 5a413714ae4dc63265f0d24663402d5dde1194a1 (diff) | |
Catch NotArity exception and transform it into an anomaly in retyping.
Add a temporary fix in solve_simple_eqn to catch anomalies
coming from retyping because the unification algorithm with metas
doesn't respect the precondition that evar instances should be
well-typed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13985 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarutil.ml | 26 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 10 |
2 files changed, 21 insertions, 15 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 1df6a3d4e..d2c05b913 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1322,17 +1322,21 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1) let evc = nf_evar evd evi.evar_concl in match evi.evar_body with | Evar_defined body -> - let ty = nf_evar evd (Retyping.get_type_of evenv evd body) in - if occur_existential evd evi.evar_concl - || occur_existential evd ty - then add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd - else - let evd,b = conv_algo evenv evd Reduction.CUMUL ty evc in - if b then evd else - user_err_loc (fst (evar_source (fst ev1) evd),"", - str "Unable to find a well-typed instantiation") - | Evar_empty -> (* Resulted in a constraint *) - evd + (* FIXME: The body might be ill-typed when this is called from w_merge *) + let ty = + try Retyping.get_type_of evenv evd body + with _ -> error "Ill-typed evar instance" + in + let ty = nf_evar evd ty in + if occur_existential evd evi.evar_concl + || occur_existential evd ty + then add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd + else + let evd,b = conv_algo evenv evd Reduction.CUMUL ty evc in + if b then evd else + user_err_loc (fst (evar_source (fst ev1) evd),"", + str "Unable to find a well-typed instantiation") + | Evar_empty -> evd (* Resulted in a constraint *) in let (evd,pbs) = extract_changed_conv_pbs evd status_changed in List.fold_left diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index c1d201736..62cd844d8 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -46,8 +46,8 @@ let retype sigma = let rec type_of env cstr= match kind_of_term cstr with | Meta n -> - (try strip_outer_cast (Evd.meta_ftype sigma n).Evd.rebus - with Not_found -> anomaly ("type_of: unknown meta " ^ string_of_int n)) + (try strip_outer_cast (Evd.meta_ftype sigma n).Evd.rebus + with Not_found -> anomaly ("type_of: unknown meta " ^ string_of_int n)) | Rel n -> let (_,_,ty) = lookup_rel n env in lift n ty @@ -127,10 +127,12 @@ let retype sigma = match kind_of_term c with | Ind ind -> let (_,mip) = lookup_mind_specif env ind in - Inductive.type_of_inductive_knowing_parameters env mip argtyps + (try Inductive.type_of_inductive_knowing_parameters env mip argtyps + with Reduction.NotArity -> anomaly "type_of: Not an arity") | Const cst -> let t = constant_type env cst in - Typeops.type_of_constant_knowing_parameters env t argtyps + (try Typeops.type_of_constant_knowing_parameters env t argtyps + with Reduction.NotArity -> anomaly "type_of: Not an arity") | Var id -> type_of_var env id | Construct cstr -> type_of_constructor env cstr | _ -> assert false |