diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /test-suite/bugs/closed/5500.v | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'test-suite/bugs/closed/5500.v')
-rw-r--r-- | test-suite/bugs/closed/5500.v | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5500.v b/test-suite/bugs/closed/5500.v new file mode 100644 index 00000000..aa63e2ab --- /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. |