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, 5 insertions, 2 deletions

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 4c834f2f8..df189735b 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -184,10 +184,13 @@ let check_type_fixpoint ?loc env evdref lna lar vdefj =
 
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
-  let pj = Retyping.get_judgment_of env sigma p in
-  let ksort = Sorts.family (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in
   let specif = Global.lookup_inductive (fst ind) in
   let sorts = elim_sorts specif in
+  let pj = Retyping.get_judgment_of env sigma p in
+  let _, s = splay_prod env sigma pj.uj_type in
+  let ksort = match EConstr.kind sigma s with
+  | Sort s -> Sorts.family (ESorts.kind sigma s)
+  | _ -> error_elim_arity env sigma ind sorts c pj None in
   if not (List.exists ((==) ksort) sorts) then
     let s = inductive_sort_family (snd specif) in
     error_elim_arity env sigma ind sorts c pj