Inductives in SProp, forbid primitive records with only sprop fields

For nonsquashed:
Either
- 0 constructors
- primitive record

6 files changed, 106 insertions, 51 deletions

diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 5e294c9729..ff2c91d913 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -122,39 +122,53 @@ let check_cumulativity univs variances env_ar params data =
 (************************** Type checking *******************************)
 (************************************************************************)
 
-type univ_info = { ind_squashed : bool;
+type univ_info = { ind_squashed : bool; ind_has_relevant_arg : bool;
                    ind_min_univ : Universe.t option; (* Some for template *)
                    ind_univ : Universe.t }
 
-let check_univ_leq env u info =
+let check_univ_leq ?(is_real_arg=false) env u info =
   let ind_univ = info.ind_univ in
-  if type_in_type env || (UGraph.check_leq (universes env) u ind_univ)
+  let info = if not info.ind_has_relevant_arg && is_real_arg && not (Univ.Universe.is_sprop u)
+    then {info with ind_has_relevant_arg=true}
+    else info
+  in
+  (* Inductive types provide explicit lifting from SProp to other universes, so allow SProp <= any. *)
+  if type_in_type env || Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ
   then { info with ind_min_univ = Option.map (Universe.sup u) info.ind_min_univ }
   else if is_impredicative_univ env ind_univ
   then if Option.is_empty info.ind_min_univ then { info with ind_squashed = true }
     else raise (InductiveError BadUnivs)
   else raise (InductiveError BadUnivs)
 
-let check_indices_matter env_params info indices =
-  let check_index d (info,env) =
+let check_context_univs ~ctor env info ctx =
+  let check_one d (info,env) =
     let info = match d with
       | LocalAssum (_,t) ->
         (* could be retyping if it becomes available in the kernel *)
         let tj = Typeops.infer_type env t in
-        check_univ_leq env (Sorts.univ_of_sort tj.utj_type) info
+        check_univ_leq ~is_real_arg:ctor env (Sorts.univ_of_sort tj.utj_type) info
       | LocalDef _ -> info
     in
     info, push_rel d env
   in
+  fst (Context.Rel.fold_outside ~init:(info,env) check_one ctx)
+
+let check_indices_matter env_params info indices =
   if not (indices_matter env_params) then info
-  else fst (Context.Rel.fold_outside ~init:(info,env_params) check_index indices)
+  else check_context_univs ~ctor:false env_params info indices
 
 (* env_ar contains the inductives before the current ones in the block, and no parameters *)
 let check_arity env_params env_ar ind =
   let {utj_val=arity;utj_type=_} = Typeops.infer_type env_params ind.mind_entry_arity in
   let indices, ind_sort = Reduction.dest_arity env_params arity in
   let ind_min_univ = if ind.mind_entry_template then Some Universe.type0m else None in
-  let univ_info = {ind_squashed=false;ind_min_univ;ind_univ=Sorts.univ_of_sort ind_sort} in
+  let univ_info = {
+    ind_squashed=false;
+    ind_has_relevant_arg=false;
+    ind_min_univ;
+    ind_univ=Sorts.univ_of_sort ind_sort;
+  }
+  in
   let univ_info = check_indices_matter env_params univ_info indices in
   (* We do not need to generate the universe of the arity with params;
      if later, after the validation of the inductive definition,
@@ -165,31 +179,49 @@ let check_arity env_params env_ar ind =
   push_rel (LocalAssum (x, arity)) env_ar,
   (arity, indices, univ_info)
 
-let check_constructor_univs env_ar_par univ_info (args,_) =
+let check_constructor_univs env_ar_par info (args,_) =
   (* We ignore the output, positivity will check that it's the expected inductive type *)
-  (* NB: very similar to check_indices_matter but that will change with SProp *)
-  fst (Context.Rel.fold_outside ~init:(univ_info,env_ar_par) (fun d (univ_info,env) ->
-      let univ_info = match d with
-        | LocalDef _ -> univ_info
-        | LocalAssum (_,t) ->
-          (* could be retyping if it becomes available in the kernel *)
-          let tj = Typeops.infer_type env t in
-          check_univ_leq env (Sorts.univ_of_sort tj.utj_type) univ_info
-      in
-      univ_info, push_rel d env)
-      args)
-
-let check_constructors env_ar_par params lc (arity,indices,univ_info) =
+  check_context_univs ~ctor:true env_ar_par info args
+
+let check_constructors env_ar_par isrecord params lc (arity,indices,univ_info) =
   let lc = Array.map_of_list (fun c -> (Typeops.infer_type env_ar_par c).utj_val) lc in
   let splayed_lc = Array.map (Reduction.dest_prod_assum env_ar_par) lc in
-  let univ_info = if Array.length lc <= 1 then univ_info
-    else check_univ_leq env_ar_par Univ.Universe.type0 univ_info
+  let univ_info = match Array.length lc with
+    (* Empty type: all OK *)
+    | 0 -> univ_info
+
+    (* SProp primitive records are OK, if we squash and become fakerecord also OK *)
+    | 1 when isrecord -> univ_info
+
+    (* Unit and identity types must squash if SProp *)
+    | 1 -> check_univ_leq env_ar_par Univ.Universe.type0m univ_info
+
+    (* More than 1 constructor: must squash if Prop/SProp *)
+    | _ -> check_univ_leq env_ar_par Univ.Universe.type0 univ_info
   in
   let univ_info = Array.fold_left (check_constructor_univs env_ar_par) univ_info splayed_lc in
   (* generalize the constructors over the parameters *)
   let lc = Array.map (fun c -> Term.it_mkProd_or_LetIn c params) lc in
   (arity, lc), (indices, splayed_lc), univ_info
 
+let check_record data =
+  List.for_all (fun (_,(_,splayed_lc),info) ->
+      (* records must have all projections definable -> equivalent to not being squashed *)
+      not info.ind_squashed
+      (* relevant records must have at least 1 relevant argument *)
+      && (Univ.Universe.is_sprop info.ind_univ
+          || info.ind_has_relevant_arg)
+      && (match splayed_lc with
+          (* records must have 1 constructor with at least 1 argument, and no anonymous fields *)
+          | [|ctx,_|] ->
+            let module D = Context.Rel.Declaration in
+            List.exists D.is_local_assum ctx &&
+            List.for_all (fun d -> not (D.is_local_assum d)
+                                   || not (Name.is_anonymous (D.get_name d)))
+              ctx
+          | _ -> false))
+    data
+
 (* Allowed eliminations *)
 
 (* Previous comment: *)
@@ -205,7 +237,7 @@ let small_sorts = [InSProp;InProp;InSet]
 let logical_sorts = [InSProp;InProp]
 let sprop_sorts = [InSProp]
 
-let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_} =
+let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_} =
   if not ind_squashed then all_sorts
   else match Sorts.family (Sorts.sort_of_univ ind_univ) with
     | InType -> assert false
@@ -279,10 +311,31 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
   let env_ar_par = push_rel_context params env_ar in
 
   (* Constructors *)
-  let data = List.map2 (fun ind data -> check_constructors env_ar_par params ind.mind_entry_lc data)
+  let isrecord = match mie.mind_entry_record with
+    | Some (Some _) -> true
+    | Some None | None -> false
+  in
+  let data = List.map2 (fun ind data ->
+      check_constructors env_ar_par isrecord params ind.mind_entry_lc data)
       mie.mind_entry_inds data
   in
 
+  let record = mie.mind_entry_record in
+  let data, record = match record with
+    | None | Some None -> data, record
+    | Some (Some _) ->
+      if check_record data then
+        data, record
+      else
+        (* if someone tried to declare a record as SProp but it can't
+           be primitive we must squash. *)
+        let data = List.map (fun (a,b,univs) ->
+            a,b,check_univ_leq env_ar_par Univ.Universe.type0m univs)
+            data
+        in
+        data, Some None
+  in
+
   let () = match mie.mind_entry_variance with
     | None -> ()
     | Some variances ->
@@ -301,4 +354,4 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
     Environ.push_rel_context ctx env
   in
 
-  env_ar_par, univs, mie.mind_entry_variance, params, Array.of_list data
+  env_ar_par, univs, mie.mind_entry_variance, record, params, Array.of_list data
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 2598548f3f..ad51af66a2 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -17,6 +17,7 @@ open Declarations
     - environment with inductives + parameters in rel context
     - abstracted universes
     - checked variance info
+    - record entry (checked to be OK)
     - parameters
     - for each inductive,
       (arity * constructors) (with params)
@@ -26,6 +27,7 @@ open Declarations
 val typecheck_inductive : env -> mutual_inductive_entry ->
   env
   * universes * Univ.Variance.t array option
+  * Names.Id.t array option option
   * Constr.rel_context
   * ((inductive_arity * Constr.types array) *
      (Constr.rel_context * (Constr.rel_context * Constr.types) array) *
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 545c0fe7b7..3173dc5383 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -408,8 +408,6 @@ let used_section_variables env inds =
 let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
 let rel_list n m = Array.to_list (rel_vect n m)
 
-exception UndefinableExpansion
-
 (** From a rel context describing the constructor arguments,
     build an expansion function.
     The term built is expecting to be substituted first by 
@@ -464,7 +462,7 @@ let compute_projections (kn, i as ind) mib =
            to [params, x:I |- t(proj1 x,..,projj x)] *)
 	let fterm = mkProj (Projection.make kn false, mkRel 1) in
         (i + 1, j + 1, lab :: labs, r :: rs, projty :: pbs, fterm :: letsubst)
-      | Anonymous -> raise UndefinableExpansion
+      | Anonymous -> assert false (* checked by indTyping *)
   in
   let (_, _, labs, rs, pbs, _letsubst) =
     List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst)
@@ -543,24 +541,12 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
   in
   let record_info = match isrecord with
   | Some (Some rid) ->
-    let is_record pkt =
-      if Array.length pkt.mind_consnames != 1 then
-        user_err ~hdr:"build_inductive"
-          Pp.(str "Primitive records must have exactly one constructor.")
-      else if pkt.mind_consnrealargs.(0) = 0 then
-        user_err ~hdr:"build_inductive"
-          Pp.(str "Primitive records must have at least one constructor argument.")
-      else List.exists (Sorts.family_equal Sorts.InType) pkt.mind_kelim
-    in
     (** The elimination criterion ensures that all projections can be defined. *)
-    if Array.for_all is_record packets then
-      let map i id =
-        let labs, rs, projs = compute_projections (kn, i) mib in
-        (id, labs, rs, projs)
-      in
-      try PrimRecord (Array.mapi map rid)
-      with UndefinableExpansion -> FakeRecord
-    else FakeRecord
+    let map i id =
+      let labs, rs, projs = compute_projections (kn, i) mib in
+      (id, labs, rs, projs)
+    in
+    PrimRecord (Array.mapi map rid)
   | Some None -> FakeRecord
   | None -> NotRecord
   in
@@ -571,7 +557,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
 
 let check_inductive env kn mie =
   (* First type-check the inductive definition *)
-  let (env_ar_par, univs, variance, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in
+  let (env_ar_par, univs, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in
   (* Then check positivity conditions *)
   let chkpos = (Environ.typing_flags env).check_guarded in
   let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames)
@@ -583,5 +569,5 @@ let check_inductive env kn mie =
   in
   (* Build the inductive packets *)
     build_inductive env names mie.mind_entry_private univs variance
-      paramsctxt kn mie.mind_entry_record mie.mind_entry_finite
+      paramsctxt kn record mie.mind_entry_finite
       inds nmr recargs
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 8b8295c64b..2d34c02302 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1075,8 +1075,19 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
                 (mind, (env', b))
 	      else check_occur env' (n+1) b
             else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.")
-        | _ -> raise_err env i NotEnoughAbstractionInFixBody in
-    check_occur fixenv 1 def in
+        | _ -> raise_err env i NotEnoughAbstractionInFixBody
+    in
+    let ((ind, _), _) as res = check_occur fixenv 1 def in
+    let _, ind = lookup_mind_specif env ind in
+    (* recursive sprop means non record with projections -> squashed *)
+    if Sorts.Irrelevant == ind.mind_relevant
+    then
+      begin
+        if names.(i).Context.binder_relevance == Sorts.Relevant
+        then raise_err env i FixpointOnIrrelevantInductive
+      end;
+    res
+  in
   (* Do it on every fixpoint *)
   let rv = Array.map2_i find_ind nvect bodies in
   (Array.map fst rv, Array.map snd rv)
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 9168c32f0e..c45fe1cf00 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -33,6 +33,7 @@ type 'constr pguard_error =
   | RecCallInCasePred of 'constr
   | NotGuardedForm of 'constr
   | ReturnPredicateNotCoInductive of 'constr
+  | FixpointOnIrrelevantInductive
 
 type guard_error = constr pguard_error
 
@@ -173,6 +174,7 @@ let map_pguard_error f = function
 | RecCallInCasePred c -> RecCallInCasePred (f c)
 | NotGuardedForm c -> NotGuardedForm (f c)
 | ReturnPredicateNotCoInductive c -> ReturnPredicateNotCoInductive (f c)
+| FixpointOnIrrelevantInductive -> FixpointOnIrrelevantInductive
 
 let map_ptype_error f = function
 | UnboundRel n -> UnboundRel n
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 41a5f19e78..88165a4f07 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -34,6 +34,7 @@ type 'constr pguard_error =
   | RecCallInCasePred of 'constr
   | NotGuardedForm of 'constr
   | ReturnPredicateNotCoInductive of 'constr
+  | FixpointOnIrrelevantInductive
 
 type guard_error = constr pguard_error