Mutual inductive universe

Stream: lean4

[Henrik Böving]

mutual

inductive A : Type where
| a (arg : B)

inductive B : Type where
| b (arg : ST.Ref Unit A)

end

This gives me:

(kernel) mutually inductive types must live in the same universe

but..these types to live in the same universe right? After all the elaborator did not complain about the : Type annotation and if I was to split up the mutual by setting A = Nat in B and B = Nat in A respectively they do end up living in the proper universes.

Is this a bug?

[Kevin Buzzard]

This works though:

structure stref (α β : Type) : Type

mutual

inductive A : Type where
| a (arg : B)

inductive B : Type where
| b (arg : stref Unit A)

end

[Henrik Böving]

Ah I think I'm onto something:

fails

opaque RefPointed : NonemptyType.{0}

structure Ref (σ : Type) (α : Type) : Type where
  ref : RefPointed.type
  h   : Nonempty α

mutual


inductive A : Type where
| a (arg : B)

inductive B : Type where
| b (arg : Ref Unit A)

end

works

opaque RefPointed : NonemptyType.{0}

structure Ref (σ : Type) (α : Type) : Type where
  ref : RefPointed.type
  -- POOF! h   : Nonempty α

mutual


inductive A : Type where
| a (arg : B)

inductive B : Type where
| b (arg : Ref Unit A)

end

[Henrik Böving]

Alternatively further minimized of course:

structure Ref1 (σ : Type) (α : Type) : Type where
  --h   : Nonempty α

structure Ref2 (σ : Type) (α : Type) : Type where
  h   : Nonempty α

mutual


inductive A : Type where
| a (arg : B)

inductive B : Type where
| b (arg : Ref2 Unit A)

end

[Reid Barton]

This doesn't seem too surprising, after all if you put a random thing instead of Ref2 then it would be unsound, so there will also be cases where it would be fine but Lean still rejects it

[Henrik Böving]

Can you elaborate? I don't understand what is wrong

[Reid Barton]

For example if Ref2 Unit A unfolds to A -> False, that would be Bad

[Henrik Böving]

Right but that would be a non positive occurence and not a universe error would it?

[Reid Barton]

Even here it is not very obvious to me what induction principle Lean is supposed to generate for these types

[Reid Barton]

oh well, I don't really trust Lean to produce the correct error message

[Reid Barton]

Maybe it is connected to the Prop-truncation of Nonempty though?

[Reid Barton]

Already this fails

mutual

inductive A : Type where
| a (arg : B)

inductive B : Type where
| b (arg : Nonempty A)

end

[Reid Barton]

or even

inductive A : Type where
| a (arg : Nonempty A)

[Reid Barton]

I am not saying that it should be allowed or shouldn't be allowed, just that I am not surprised that it is currently not allowed.

[Sebastian Ullrich]

Yes, Nonempty is inlined, which makes this a mixed-Type/Prop mutual inductive

[Henrik Böving]

:( So I cannot have mutual inductives with mutable references for now?

[Reid Barton]

If you could have one then you could build a cyclic reference right? I was under the impression that was intended to be impossible

[Mario Carneiro]

you can do it with an unsafe inductive