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

Author: mattam82

dev/ci/user-overlays/00664-herbelin-master+change-for-coq-pr664-compatibility.sh

@@ -0,0 +1,4 @@
+ if [ "$CI_PULL_REQUEST" = "664" ] || [ "$CI_BRANCH" = "trunk+fix-5500-too-weak-test-return-clause" ]; then
+    fiat_parsers_CI_BRANCH=master+change-for-coq-pr664-compatibility
+    fiat_parsers_CI_GITURL=https://github.com/herbelin/fiat
+fi

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 }

pretyping/typing.ml

@@ -197,10 +197,13 @@ let check_type_fixpoint ?loc env sigma 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

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.

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