Fix #8459: anomaly not enough abstractions in fix body

We reach the anomaly because we call check_fix on a surrounding
fixpoint from the pretyper, and the inner fix hasn't been checked.

Using whd_all isn't useful in the specific reported case but a case
where it's necessary can probably be crafted.

See also #11013

2 files changed, 37 insertions, 8 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index cd969ea457..9c2af7aebb 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -885,6 +885,9 @@ let filter_stack_domain env p stack =
   in
   filter_stack env ar stack
 
+let judgment_of_fixpoint (_, types, bodies) =
+  Array.map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies
+
 (* Check if [def] is a guarded fixpoint body with decreasing arg.
    given [recpos], the decreasing arguments of each mutually defined
    fixpoint. *)
@@ -982,7 +985,12 @@ let check_one_fix renv recpos trees def =
                 if Int.equal i j && (List.length stack' > decrArg) then
                   let recArg = List.nth stack' decrArg in
                   let arg_sp = stack_element_specif recArg in
-                  check_nested_fix_body renv' (decrArg+1) arg_sp body
+                  let illformed () =
+                    error_ill_formed_rec_body renv.env NotEnoughAbstractionInFixBody
+                      (pi1 recdef) i (push_rec_types recdef renv.env)
+                      (judgment_of_fixpoint recdef)
+                  in
+                  check_nested_fix_body illformed renv' (decrArg+1) arg_sp body
                 else check_rec_call renv' [] body)
             with (FixGuardError _ as exn) ->
               let exn = CErrors.push exn in
@@ -1065,23 +1073,20 @@ let check_one_fix renv recpos trees def =
 
         | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *)
 
-  and check_nested_fix_body renv decr recArgsDecrArg body =
+  and check_nested_fix_body illformed renv decr recArgsDecrArg body =
     if Int.equal decr 0 then
       check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
     else
-      match kind body with
+      match kind (whd_all renv.env body) with
         | Lambda (x,a,b) ->
 	    check_rec_call renv [] a;
             let renv' = push_var_renv renv (x,a) in
-	      check_nested_fix_body renv' (decr-1) recArgsDecrArg b
-	| _ -> anomaly (Pp.str "Not enough abstractions in fix body.")
+              check_nested_fix_body illformed renv' (decr-1) recArgsDecrArg b
+        | _ -> illformed ()
 	    
   in
   check_rec_call renv [] def
 
-let judgment_of_fixpoint (_, types, bodies) =
-  Array.map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies
-
 let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
   let nbfix = Array.length bodies in
   if Int.equal nbfix 0
diff --git a/test-suite/bugs/closed/bug_8459.v b/test-suite/bugs/closed/bug_8459.v
new file mode 100644
index 0000000000..62c49e9ea7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8459.v
@@ -0,0 +1,24 @@
+Require Import Coq.Vectors.Vector.
+
+Axiom exfalso : False.
+
+Fixpoint all_then_someV (n:nat) (l:Vector.t bool n) {struct l}:
+(Vector.fold_left orb false l) = false ->
+(forall p, (Vector.nth l p  ) = false).
+Proof.
+intros.
+destruct l.
+inversion p.
+revert h l H.
+set (P := fun n p => forall (h : bool) (l : t bool n),
+fold_left orb false (cons bool h n l) = false -> @eq bool (@nth bool (S n) (cons bool h n l) p) false).
+revert n p.
+fix loop 1.
+unshelve eapply (@Fin.rectS P).
++ elim exfalso.
++ unfold P.
+  intros.
+  eapply all_then_someV.
+  exact H0.
+Fail Defined.
+Abort.