Fixing #5500 (missing test in return clause of match leading to anomaly).

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.

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