do block: invalid reassignment

Stream: lean4

[Marcus Rossel]

The following example produces an error on the for loop:

example : Unit := Id.run do
  let mut nat : ULift.{1} Nat := ULift.up 0
  for _ in [""] do -- error
    nat := ULift.up.{1} 123

/-
invalid reassignment, value has type
  ?m.8285 : Type
but is expected to have type
  ULift Nat : Type 1
-/

Also, hovering over nat shows nat : ?m.8285.
Is it not possible to use any types in higher universes than Type 0 in do blocks?

[James Gallicchio]

You can, but some of the relevant typeclasses aren't universe polymorphic. I thought list forin was universe polymorphic, but...

[James Gallicchio]

Actually I have no idea why this doesn't compile, List forin is universe polymorphic

[James Gallicchio]

Oh, wait. StateT requires the state & the return type to be in the same universe? This compiles:

example : PUnit.{2} := Id.run do
  let mut nat : ULift.{1} Nat := ULift.up 0
  for _ in [""] do
    nat := ULift.up.{1} 123

[Marcus Rossel]

James Gallicchio said:

Oh, wait. StateT requires the state & the return type to be in the same universe? This compiles:

example : PUnit.{2} := Id.run do
  let mut nat : ULift.{1} Nat := ULift.up 0
  for _ in [""] do
    nat := ULift.up.{1} 123

Hm, so if I'm working in IO I'm doomed right? Because IO PUnit.{2} isn't possible.

[James Gallicchio]

Yeah, IO is limited to Type 0

[Marcus Rossel]

I wonder though whether the same-universe requirement on StateT is intentional?

[James Gallicchio]

I think it is; just changed it in the prelude to see what breaks, and, well, many things break

[James Gallicchio]

Don't really have the time to figure out whether those are fixable breaks, but... :p There's been other discussions about this restriction on here, if you search IO and universe they should come up

[Marcus Rossel]

Yeah, I've seen the universe polymorphic IO discussion, but was hoping I could avoid that since I'm just returning Unit. But I guess I have to return PUnit.{2} :see_no_evil: