From cf44127379de49770232d6956b0455f92d6d6323 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 21 May 2017 01:49:43 +0200 Subject: Fixing #5500 (missing test in return clause of match leading to anomaly). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This is a quick fix to check in nested pattern-matching that the return clause is typed by an arity (there was already a check when the return clause was given explicitly - in the 3rd section of prepare_predicate -; it was automatically typed by a sort when the return clause was coming by pattern-matching with the type constraint, since the type constraint is a type; but it was not done when the predicate was derived from a former predicate in nested pattern-matching). Indeed, in nested pattern-matching, we know that the return predicate has the form λy1..yn.λx:I(y1,..,yn).T(y1,..,yn,x) and we know that T(v1,...,vn,u) : Type for the effective u:I(v1,..,vn) we are matching on, but we don't know if T(y1,..,yn,x) is itself a sort (e.g. it can be a "match" which reduces to a sort when instantiated with v1..vn, but whose evaluation remains blocked when the y1..yn are variables). Note that in the bug report, the incorrect typing is produced by small inversion. In practice, we can raise the anomaly also without small inversion, so we fix it in the general case. See file 5500.v for details. --- pretyping/typing.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 4c834f2f8..df189735b 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 -- cgit v1.2.3 From 414e4ea9f226ade9686da28ebee39cd1b93f42a6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 22 May 2017 10:13:47 +0200 Subject: Fixing #5547 (typability of return predicate in nested pattern-matching). Answering to commit about #5500: we don't know in general if the return predicate T(y1,..,yn,x) in the intermediate step of a nested pattern-matching is a sort, but we don't even know if it is well-typed: retyping is not enough, we need full typing. --- pretyping/cases.ml | 1 + test-suite/bugs/closed/5547.v | 16 ++++++++++++++++ 2 files changed, 17 insertions(+) create mode 100644 test-suite/bugs/closed/5547.v (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index a5b7a9e6f..a48889c6c 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1427,6 +1427,7 @@ and match_current pb (initial,tomatch) = let case = make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals in + let _ = Typing.e_type_of pb.env pb.evdref pred in Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; { uj_val = applist (case, inst); uj_type = prod_applist !(pb.evdref) typ inst } diff --git a/test-suite/bugs/closed/5547.v b/test-suite/bugs/closed/5547.v new file mode 100644 index 000000000..79633f489 --- /dev/null +++ b/test-suite/bugs/closed/5547.v @@ -0,0 +1,16 @@ +(* Checking typability of intermediate return predicates in nested pattern-matching *) + +Inductive A : (Type->Type) -> Type := J : A (fun x => x). +Definition ret (x : nat * A (fun x => x)) + := match x return Type with + | (y,z) => match z in A f return f Type with + | J => bool + end + end. +Definition foo : forall x, ret x. +Proof. +Fail refine (fun x + => match x return ret x with + | (y,J) => true + end + ). -- cgit v1.2.3