Lean Kernel Arena / corner-cases/proj-maybe-prop

Projecting out of a structure that may or may not be a proposition.

MaybeProp is a structure whose sort is a bare level parameter: a proposition for u := 0 and a data type for every other u. Lean's inductive command refuses to declare one ("the resulting universe is not Prop, but it may be Prop for some parameter values"), but the kernel accepts it. The exported definition projects out its first field, field : PUnit.{u}.

The official kernel accepts this. The field is not a proof for every u, but the projection is sound at every instantiation: MaybeProp.{u} is a proposition only for u := 0, and there the field's type PUnit.{0} is a proposition too. That is no coincidence. A structure that is not a Prop had every constructor field's universe checked against its resulting universe (see the tutorial's typeWithTooHighTypeField), here u ≤ u, and such an inequality survives instantiation — so wherever the structure does turn out to be a proposition, so do all of its fields.

At the same time, the official kernel here allows more projections than the recursor allows: MaybeProp.rec eliminates into Prop only, so this projection cannot be expressed through the recursor. The elaborator does not currently rely on this extra power, so for now it is reasonable for a checker to be more restrictive here and reject the projection — for example by asking "could this be a proposition?" and then demanding that the field be definitely a proof. See https://github.com/leanprover/lean4/issues/7637 for discussion.