Universe inference

Stream: lean4

[Siddharth Bhat]

consider:

inductive NoWorkBlockLens: Type -> Type where
| BlockOp: o -> NoWorkBlockLens o
| BlockUnit:  NoWorkBlockLens Unit

which does not type check with :

(kernel) universe level of type_of(arg #1) of 'NoWorkBlockLens.BlockOp' is too big for the corresponding inductive datatype

The fix is to manually declare all universes:

-- | Needs to be sure that o and Unit are on the same level.
inductive BlockLens: Type u -> Type (u + 1)  where
| BlockOp: (o: Type u) -> BlockLens o
| BlockUnit:  BlockLens (ULift Unit)

Coq infers universes:

Set Printing Universes.
Inductive BlockLens : Type -> Type :=
| BlockOp: forall (o: Type), o -> BlockLens o
| BlockUnit: BlockLens nat
.
Print BlockLens.

with:

Inductive BlockLens : Type@{BlockLens.u0} -> Type@{max(Set,BlockLens.u1+1)} :=
    BlockOp : forall o : Type@{BlockLens.u1}, o -> BlockLens o | BlockUnit : BlockLens nat.

Is this intended behaviour?

[Sebastian Ullrich]

Lean can infer universes as well: Type _

[James Gallicchio]

Coq has no problem with this definition living in Type instead of Type (u+1), do you know why that difference exists?

It came up as an issue here that requires a pretty annoying workaround

[James Gallicchio]

Oh wait, re-reading that, it is not living in the same universe as o, nevermind

[Sebastian Ullrich]

@Siddharth Bhat You don't need to define them either, and there's PUnit

inductive NoWorkBlockLens : Type _ → Type _ where
  | BlockOp : o → NoWorkBlockLens o
  | BlockUnit : NoWorkBlockLens PUnit

[Siddharth Bhat]

Thanks for that, I'd forgotten about the existence of PUnit. In the real use-case I have, it's not Unit, but some kind of user defined datatype, so I unfortunately still need the ULift, I think. I'll experiment a little!