type theory edge case: projections and sort polymorphism

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Using set_option bootstrap.inductiveCheckResultingUniverse false allows the creation of inductive types in Sort u that support primitive projections to types in Sort u, yet with a recursor that only allows eliminating into Prop. This means that primitive projections are currently not conservative over recursors.

Context

https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/type.20theory.20edge.20case.3A.20projections.20and.20sort.20polymorphism

Steps to Reproduce

set_option bootstrap.inductiveCheckResultingUniverse false in
set_option genSizeOf false in
set_option genInjectivity false in
inductive Wrap (α : Sort u) : Sort u
  | wrap (unwrap : α)

abbrev Wrap.unwrap {α : Sort u} (self : Wrap α) : α := self.1

/--
info: Wrap.rec.{u} {α : Sort u} {motive : Wrap α → Prop} (wrap : ∀ (unwrap : α), motive (Wrap.wrap unwrap)) (t : Wrap α) :
  motive t
-/
#guard_msgs in
#check Wrap.rec

The recursor for Wrap can only eliminate into Prop since the argument unwrap : α to the constructor is not a Prop. However, primitive projection is allowed since Wrap α : Prop only when α : Prop, and projecting a Prop field is valid. This means that the projection Wrap.unwrap cannot be expressed using the recursor Wrap.rec.

Versions

Lean 4.19.0-nightly-2025-03-22

Additional Information

There seem to be two ways to fix this discrepency between the strength of recursors and projections.
One is to disallow projections for such types, weakening projections to match the existing recursors, and the other is to allow subsingleton elimination for such types, strengthening recursors to match the existing projections.
I have implemented the latter at https://github.com/leanprover/lean4/commit/0194f054243f271ed3ec45303b41c96ef03ff307, where the subsingleton elimination check in elim_only_at_universe_zero is modified to check that the fields live in Prop for level assignments that result in the inductive type being in Prop. In the example above, this causes Wrap.rec to support non-Prop motives. This change would also allow structures like PProd and PSigma to avoid having max 1 in their sort level, which could potentially simplify metaprogramming code:

set_option bootstrap.inductiveCheckResultingUniverse false in
structure PProd' (α : Sort u) (β : Sort v) : Sort (max u v) where
  fst : α
  snd : β

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the minimal Wrap reproduction in the issue and verify its behavior on the current nightly release. Read the linked Zulip discussion and compare the allowed primitive projection with the generated recursor. Done means resolving the discrepancy consistently and adding a regression test for the chosen behavior.