Primitive projections: protect kernel from erroneous definitions.

E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive
records with eta for which conversion is incomplete.

- Eta-conversion only applies to BiFinite inductives
- Finiteness information is now checked by the kernel (the constructor types
  must be strictly non recursive for BiFinite declarations).

5 files changed, 17 insertions, 26 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 2ba80d8362..93e63d0fb5 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -784,7 +784,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
     | Some (Some (_,projs,pbs)) when
-	mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> 
+	mib.Declarations.mind_finite == Decl_kinds.BiFinite -> 
 	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
 	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
       let pars = mib.Declarations.mind_nparams in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 49e8583158..acf5ab17d3 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -452,7 +452,7 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else
 
 (* The recursive function that checks positivity and builds the list
    of recursive arguments *)
-let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
+let check_positivity_one recursive (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
   let lparams = rel_context_length hyps in
   let nmr = rel_context_nhyps hyps in
   (* Checking the (strict) positivity of a constructor argument type [c] *)
@@ -538,6 +538,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
 
           | Prod (na,b,d) ->
 	      let () = assert (List.is_empty largs) in
+	      if not recursive && not (noccur_between n ntypes b) then
+	        raise (InductiveError BadEntry);
               let nmr',recarg = check_pos ienv nmr b in
               let ienv' = ienv_push_var ienv (na,b,mk_norec) in
                 check_constr_rec ienv' nmr' (recarg::lrec) d
@@ -570,9 +572,11 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
   and nmr' = array_min nmr irecargs_nmr
   in (nmr', mk_paths (Mrec ind) irecargs)
 
-let check_positivity kn env_ar params inds =
+let check_positivity kn env_ar params finite inds =
   let ntypes = Array.length inds in
-  let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
+  let recursive = finite != Decl_kinds.BiFinite in
+  let rc = Array.mapi (fun j t -> (Mrec (kn,j),t))
+		      (Rtree.mk_rec_calls ntypes) in
   let lra_ind = Array.rev_to_list rc in
   let lparams = rel_context_length params in
   let nmr = rel_context_nhyps params in
@@ -581,7 +585,7 @@ let check_positivity kn env_ar params inds =
       List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
     let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
     let nargs = rel_context_nhyps sign - nmr in
-    check_positivity_one ienv params (kn,i) nargs lcnames lc
+    check_positivity_one recursive ienv params (kn,i) nargs lcnames lc
   in
   let irecargs_nmr = Array.mapi check_one inds in
   let irecargs = Array.map snd irecargs_nmr
@@ -807,10 +811,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
 	mind_reloc_tbl = rtbl;
       } in
   let packets = Array.map2 build_one_packet inds recargs in
-  let pkt = packets.(0) in	  
+  let pkt = packets.(0) in
   let isrecord = 
     match isrecord with
-    | Some (Some rid) when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1
+    | Some (Some rid) when pkt.mind_kelim == all_sorts
+			   && Array.length pkt.mind_consnames == 1
 			   && pkt.mind_consnrealargs.(0) > 0 ->
       (** The elimination criterion ensures that all projections can be defined. *)
       let u = 
@@ -851,7 +856,7 @@ let check_inductive env kn mie =
   (* First type-check the inductive definition *)
   let (env_ar, env_ar_par, params, inds) = typecheck_inductive env mie in
   (* Then check positivity conditions *)
-  let (nmr,recargs) = check_positivity kn env_ar_par params inds in
+  let (nmr,recargs) = check_positivity kn env_ar_par params mie.mind_entry_finite inds in
   (* Build the inductive packets *)
     build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
       mie.mind_entry_universes
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 637a9e50e0..690b974be5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -854,7 +854,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
 and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
-    | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> 
+    | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite -> 
       let pars = mib.Declarations.mind_nparams in
 	(try 
 	   let l1' = Stack.tail pars sk1 in
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index fd51fd6b0f..4d9d40ae08 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -215,8 +215,8 @@ let print_polymorphism ref =
 let print_primitive_record recflag mipv = function
   | Some (Some (_, ps,_)) ->
     let eta = match recflag with
-    | Decl_kinds.CoFinite -> mt ()
-    | Decl_kinds.Finite | Decl_kinds.BiFinite -> str " and has eta conversion"
+    | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt ()
+    | Decl_kinds.BiFinite -> str " and has eta conversion"
     in
     [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
   | _ -> []
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 281d707cb3..b5e6ccd618 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -35,10 +35,6 @@ Set Implicit Arguments.
 
 Check nat.
 
-(* Inductive X (U:Type) := Foo (k : nat) (x : X U).  *)
-(* Parameter x : X nat. *)
-(* Check x.(k). *)
-
 Inductive X (U:Type) := { k : nat; a: k = k -> X U; b : let x := a eq_refl in X U }.
 
 Parameter x:X nat.
@@ -49,18 +45,8 @@ Inductive Y := { next : option Y }.
 
 Check _.(next) : option Y.
 Lemma eta_ind (y : Y) : y = Build_Y y.(next).
-Proof. reflexivity. Defined.
-
-Variable t : Y.
-
-Fixpoint yn (n : nat) (y : Y) : Y := 
-  match n with
-    | 0 => t
-    | S n => {| next := Some (yn n y) |}
-  end.
+Proof. Fail reflexivity. Abort.
 
-Lemma eta_ind'  (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}.
-Proof. reflexivity. Defined.
 
 
 (*