Fix #3824. de Bruijn error in normalization of fixpoints.

This bug was affecting the VM and the native compiler, but only in the pretyper
(not the kernel). Types of arguments of fixpoints were incorrectly normalized
due to a missing lift.

2 files changed, 12 insertions, 3 deletions

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 024af30ae..274357adb 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -312,12 +312,17 @@ and nf_atom_type env atom =
       let ci = ans.asw_ci in
       mkCase(ci, p, a, branchs), tcase 
   | Afix(tt,ft,rp,s) ->
-      let tt = Array.map (nf_type env) tt in
+      let tt = Array.map (fun t -> nf_type env t) tt in
       let name = Array.map (fun _ -> (Name (id_of_string "Ffix"))) tt in
       let lvl = nb_rel env in
+      let nbfix = Array.length ft in
       let fargs = mk_rels_accu lvl (Array.length ft) in
+      (* Third argument of the tuple is ignored by push_rec_types *)
       let env = push_rec_types (name,tt,[||]) env in
-      let ft = Array.mapi (fun i v -> nf_val env (napply v fargs) tt.(i)) ft in
+      (* We lift here because the types of arguments (in tt) will be evaluated
+         in an environment where the fixpoints have been pushed *)
+      let norm_body i v = nf_val env (napply v fargs) (lift nbfix tt.(i)) in
+      let ft = Array.mapi norm_body ft in
       mkFix((rp,s),(name,tt,ft)), tt.(s)
   | Acofix(tt,ft,s,_) | Acofixe(tt,ft,s,_) ->
       let tt = Array.map (nf_type env) tt in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index be4ad7dbb..c3a1f0d94 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -275,8 +275,12 @@ and nf_fix env f =
   let ndef = Array.length vt in
   let ft = Array.map (fun v -> nf_val env v crazy_type) vt in
   let name = Array.init ndef (fun _ -> (Name (Id.of_string "Ffix"))) in
+  (* Third argument of the tuple is ignored by push_rec_types *)
   let env = push_rec_types (name,ft,ft) env in
-  let fb = Util.Array.map2 (fun v t -> nf_fun env v t) vb ft in
+  (* We lift here because the types of arguments (in tt) will be evaluated
+     in an environment where the fixpoints have been pushed *)
+  let norm_vb v t = nf_fun env v (lift ndef t) in
+  let fb = Util.Array.map2 norm_vb vb ft in
   mkFix ((rec_args,init),(name,ft,fb))
 
 and nf_fix_app env f vargs =