diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-09-10 11:31:01 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-09-10 11:34:08 +0200 |
commit | 43104a0b94e42fb78764b5d1365ca1e85a158508 (patch) | |
tree | 68943411671327facf236b25c6cabd63b96f90d0 | |
parent | 7a037b8c1de11b18d47b01e5b0262090f32bfc40 (diff) |
Fixing #5077 (failure on typing a fixpoint with evars in its type).
Typing.type_of was using conversion for types of fixpoints while it
could have used unification.
-rw-r--r-- | pretyping/pretyping.ml | 17 | ||||
-rw-r--r-- | pretyping/typing.ml | 12 | ||||
-rw-r--r-- | pretyping/typing.mli | 5 |
3 files changed, 17 insertions, 17 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d6f8f0de5..2e164e540 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -267,21 +267,6 @@ let process_inference_flags flags env initial_sigma (sigma,c) = (* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) let allow_anonymous_refs = ref false -(* Utilisé pour inférer le prédicat des Cases *) -(* Semble exagérement fort *) -(* Faudra préférer une unification entre les types de toutes les clauses *) -(* et autoriser des ? à rester dans le résultat de l'unification *) - -let evar_type_fixpoint loc env evdref lna lar vdefj = - let lt = Array.length vdefj in - if Int.equal (Array.length lar) lt then - for i = 0 to lt-1 do - if not (e_cumul env evdref (vdefj.(i)).uj_type - (lift lt lar.(i))) then - error_ill_typed_rec_body_loc loc env !evdref - i lna vdefj lar - done - (* coerce to tycon if any *) let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function | None -> j @@ -579,7 +564,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in - evar_type_fixpoint loc env evdref names ftys vdefj; + Typing.check_type_fixpoint loc env evdref names ftys vdefj; let ftys = Array.map (nf_evar !evdref) ftys in let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in let fixj = match fixkind with diff --git a/pretyping/typing.ml b/pretyping/typing.ml index eb16628b1..bb3f19859 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -126,6 +126,16 @@ let e_judge_of_case env evdref ci pj cj lfj = { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } +let check_type_fixpoint loc env evdref lna lar vdefj = + let lt = Array.length vdefj in + if Int.equal (Array.length lar) lt then + for i = 0 to lt-1 do + if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type + (lift lt lar.(i))) then + Pretype_errors.error_ill_typed_rec_body_loc loc env !evdref + i lna vdefj lar + done + (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = let pj = Retyping.get_judgment_of env sigma p in @@ -263,7 +273,7 @@ and execute_recdef env evdref (names,lar,vdef) = let env1 = push_rec_types (names,lara,vdef) env in let vdefj = execute_array env1 evdref vdef in let vdefv = Array.map j_val vdefj in - let _ = type_fixpoint env1 names lara vdefj in + let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in (names,lara,vdefv) and execute_array env evdref = Array.map (execute env evdref) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index dafd75231..22cb7f3b9 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -39,3 +39,8 @@ val solve_evars : env -> evar_map ref -> constr -> constr (** (first constr is term to match, second is return predicate) *) val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr -> unit + +(** Raise an error message if bodies have types not unifiable with the + expected ones *) +val check_type_fixpoint : Loc.t -> env -> evar_map ref -> + Names.Name.t array -> types array -> unsafe_judgment array -> unit |