Type annotation for `let` in a monad

Stream: metaprogramming / tactics

[Mirek Olšák]

I originally thought that something like this could work

def something : Unit := Id.run do
  let a : String ←
    match () with
      | () => pure "hello"

but no, it throws a weird type error.

After experimenting a bit, I found that parentheses solve the issue

def something2 : Unit := Id.run do
  let (a : String) ←
    match () with
      | () => pure "hello"

however, I am still really confused what is going on. For example, this is a valid syntax.

def something3 : Unit := Id.run do
  let a : b ←
    match () with
      | () => pure ()

(tested on current live lean)

[Robin Arnez]

lean4#3126

[Robin Arnez]

This will probably be fixed by the new do elaborator (lean4#12459)