Why are these mutually recursive?

Stream: lean4

[Max Nowak 🐉]

I have the following mwe:

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

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

And the Lean kernel complains that "(kernel) mutually inductive types must live in the same universe", but I do not see what is mutually recursive about these two types.

[Jannis Limperg]

TInv is nested and is therefore presumably translated to a mutual inductive type before it reaches the kernel.

[Max Nowak 🐉]

I thought you can construct Declarations (from Expr yourself) which contain nested TInv and addDecl those directly to the kernel, skipping the elaborator?

[Max Nowak 🐉]

So then the "mutual inductive type must live in the same universes" does not refer to T and TInv, but rather to TInv and whatever other mutual declaration is generated by the elaborator?

[Sebastian Ullrich]

Yes, the specialization of Subtype. But this transformation is done in the kernel, not in the elaborator.

[Sebastian Ullrich]

See also https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Mutual.20inductive.20universe

[Max Nowak 🐉]

Specialization? I have encountered that term a few times before but thus far joyfully ignored it.

If the transformation is done in the kernel, I suppose there is no way around it, even if I define my own copy of Subtype.

[Max Nowak 🐉]

I was hoping to simplify my code generating binders (a : T) -> (prf : TInv a) -> ... (which works) into just a subtype.

[Jannis Limperg]

When Lean sees a nested inductive type

inductive T
  | c : A T -> T

it translates this into the mutual inductive types

inductive AT
  <constructors mentioning T>

inductive T
  | c : AT -> T

where AT is isomorphic to A T (and hence a specialisation of A). Here, A is Subtype. You can perform this translation yourself to get a sense of what might be going wrong.

With that said, if you can easily avoid nested/mutual inductive types, I would highly recommend you do that. Lean's support for them is still pretty rough.

[Max Nowak 🐉]

Sigh, yeah, I suppose I will just avoid Subtype and keep my old approach, which will get fiddly in other places.