unknown identifier in `let var := if let`

Stream: lean4

[Utensil Song]

I managed to make a #mwe for something I encountered :

import Lean
open Lean System

def getOption (str : String) : Option FilePath := str

def getIOString (file : FilePath) : IO String := do
  return file.toString

def works : IO String := do
  if let some opt := getOption "str" then
    let ret := (<- getIOString opt)
    return ret
  else
    return "no option"

def also_works : IO String := do
  let var <- if let some opt := getOption "str" then
    let ret := (<- getIOString opt)
    pure ret
  else
    pure "no option"

  return var

def oops : IO String := do
  let var := if let some opt := getOption "str" then
    let ret := (<- getIOString opt) -- unknown identifier 'opt'
    ret
  else
    "no option"

  return var

#eval works -- "str"

#eval also_works -- "str"

#eval oops -- cannot evaluate code because 'oops' uses 'sorry' and/or contains errors

What's happening here?

[Marcus Rossel]

I think the unknown identifier message is just unfortunate and the problem is actually related to the use of ← in do-notation. If you try this, it works:

def oops : IO String := do
  let var ← if let some opt := getOption "str" then getIOString opt else return "no option"
  return var

[Utensil Song]

Yes, that's the also_works case . I wonder why this message would show up, usually if I use := incorrectly I would get an error tell me to use the arrow.

[Utensil Song]

Seems some info is unavailable to Lean during elaboration

[Marcus Rossel]

Oh sorry, I totally ignored the other definitions :see_no_evil:

[Eric Wieser]

The fact this fails looks like expected behavior to me; after the := you are no longer in a monadic context, so the (<- getIOString opt) has to be lifted all the way before it

[Eric Wieser]

I'm a bit surprised this doesn't work

def also_works : IO String := do
  let var := (<- if let some opt := getOption "str" then
    let ret := (<- getIOString opt)
    pure ret
  else
    pure "no option")

I thought that let x <- f and let x := (<- f) meant the same thing

[Mario Carneiro]

it does work

[Mario Carneiro]

but the entire do block has no return value, so it complains about a Unit/ String mismatch on the last line

[Mario Carneiro]

putting _ after the do block makes the error go away

[Mario Carneiro]

Oh! The version with let x <- f has no errors, which is definitely a bug (it apparently just ignores the x binding and returns f to the do block)

[Utensil Song]

Eric Wieser said:

The fact this fails looks like expected behavior to me; after the := you are no longer in a monadic context, so the (<- getIOString opt) has to be lifted all the way before it

Yes, this fails is expected, actually I was fiddling deep in levels of nesting even forgot the := that was already there so I didn't realize why until I minimize it. But the real wierd thing is the error unkown identifier, which creeps me out as it's another level of horror.

Usually, when I misuse :=, <-, := (<- ...), I get an informative error.

1. expect <-, misuse :=

The error propagates down to

type mismatch, result value has type
  String : Type
but is expected to have type
  IO String : Type

which reminds me I'm dealing with Monad

2. expect :=, misuse `<-'

type mismatch
  "str"
has type
  String : Type
but is expected to have type
  IO ?m.1506 : Type

which also reminds me.

3. even better, in if let, expect :=, misuse `<-', gives me:

unexpected token '<-'; expected ':=' or '←'

4. in if let, expect := (<- ... ), misuse :=gives me type mismatch, misuse <- gives me unexpected token '<-'; expected ':=' or '←' which corner me to := (<- ...).

[Utensil Song]

I'll make a longer #mwe to produce all these in a sec.

[Mario Carneiro]

lean4#2676

[Utensil Song]

EDIT: the following is improved and published to a LeanInk annotated output : https://utensil.github.io/lean-playground/Zulip/Arrow.html

import Lean
open Lean System

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

def getIO (str : String) : IO String := pure str

def getOptIO (str : String) : IO (Option String) := pure (some str)

-- if let return
def works₁ : IO String := do
  if let some opt := getOpt "str" then
    let ret := (<- getIO opt)
    return ret
  else
    return "none"

#eval works₁ -- works "str"

-- let var <- if let
def works₂ : IO String := do
  let var <- if let some opt := getOpt "str" then
    let ret := (<- getIO opt)
    pure ret
  else
    pure "none"

  return var

#eval works₂ -- works: "str"

-- let var := if let
def oops₀ : IO String := do
  let var := if let some opt := getOpt "str" then
    let ret := (<- getIO opt)  -- unknown identifier 'opt'
    ret
  else
    "none"

  return var

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

def oops₁₁ : IO String := do
  let some ret := getOptIO "str"
  ret -- unknown identifier 'ret'

def oops₁₂ : IO String := do
  let some ret := getOptIO "str" | pure "none" -- type mismatch: `IO (Option String)` got `Option ?m.2842`
  pure ret

def works₁₃ : IO String := do
  let some ret <- getOptIO "str" | pure "none"
  pure ret -- works

-- 2. expect `:=`, misuse `<-`
def oops₂ : IO String := do
  let io <- getIO "str"
  io -- type mismatch: expected `IO String`, got `String`

-- 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"

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

-- 4.1 misuse `:=` gives me type mismatch

def oops₄₁ : IO String := do
  if let some opt := getOptIO "str" then -- type mismatch: expected `IO (Option String)`, got `Option ?m.3586`
    let ret <- getIO opt
    pure ret
  else
    pure "none"

-- 4.2 misues `<-`
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"

def works₄₃ : IO String := do
  if let some opt := (<- getOptIO "str") then
    let ret <- getIO opt
    pure ret
  else
    pure "none"

[Utensil Song]

OK, I've got all the variants I want to try, don't know if lean4#2676 fixes them all.

[Utensil Song]

The key ones are

• oops₀:
  • let var := if let
  • gives unknown identifier
• oops₁₁
  • expect <-, misuse :=
  • gives unknown identifier
• oops₄
  • in if let, forces (<- ... )

[Eric Wieser]

@Mario Carneiro, forgetting the final return was a typo. This still doesn't work:

import Lean
open Lean System

def getOption (str : String) : Option FilePath := str

def getIOString (file : FilePath) : IO String := do
  return file.toString

def also_works : IO String := do
  let var := (<- if let some opt := getOption "str" then
    let ret := (<- getIOString opt)
    pure ret
  else
    pure "no option")
  pure var

[Eric Wieser]

(but works fine if I replace := (<- ...) with <- ...)

[Utensil Song]

Idk how to try the Lean in PR...

[Mario Carneiro]

this is I guess semi-expected

[Mario Carneiro]

in the variation := (<- ...) the if let expression is treated as a term, because (<- ...) takes a term. Thus the inner <- getIOString needs to be hoisted out of it (and because of another bug lean doesn't give a nice error message saying it can't lift <- over a binder like it normally does) and you get an unknown variable error

[Mario Carneiro]

In the variation <- ... the if let is a doElem, because the let x <- ... doElem takes a doElem on the RHS (and it specially forbids things like let x <- let y <- 1 which are otherwise syntactically correct). I believe the reason this is done is so that control flow like if and match are still considered to be part of the same do block

[Utensil Song]

Utensil Song said:

The key ones are

• oops₀:
  • let var := if let
  • gives unknown identifier
• oops₁₁
  • expect <-, misuse :=
  • gives unknown identifier
• oops₄
  • in if let, forces (<- ... )

I can't relate the tests added in PR to these oops. The 2nd test gives me unknown identifier, the 1st test gives me:

image.png

[Mario Carneiro]

the second test is a separate bug, I thought it was a duplicate but it's not

[Mario Carneiro]

the first test gives the error you are showing without the fix, but the fix should make it pass

[Eric Wieser]

Ah, so it sounds like the transformation is actually from let x <- f g to let x := (<- do f g)?

[Mario Carneiro]

...does that work? I would expect it to have a separate scope for mutation but now I'm not sure

[Mario Carneiro]

no luck:

#eval Id.run do
  let mut x := 1
  let y := (← do
    x := x + 1 -- `x` cannot be mutated
    pure ())
  pure x

[Mario Carneiro]

this is because the do term starts a new scope for mutation, return etc while the do doElem is just a grouping construct (i.e. it's the same issue)

[Scott Morrison]

Utensil Song said:

Idk how to try the Lean in PR...

@Utensil Song, once the PR compiles, you will be able to use it by setting your lean-toolchain to leanprover/lean4-pr-releases:pr-release-2676.

[Scott Morrison]

Alternatively you can compile the PR locally and use elan override set following the instructions at https://lean-lang.org/lean4/doc/dev/index.html

[Utensil Song]

info: downloading component 'lean'
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
error: could not download nonexistent lean version `leanprover/lean4-pr-releases:pr-release-2676`
info: caused by: could not download file from 'https://github.com/leanprover/lean4-pr-releases/releases/expanded_assets/pr-release-2676' to '/Users/utensil/.elan/tmp/f52sgiqoibbyouat_file'
info: caused by: http request returned an unsuccessful status code: 404

Maybe this method won't work for Mac M1? It seems most of the CI has passed. But maybe can't try it on Linux yet as well since one of the Linux CIs gives

[    ] Building Lean/Elab/Binders.lean
Lean/PrettyPrinter/Delaborator/Builtins.lean:672:4: error: application type mismatch
  pure PUnit.unit
argument
  PUnit.unit
has type
  PUnit : Sort ?u.538015
but is expected to have type
  Syntax × Name : Type

EDIT: tested on Codespaces (Ubuntu), not working either. (EDIT: I realized that I should check toolchain-available label first, I thought the release CI has passed).

I'll try to build Lean now (following nix setup, ~45min on Codespaces).

[Utensil Song]

Tests from the PR pass for me, but oops₀, oops₁₁ and oops₄ are not fixed per my test (same errors), and I've confirmed the Lean version by #eval Lean.githash to be "4bb9a11e0c13a82682af6238e237f05e95a989ac" immediately before oops.

Don't know if I have missed something.