diff options
| -rw-r--r-- | pretyping/typing.ml | 7 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5500.v | 35 |
2 files changed, 40 insertions, 2 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 4c834f2f8f..df189735b7 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -184,10 +184,13 @@ let check_type_fixpoint ?loc env evdref lna lar vdefj = (* 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 - let ksort = Sorts.family (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in let specif = Global.lookup_inductive (fst ind) in let sorts = elim_sorts specif in + let pj = Retyping.get_judgment_of env sigma p in + let _, s = splay_prod env sigma pj.uj_type in + let ksort = match EConstr.kind sigma s with + | Sort s -> Sorts.family (ESorts.kind sigma s) + | _ -> error_elim_arity env sigma ind sorts c pj None in if not (List.exists ((==) ksort) sorts) then let s = inductive_sort_family (snd specif) in error_elim_arity env sigma ind sorts c pj diff --git a/test-suite/bugs/closed/5500.v b/test-suite/bugs/closed/5500.v new file mode 100644 index 0000000000..aa63e2ab0e --- /dev/null +++ b/test-suite/bugs/closed/5500.v @@ -0,0 +1,35 @@ +(* Too weak check on the correctness of return clause was leading to an anomaly *) + +Inductive Vector A: nat -> Type := + nil: Vector A O +| cons: forall n, A -> Vector A n -> Vector A (S n). + +(* This could be made working with a better inference of inner return + predicates from the return predicate at the higher level of the + nested matching. Currently, we only check that it does not raise an + anomaly, but eventually, the "Fail" could be removed. *) + +Fail Definition hd_fst A x n (v: A * Vector A (S n)) := + match v as v0 return match v0 with + (l, r) => + match r in Vector _ n return match n with 0 => Type | S _ => Type end with + nil _ => A + | cons _ _ _ _ => A + end + end with + (_, nil _) => x + | (_, cons _ n hd tl) => hd + end. + +(* This is another example of failure but involving beta-reduction and + not iota-reduction. Thus, for this one, I don't see how it could be + solved by small inversion, whatever smart is small inversion. *) + +Inductive A : (Type->Type) -> Type := J : A (fun x => x). + +Fail Check fun x : nat * A (fun x => x) => + match x return match x with + (y,z) => match z in A f return f Type with J => bool end + end with + (y,J) => true + end. |