From 3910e8dca2154d15c422a8e5ceb16f93c5faf889 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 31 Oct 2019 13:17:15 +0100
Subject: 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
---
 kernel/inductive.ml | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3