import Lean
open Lean System

set_option pp.mvars false

From https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unknown.20identifier.20in.20.60let.20var.20.3A.3D.20if.20let.60

def getOpt: String → Option String
getOpt (str: String
str : String: Type
String) : Option: Type → Type
Option String: Type
String := str: String
str

def getIO: String → IO String
getIO (str: String
str : String: Type
String) : IO: Type → Type
IO String: Type
String := pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure str: String
str

def getOptIO: String → IO (Option String)
getOptIO (str: String
str : String: Type
String) : IO: Type → Type
IO (Option: Type → Type
Option String: Type
String) := pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure (some: {α : Type} → α → Option α
some str: String
str)

Initial problem

Case `if let return` works

def works₁: IO String
works₁ : IO: Type → Type
IO String: Type
String := do
  if let some: {α : Type _} → α → Option α
some opt: String
opt := getOpt: String → Option String
getOpt "str": String
"str" then
    let ret: String
ret := (<- getIO opt): String
(<- getIO: String → IO String
getIO(<- getIO opt): String
 opt: String
opt(<- getIO opt): String
)
    return ret: String
ret
  else
    return "none": String
"none"

#eval"str" works₁: IO String
works₁ -- works "str"

Case `let var <- if let` also works

def works₂: IO String
works₂ : IO: Type → Type
IO String: Type
String := do
  let var: String
var <- if let some: {α : Type _} → α → Option α
some opt: String
opt := getOpt: String → Option String
getOpt "str": String
"str" then
    let ret: String
ret := (<- getIO opt): String
(<- getIO: String → IO String
getIO(<- getIO opt): String
 opt: String
opt(<- getIO opt): String
)
    pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure ret: String
ret
  else
    pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure "none": String
"none"

  return var: String
var

#eval"str" works₂: IO String
works₂ -- works: "str"

Case `let var := if let` gives `unknown identifier`

error: Unknown identifier opt

#guard_msgsError: ❌️ Docstring on `#guard_msgs` does not match generated message:

-
+ error: Unknown identifier `opt`
 in
def oops₀: IO String
oops₀ : IO: Type → Type
IO String: Type
String := do
  let var: String
var := if let some: {α : Type _} → α → Option α
some opt: String
opt := getOpt: String → Option String
getOpt "str": String
"str" then
    let ret: String
ret := (<- getIO : String
(<- getIO: String → IO String
getIO(<- getIO : String
 opt: String
optError: Unknown identifier `opt`): String
)  -- unknown identifier 'opt'
    ret: String
ret
  else
    "none": String
"none"

  return var: String
var

More variants

Variant 1. expect `<-`, misuse `:=`

1.1 expect `<-`, misuse `:=`, gives `unknown identifier`

error: Unknown identifier ret

#guard_msgsError: ❌️ Docstring on `#guard_msgs` does not match generated message:

-
+ error: Unknown identifier `ret`
 in
def oops₁₁: IO String
oops₁₁ : IO: Type → Type
IO String: Type
String := do
  let some: ?_ → IO (Option String)
some ret: ?_
ret := getOptIO: String → IO (Option String)
getOptIO "str": String
"str"
  ret: IO String
retError: Unknown identifier `ret` -- unknown identifier 'ret'

1.2 expect `<-`, misuse `:=`, gives `type mismatch`

error: Type mismatch some ret has type Option ?_ but is expected to have type IO (Option String)

#guard_msgsError: ❌️ Docstring on `#guard_msgs` does not match generated message:

-
+ error: Type mismatch
+   some ret
+ has type
+   Option ?_
+ but is expected to have type
+   IO (Option String)
 in
def oops₁₂: IO String
oops₁₂ : IO: Type → Type
IO String: Type
String := do
  let some: {α : Type _} → α → Option α
some retError: Type mismatch
  some ret
has type
  Option ?_
but is expected to have type
  IO (Option String) := getOptIO: String → IO (Option String)
getOptIO "str": String
"str" | pure "none" -- type mismatch: `IO (Option String)` got `Option ?m.2842`
  pure ret

1.3 using `<-` works

def works₁₃: IO String
works₁₃ : IO: Type → Type
IO String: Type
String := do
  let some: {α : Type _} → α → Option α
some ret: String
ret <- getOptIO: String → IO (Option String)
getOptIO "str": String
"str" | pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure "none": String
"none"
  pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure ret: String
ret -- works

Variant 2. expect `:=`, misuse `<-`, gives `type mismatch`

error: Type mismatch io has type String but is expected to have type IO String

#guard_msgsError: ❌️ Docstring on `#guard_msgs` does not match generated message:

-
+ error: Type mismatch
+   io
+ has type
+   String
+ but is expected to have type
+   IO String
 in
def oops₂: IO String
oops₂ : IO: Type → Type
IO String: Type
String := do
  let io: String
io <- getIO: String → IO String
getIO "str": String
"str"
  io: String
ioError: Type mismatch
  io
has type
  String
but is expected to have type
  IO String -- type mismatch: expected `IO String`, got `String`

Variant 3. in `if let`, expect `:=`, misuse `<-`

-- def oops₃ : IO String := do
--   if let some opt <- getOpt "str" then  -- unexpected token '<-'; expected ':=' or '←'
--     let ret := (<- getIO opt)
--     return ret
--   else
--     return "none"

Variant 4. in `if let`, expect `:= (<- ... )`

4.1 misuse `:=` gives me type mismatch

error: Type mismatch some opt has type Option ?_ but is expected to have type IO (Option String)

#guard_msgsError: ❌️ Docstring on `#guard_msgs` does not match generated message:

-
+ error: Type mismatch
+   some opt
+ has type
+   Option ?_
+ but is expected to have type
+   IO (Option String)
 in
def oops₄₁: IO String
oops₄₁ : IO: Type → Type
IO String: Type
String := do
  if let some: {α : Type _} → α → Option α
some optError: Type mismatch
  some opt
has type
  Option ?_
but is expected to have type
  IO (Option String) := getOptIO: String → IO (Option String)
getOptIO "str": String
"str" then -- type mismatch: expected `IO (Option String)`, got `Option ?m.3586`
    let ret <- getIO opt
    pure ret
  else
    pure "none"

4.2 misuse `<-` gives me `unexpected token '<-'; expected ':=' or '←'`

-- def oops₄₂ : IO String := do
--   if let some opt <- getOptIO "str" then -- unexpected token '<-'; expected ':=' or '←'
--     let ret <- getIO opt
--     pure ret
--   else
--     pure "none"

4.3 using `:= (<- ... )` works

def works₄₃: IO String
works₄₃ : IO: Type → Type
IO String: Type
String := do
  if let some: {α : Type _} → α → Option α
some opt: String
opt := (<- getOptIO "str"): Option String
(<- getOptIO: String → IO (Option String)
getOptIO(<- getOptIO "str"): Option String
 "str": String
"str"(<- getOptIO "str"): Option String
) then
    let ret: String
ret <- getIO: String → IO String
getIO opt: String
opt
    pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure ret: String
ret
  else
    pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure "none": String
"none"

Cases from https://github.com/leanprover/lean4/pull/2676

v4.32: both cases below used to fail to elaborate (an application type mismatch on the if branches, and unknown identifier 'x' on the mut binding). The underlying do-block elaborator bugs were fixed, so the examples now compile; the guards document the current (fixed) behavior instead of the historical errors.

warning: Variable name x is not explicitly referenced.

The binding can be removed (if unused) or named _ (if used implicitly).

Note: This linter can be disabled with set_option linter.unusedVariables false

-- v4.32: the `if true then pure true else pure false` branches now unify, so this example
-- only triggers the unused-variable linter (previously it was an application type mismatch).
#guard_msgsError: ❌️ Docstring on `#guard_msgs` does not match generated message:

+ warning: Variable name `x` is not explicitly referenced.
 
+ The binding can be removed (if unused) or named `_` (if used implicitly).
+
+ Note: This linter can be disabled with `set_option linter.unusedVariables false`
 in
example: IO Unit
example : IO: Type → Type
IO Unit: Type
Unit := do
  let x: Bool
xWarning: Variable name `x` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false` ← if true: Bool
true then pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure true: Bool
true else pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure false: Bool
false

-- v4.32: the `Id` do-block now elaborates cleanly, so there are no messages to guard.
/- -/
#guard_msgs in
example: Id Unit
example : Id: Type → Type
Id Unit: Type
Unit := do
  let mut x: Bool
x ← if true: Bool
true then pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure true: Bool
true else pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure false: Bool
false
  if let .true: Bool
.true := x: Bool
x then
    x: Bool
x := false: Bool
false

Initial problem

Case if let return works

Case let var <- if let also works

Case let var := if let gives unknown identifier

More variants

Variant 1. expect <-, misuse :=

1.1 expect <-, misuse :=, gives unknown identifier

1.2 expect <-, misuse :=, gives type mismatch

1.3 using <- works

Variant 2. expect :=, misuse <-, gives type mismatch

Variant 3. in if let, expect :=, misuse <-

Variant 4. in if let, expect := (<- ... )

4.1 misuse := gives me type mismatch

4.2 misuse <- gives me unexpected token '<-'; expected ':=' or '←'

4.3 using := (<- ... ) works