Merge PR #664: Fixing #5500 (missing test in return clause of match leading to anomaly)

2 files changed, 51 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/5500.v b/test-suite/bugs/closed/5500.v
new file mode 100644
index 000000000..aa63e2ab0
--- /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.
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
+         ).