Inductives in SProp, forbid primitive records with only sprop fields

For nonsquashed:
Either
- 0 constructors
- primitive record

11 files changed, 270 insertions, 80 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
 
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index f4544a0df3..ffba1d35cc 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -1,59 +1,72 @@
 le_n: forall n : nat, n <= n
 le_0_n: forall n : nat, 0 <= n
 le_S: forall n m : nat, n <= m -> n <= S m
-le_n_S: forall n m : nat, n <= m -> S n <= S m
-le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
 le_S_n: forall n m : nat, S n <= S m -> n <= m
-min_l: forall n m : nat, n <= m -> Nat.min n m = n
+le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
+le_n_S: forall n m : nat, n <= m -> S n <= S m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
 max_r: forall n m : nat, n <= m -> Nat.max n m = m
 min_r: forall n m : nat, m <= n -> Nat.min n m = m
-max_l: forall n m : nat, m <= n -> Nat.max n m = n
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
 le_ind:
   forall (n : nat) (P : nat -> Prop),
   P n ->
   (forall m : nat, n <= m -> P m -> P (S m)) ->
   forall n0 : nat, n <= n0 -> P n0
+le_sind:
+  forall (n : nat) (P : nat -> SProp),
+  P n ->
+  (forall m : nat, n <= m -> P m -> P (S m)) ->
+  forall n0 : nat, n <= n0 -> P n0
 false: bool
 true: bool
+eq_true: bool -> Prop
 is_true: bool -> Prop
 negb: bool -> bool
-eq_true: bool -> Prop
-implb: bool -> bool -> bool
-orb: bool -> bool -> bool
 andb: bool -> bool -> bool
+orb: bool -> bool -> bool
+implb: bool -> bool -> bool
 xorb: bool -> bool -> bool
 Nat.even: nat -> bool
 Nat.odd: nat -> bool
 BoolSpec: Prop -> Prop -> bool -> Prop
-Nat.eqb: nat -> nat -> bool
-Nat.testbit: nat -> nat -> bool
 Nat.ltb: nat -> nat -> bool
+Nat.testbit: nat -> nat -> bool
+Nat.eqb: nat -> nat -> bool
 Nat.leb: nat -> nat -> bool
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
 bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
+eq_true_ind_r:
+  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
 eq_true_rec:
   forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b
-bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
-eq_true_rect_r:
-  forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
-eq_true_rec_r:
-  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
 eq_true_rect:
   forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
+eq_true_sind:
+  forall P : bool -> SProp, P true -> forall b : bool, eq_true b -> P b
+bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
 eq_true_ind:
   forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
-eq_true_ind_r:
-  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
+eq_true_rec_r:
+  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+eq_true_rect_r:
+  forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
+bool_sind:
+  forall P : bool -> SProp, P true -> P false -> forall b : bool, P b
 Byte.to_bits:
   Byte.byte ->
   bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
 Byte.of_bits:
   bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
   Byte.byte
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 andb_true_intro:
   forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+BoolSpec_sind:
+  forall (P Q : Prop) (P0 : bool -> SProp),
+  (P -> P0 true) ->
+  (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
 BoolSpec_ind:
   forall (P Q : Prop) (P0 : bool -> Prop),
   (P -> P0 true) ->
diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v
index 1e17d090c2..0e65211390 100644
--- a/test-suite/success/sprop.v
+++ b/test-suite/success/sprop.v
@@ -1,8 +1,12 @@
 (* -*- mode: coq; coq-prog-args: ("-allow-sprop") -*- *)
 
+Set Primitive Projections.
+Set Warnings "+non-primitive-record".
+
 Check SProp.
 
 Definition iUnit : SProp := forall A : SProp, A -> A.
+
 Definition itt : iUnit := fun A a => a.
 
 Definition iSquash (A:Type) : SProp
@@ -17,3 +21,122 @@ Proof. pose (fun A : SProp => A : Type). Abort.
 
 (* define evar as product *)
 Check (fun (f:(_:SProp)) => f _).
+
+Inductive sBox (A:SProp) : Prop
+  := sbox : A -> sBox A.
+
+Definition uBox := sBox iUnit.
+
+(* Primitive record with all fields in SProp has the eta property of SProp so must be SProp. *)
+Fail Record rBox (A:SProp) : Prop := rmkbox { runbox : A }.
+Section Opt.
+  Local Unset Primitive Projections.
+  Record rBox (A:SProp) : Prop := rmkbox { runbox : A }.
+End Opt.
+
+(* Check that defining as an emulated record worked *)
+Check runbox.
+
+(* Check that it doesn't have eta *)
+Fail Check (fun (A : SProp) (x : rBox A) => eq_refl : x = @rmkbox _ (@runbox _ x)).
+
+Inductive sEmpty : SProp := .
+
+Inductive sUnit : SProp := stt.
+
+Inductive BIG : SProp := foo | bar.
+
+Inductive Squash (A:Type) : SProp
+  := squash : A -> Squash A.
+
+Definition BIG_flip : BIG -> BIG.
+Proof.
+  intros [|]. exact bar. exact foo.
+Defined.
+
+Inductive pb : Prop := pt | pf.
+
+Definition pb_big : pb -> BIG.
+Proof.
+  intros [|]. exact foo. exact bar.
+Defined.
+
+Fail Definition big_pb (b:BIG) : pb :=
+  match b return pb with foo => pt | bar => pf end.
+
+Inductive which_pb : pb -> SProp :=
+| is_pt : which_pb pt
+| is_pf : which_pb pf.
+
+Fail Definition pb_which b (w:which_pb b) : bool
+  := match w with
+     | is_pt => true
+     | is_pf => false
+     end.
+
+(* Non primitive because no arguments, but maybe we should allow it for sprops? *)
+Fail Record UnitRecord : SProp := {}.
+
+Section Opt.
+  Local Unset Primitive Projections.
+  Record UnitRecord' : SProp := {}.
+End Opt.
+Fail Scheme Induction for UnitRecord' Sort Set.
+
+Record sProd (A B : SProp) : SProp := sPair { sFst : A; sSnd : B }.
+
+Scheme Induction for sProd Sort Set.
+
+Unset Primitive Projections.
+Record sProd' (A B : SProp) : SProp := sPair' { sFst' : A; sSnd' : B }.
+Set Primitive Projections.
+
+Fail Scheme Induction for sProd' Sort Set.
+
+Inductive Istrue : bool -> SProp := istrue : Istrue true.
+
+Definition Istrue_sym (b:bool) := if b then sUnit else sEmpty.
+Definition Istrue_to_sym b (i:Istrue b) : Istrue_sym b := match i with istrue => stt end.
+
+Record Truepack := truepack { trueval :> bool; trueprop : Istrue trueval }.
+
+Class emptyclass : SProp := emptyinstance : forall A:SProp, A.
+
+(** Sigma in SProp can be done through Squash and relevant sigma. *)
+Definition sSigma (A:SProp) (B:A -> SProp) : SProp
+  := Squash (@sigT (rBox A) (fun x => rBox (B (runbox _ x)))).
+
+Definition spair (A:SProp) (B:A->SProp) (x:A) (y:B x) : sSigma A B
+  := squash _ (existT _ (rmkbox _ x) (rmkbox _ y)).
+
+Definition spr1 (A:SProp) (B:A->SProp) (p:sSigma A B) : A
+  := let 'squash _ (existT _ x y) := p in runbox _ x.
+
+Definition spr2 (A:SProp) (B:A->SProp) (p:sSigma A B) : B (spr1 A B p)
+  := let 'squash _ (existT _ x y) := p return B (spr1 A B p) in runbox _ y.
+(* it's SProp so it computes properly *)
+
+(** Fixpoints on SProp values are only allowed to produce SProp results *)
+Inductive sAcc (x:nat) : SProp := sAcc_in : (forall y, y < x -> sAcc y) -> sAcc x.
+
+Definition sAcc_inv x (s:sAcc x) : forall y, y < x -> sAcc y.
+Proof.
+  destruct s as [H]. exact H.
+Defined.
+
+Section sFix_fail.
+  Variable P : nat -> Type.
+  Variable F : forall x:nat, (forall y:nat, y < x -> P y) -> P x.
+
+  Fail Fixpoint sFix (x:nat) (a:sAcc x) {struct a} : P x :=
+    F x (fun (y:nat) (h: y < x) => sFix y (sAcc_inv x a y h)).
+End sFix_fail.
+
+Section sFix.
+  Variable P : nat -> SProp.
+  Variable F : forall x:nat, (forall y:nat, y < x -> P y) -> P x.
+
+  Fixpoint sFix (x:nat) (a:sAcc x) {struct a} : P x :=
+    F x (fun (y:nat) (h: y < x) => sFix y (sAcc_inv x a y h)).
+
+End sFix.
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 8b8307c14a..977e804da2 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -140,9 +140,6 @@ let make_conclusion_flexible sigma = function
         | None -> sigma)
      | _ -> sigma)
 
-let is_impredicative env u =
-  Sorts.is_prop u || (is_impredicative_set env && Sorts.is_set u)
-
 let interp_ind_arity env sigma ind =
   let c = intern_gen IsType env sigma ind.ind_arity in
   let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
@@ -177,7 +174,7 @@ let sign_level env evd sign =
         in
         let u = univ_of_sort s in
           (Univ.sup u lev, push_rel d env))
-    sign (Univ.type0m_univ,env))
+    sign (Univ.Universe.sprop,env))
 
 let sup_list min = List.fold_left Univ.sup min
 
@@ -261,7 +258,7 @@ let solve_constraints_system levels level_bounds =
 let inductive_levels env evd poly arities inds =
   let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
   let levels = List.map (fun (x,(ctx,a)) ->
-    if Sorts.is_prop a then None
+    if Sorts.is_prop a || Sorts.is_sprop a then None
     else Some (univ_of_sort a)) destarities
   in
   let cstrs_levels, min_levels, sizes =
@@ -270,7 +267,7 @@ let inductive_levels env evd poly arities inds =
         let len = List.length tys in
         let minlev = Sorts.univ_of_sort du in
         let minlev =
-          if len > 1 && not (is_impredicative env du) then
+          if len > 1 && not (is_impredicative_sort env du) then
             Univ.sup minlev Univ.type0_univ
           else minlev
         in
@@ -291,7 +288,7 @@ let inductive_levels env evd poly arities inds =
   in
   let evd, arities =
     CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len ->
-      if is_impredicative env du then
+      if is_impredicative_sort env du then
         (* Any product is allowed here. *)
         evd, arity :: arities
       else (* If in a predicative sort, or asked to infer the type,
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 0e0788c470..047bdd2b61 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -489,6 +489,8 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
      str "The return clause of the following pattern matching should be" ++
      strbrk " a coinductive type:" ++
      spc () ++ pr_lconstr_env env sigma c
+  | FixpointOnIrrelevantInductive ->
+    strbrk "Fixpoints on proof irrelevant inductive types should produce proof irrelevant values"
   in
   prt_name i ++ str " is ill-formed." ++ fnl () ++
   pr_ne_context_of (str "In environment") env sigma ++
@@ -1205,7 +1207,7 @@ let error_large_non_prop_inductive_not_in_type () =
   str "Large non-propositional inductive types must be in Type."
 
 let error_inductive_bad_univs () =
-  str "Incorrect universe constrains declared for inductive type."
+  str "Incorrect universe constraints declared for inductive type."
 
 (* Recursion schemes errors *)
 
diff --git a/vernac/record.ml b/vernac/record.ml
index 6b223f845b..46b4074eaa 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -92,7 +92,7 @@ let compute_constructor_level evars env l =
 	  Univ.sup (univ_of_sort s) univ 
       else univ
     in (EConstr.push_rel d env, univ))
-    l (env, Univ.type0m_univ)
+    l (env, Univ.Universe.sprop)
 
 let binder_of_decl = function
   | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
@@ -167,8 +167,8 @@ let typecheck_params_and_fields finite def poly pl ps records =
     Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma in
   let fold sigma (typ, sort) (_, newfs) =
     let _, univ = compute_constructor_level sigma env_ar newfs in
-      if not def && (Sorts.is_prop sort ||
-	(Sorts.is_set sort && is_impredicative_set env0)) then
+    let univ = if Sorts.is_sprop sort then univ else Univ.Universe.sup univ Univ.type0m_univ in
+      if not def && is_impredicative_sort env0 sort then
         sigma, typ
       else
         let sigma = Evd.set_leq_sort env_ar sigma (Sorts.sort_of_univ univ) sort in