monadic bind ignoring type annotation

Stream: lean4

[Jakob von Raumer]

Is it intended if I write something like

def foo : Nat := Id.run <| do
  let x : Int × Int ← do
    pure ((5 : Nat), (6 : Nat))
  pure x.1

the annotation for x just gets ignored? (In that no cast is applied) I would have expected the above snippet to fail like

def bar : Nat := Id.run <| do
  let x : Int × Int :=
    ((5 : Nat), (6 : Nat))
  pure x.1

does

[Jakob von Raumer]

(I mean, there's no coercion from Nat × Nat to Int × Int, so I'd expect the error to be at the second line, not at the fourth line)

[Jakob von Raumer]

Maybe slightly unrelated but also on the topic of type ascriptions on monadic lets: Why is it a syntax error if I attempt a let pattern on a monadic let:

def foo : Id Unit := do
  let (x, y) : Nat × Nat ← do
    pure (3, 4)
  pure ()

[Jakob von Raumer]

This works if I expand it to

def foo : Id Unit := do
  let (x, y) : Nat × Nat := ← do
    pure (3, 4)
  pure ()

[Eric Wieser]

lean4#3126:

set_option autoImplicit false

example : IO Unit := do
  let x : IAmIgnored ← do pure 1
  return

[Jakob von Raumer]

Do you think the matching issue counts as a separate bug?

[Eric Wieser]

Yes, probably worth filing a separate bug

[Eric Wieser]

This works fine too:

  let ((x, y) : Nat × Nat) ← do
    pure (3, 4)

[Jakob von Raumer]

(deleted)

[Jakob von Raumer]

But somehow this only works without the brackets:

instance : CoeT (BitVec n) x (BitVec m) where
  coe := x.setWidth m

def foo (x : Nat) : Id Unit := do
  let ((z, b) : ((BitVec x) × Bool)) :=
    match x with
    | 16 => (0#16, false)
    | n => (0#n, false)
  pure ()

I guess because putting brackets in a let binder performs a casting after elaborating the body?

[Jakob von Raumer]

(This probably isn't a bug, just shows that having brackets there changes the elaboration, sometimes in unfavourable ways)