How to program in a way where I can avoid universe errors

Stream: new members

[Kitsune-Violet]

Hello! I have just started using lean for programming because it seems like the best and most powerful language for programming with monad transformers, the biggest issue I am running into is that the type system is complex and the compile errors can be all manner of scary!

I only want to use dependent typing for a single step so that I can do my AST lowering in a well typed way. The rest I would prefer to avoid that aspect of the type system entirely. :sweat_smile:

How do I do this? For the record here is the (probably embarrassing) code and error that caused this:

structure Parser (m: Type -> Type) (a: Type) where
    (run: Array Token -> m (ParseResult $ Prod (Array Token) a))

which gave this error

stuck at solving universe constraint
  1 =?= max (max 1 ?u.847) ?u.848
while trying to unify
  Type : Type 1
with
  Sort (max (max 1 ?u.848) ?u.847) : Type (max (max 1 ?u.848) ?u.847)

Highlighting run.

(I hope I am doing this Zulip thing right)

[Eric Wieser]

Can you make this a #mwe ?

[Kitsune-Violet]

abbrev ParseErr: Type := sorry

abbrev Token: Type := sorry

inductive ParseResult (a: Type) where
    | ShallowErr: sorry -> ParseResult a
    | DeepErr: sorry -> ParseResult a
    | Success: a -> ParseResult a

structure Parser (m: Type -> Type) (a: Type) where
    (run: Array Token -> m (ParseResult $ Prod (Array Token) a))

[Aaron Liu]

did you want everything to be in Type?

[Aaron Liu]

if so, then you should fix those type-valued sorrys which are not in Type

abbrev ParseErr: Type := sorry

abbrev Token: Type := sorry

inductive ParseResult (a: Type) where
    | ShallowErr: (sorry : Type) -> ParseResult a
    | DeepErr: (sorry : Type) -> ParseResult a
    | Success: a -> ParseResult a

structure Parser (m: Type -> Type) (a: Type) where
  -- doesn't error
    (run: Array Token -> m (ParseResult $ Prod (Array Token) a))

[Kitsune-Violet]

Aaron Liu said:

if so, then you should fix those type-valued sorrys which are not in Type

abbrev ParseErr: Type := sorry

abbrev Token: Type := sorry

inductive ParseResult (a: Type) where
    | ShallowErr: (sorry : Type) -> ParseResult a
    | DeepErr: (sorry : Type) -> ParseResult a
    | Success: a -> ParseResult a

structure Parser (m: Type -> Type) (a: Type) where
  -- doesn't error
    (run: Array Token -> m (ParseResult $ Prod (Array Token) a))

So sorry for how simple that solution was! Thank you so much for the help, how do I avoid this type of thing whilst I am intending to be in my single universe level "safe space" :p.

Or is sorry just a weird example?

[Henrik Böving]

sorry is a universe polymorphic construction that can live in some arbitrary universe Sort u so your construction was automatically polymorphised to live in

ParseResult.{u_1, u_2} (a : Type) : Sort (max (max 1 u_1) u_2)

if you had provided Lean with some concrete Type things there (or as shown in the fix made clear that sorry is supposed to stand in for precisely a Type as opposed to a Sort u) the type will remain in Type.

[Kyle Miller]

One way to think about it for now is if you see any question marks in an error about universes, you can take it to mean that something's type isn't fully determined yet.