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.

2 files changed, 17 insertions, 0 deletions

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