Failure of for loop in `Id` monad, in presence of universe

Stream: lean4

[Adam Topaz]

Here is a MWE:

import Lean

open Std

universe u

-- Works
example {α : Type u} [Hashable α] [BEq α] (A : Array α) : HashMap α Nat := Id.run do
  let mut t : HashMap α Nat := {}
  for (x,i) in A.zipWithIndex do
    t := t.insert x i
  return t

-- Works
example {α : Type} [Hashable α] [BEq α] (A : Array α) : Nat := Id.run do
  let mut t : HashMap α Nat := {}
  for (x,i) in A.zipWithIndex do
    t := t.insert x i
  return 0

-- Fails
example {α : Type u} [Hashable α] [BEq α] (A : Array α) : Nat := Id.run do
  let mut t : HashMap α Nat := {}
  for (x,i) in A.zipWithIndex do
    t := t.insert x i
  return 0

Can someone explain why the last example fails while the first two are okay?

[Eric Wieser]

I think this is the standard "do notation / Monad is universe-monomorphic" issue, combined with the notation that for is transformed into

[Eric Wieser]

You can fix it by making the return type  ULift.{u} Nat

[Adam Topaz]

Yeah, I guess this is what's going on, but I find it strange that the above fails while something like the following works perfectly fine:

import Lean

open Std

universe u

example {α : Type u} [Hashable α] [BEq α] (A : Array α) : Nat := Id.run do
  let _t : HashMap α Nat := Id.run do
    let mut t : HashMap α Nat := {}
    for (x,i) in A.zipWithIndex do
      t := t.insert x i
    return t
  return 0

[Adam Topaz]

Of course if I change let _t ... := ... to let _t ... <- ... then a similar error appears.

[Eric Wieser]

I think the fact that this in Id makes it easier to make examples which accidentally work

[Eric Wieser]

Here your _t is using a unrelated do block that is not binded with the external one (which would force a single universe for the results)

[Adam Topaz]

yeah, I understand (and this is also why binding with <- fails)

[Eric Wieser]

I'm contesting your claim that this is strange :)

[Adam Topaz]

Fair enough.

[Adam Topaz]

I guess it's not "strange" if we understand it :)