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.

1 files changed, 16 insertions, 0 deletions

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
+         ).