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 α
purepure ret: IO String
 ret: String
ret
  else
    pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
purepure "none": IO String
 "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 ?_ : Type but is expected to have type IO (Option String) : Type

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

error: type mismatch
  some ret
has type
  Option ?_ : Type
but is expected to have type
  IO (Option String) : Type 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 ?_ : Type
but is expected to have type
  IO (Option String) : Type := 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 : Type but is expected to have type IO String : Type

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

error: type mismatch
  io
has type
  String : Type
but is expected to have type
  IO String : Type 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 : Type
but is expected to have type
  IO String : Type -- 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 ?_ : Type but is expected to have type IO (Option String) : Type

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

error: type mismatch
  some opt
has type
  Option ?_ : Type
but is expected to have type
  IO (Option String) : Type 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 ?_ : Type
but is expected to have type
  IO (Option String) : Type := 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

error: application type mismatch pure true argument true has type Bool : Type but is expected to have type Unit : Type

error: application type mismatch pure false argument false has type Bool : Type but is expected to have type Unit : Type

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

error: application type mismatch
  pure true
argument
  true
has type
  Bool : Type
but is expected to have type
  Unit : Type
---
error: application type mismatch
  pure false
argument
  false
has type
  Bool : Type
but is expected to have type
  Unit : Type in
example: IO Unit
example : IO: Type → Type
IO Unit: Type
Unit := do
  let x ← if true: Bool
true then pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure true: Bool
trueError: application type mismatch
  pure true
argument
  true
has type
  Bool : Type
but is expected to have type
  Unit : Type else pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure false: Bool
falseError: application type mismatch
  pure false
argument
  false
has type
  Bool : Type
but is expected to have type
  Unit : Type

error: unknown identifier 'x'

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

error: unknown identifier 'x'
---
error: unknown identifier 'x'
---
error: unknown identifier 'x' 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: ?_
xError: unknown identifier 'x'
Error: unknown identifier 'x'
Error: unknown identifier '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

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

error: application type mismatch pure true argument true has type Bool : Type but is expected to have type Unit : Type

error: unknown identifier 'x'

error: unknown identifier 'x'

Case `if let return` works

Case `let var <- if let` also works

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

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