RFC: Mutual inductives with heterogeneous universes

Proposal

Add support for mutual inductives where all not inductive types live in the same universe. This can occur safely with multiple different data-carrying types, as in:

mutual
  inductive A : Prop where
    | fromB : B → A
    | fromC : C → A
  inductive B : Type 0 where
    | fromA : Nat → A → B
    | wrap : B → B
  inductive C : Type 2 where
    | fromA : A → C
    | higherUniv : Nat → Type → C
    | pair : B → C → C
end

The most immediate use case would be that nested inductives with a nested Prop get compiled to a mutual block, which blocks some development, e.g. these examples from Zulip 1, 2:

-- (kernel) mutually inductive types must live in the same universe
inductive AutoDiffNode (α : Type) (β : Type) : Type
| mk
    (outShape : List Nat)
    (parents : Array (ST.Ref IO.RealWorld (AutoDiffNode α β)))
    : AutoDiffNode α β

inductive T : Type where
| c : T -> T

inductive TInv : T -> Prop where
| c : (a : {t : T // TInv t}) -> TInv (T.c a.val)

As a minimal example,

inductive MyType : Nat → Type
| base : String → MyType 0
| next (n) : Nonempty (MyType n) → MyType (n + 1)

This effectively gets lowered to

mutual
  inductive NE : Nat → Prop where
    | intro : (n : Nat) → MyType3 n → NE n

  inductive MyType3 : Nat → Type where
    | base : String → MyType3 0
    | next : (n : Nat) → NE n → MyType3 (n + 1)
end

and rejected, even though it's type theoretically safe. I have a working demo to show that it's type theoretically safe, by an extension to the elaborator to lower this to homogeneous universes, at PR #14945.

Community Feedback

This was posed in #general > Mutual inductives in different universes.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reading the proposal examples and the referenced community discussion, then review PR #14945 for the existing elaborator approach. Done means mutual inductives with heterogeneous universes are accepted safely, including the minimal MyType example and the nested-Prop use cases described here.