Unreachable code in #eval from infinite loop

Stream: lean4

[Thomas Murrills]

I noticed the following:

import Lean

partial def loop (n : Nat) : Bool := loop n
#eval loop 4 -- unreachable code

Interestingly, this behavior changes (to hanging as expected) if imports are removed. (Any import I've tried seems to be sufficient to produce 'unreachable code', not just import Lean.)

I'm reporting this just in case it's a bug. :)

[Damiano Testa]

I think that importing Lean.Message gives unreachable code, but importing any of its imports hangs.

[Thomas Murrills]

By deleting content in that file, I've minimized it further now to

import Lean.Util.PPExt
import Lean.Util.Sorry

namespace Lean

inductive MessageData where
  | ofFormatWithInfos : FormatWithInfos → MessageData
  | ofLazy (f : Option PPContext → BaseIO Dynamic) (hasSyntheticSorry : MetavarContext → Bool)
  deriving TypeName

namespace MessageData

def ofFormat (fmt : Format) : MessageData := .ofFormatWithInfos ⟨fmt, .empty⟩

def ofExpr (e : Expr) : MessageData :=
  .ofLazy
    (fun ctx? => do
      let msg ← ofFormatWithInfos <$> match ctx? with
        | .none => pure (format (toString e))
        | .some ctx => ppExprWithInfos ctx e
      return Dynamic.mk msg)
    (fun mctx => instantiateMVarsCore mctx e |>.1.hasSyntheticSorry)

partial def loop (n : Nat) : Bool := loop n
#eval loop 4 -- unreachable code

Changing the names of ofExpr and ofFormat results in hanging. I haven't tried editing their bodies yet.

[Damiano Testa]

Changing the names that are not later referenced! :open_mouth:

[Thomas Murrills]

Maybe this reveals the issue somewhat:

namespace Lean.MessageData

def ofFormat : Bool := true

partial def loop (n : Nat) : Bool := loop n
#eval loop 4 -- function expected ofFormat (repr (loopBool 4))

(No imports!)

[Damiano Testa]

Well, you could minimize it further by evaluating at 0, instead of 4. :lol:

[Damiano Testa]

You can also inline the namespace in ofFormat, if you prefer.

[Aaron Liu]

It's probably to do with how #eval displays the output

[Thomas Murrills]

Lean.MessageData.ofFormat and Lean.MessageData.ofExpr must be special-cased somewhere. It looks like docs#Lean.Elab.Command.elabEvalCoreUnsafe, here, with ofExpr looked for here

[Thomas Murrills]

Aaron Liu said:

It's probably to do with how #eval displays the output

True, but it's a bit strange that there shouldn't be any output to display...

[Thomas Murrills]

It seems that #eval compiles a definition of type MessageData whose body is ofExpr (toExpr (loop 4)), and then evalConst is called on this, which produces the error. In fact, ofExpr is irrelevant, and we find

import Lean
open Lean

partial def loop (n : Nat) : Bool := loop n
def foo : Expr := toExpr (loop 4)
run_cmd evalConst Expr ``foo -- unreachable code

or more generally

import Lean

open Lean

partial def loop (n : Nat) : Bool := loop n
def foo : String := if loop 4 then "yes" else "no"
run_cmd evalConst String ``foo -- unreachable code

Replacing String with Bool causes hanging (any other non-bool type seems to cause unreachable code).

[Thomas Murrills]

Interestingly, changing the body of loop as follows changes the behavior:

• match n with | 0 => true | n => loop n: hangs
• true || loop n: returns true (expected, I'm guessing loop n is optimized away here)
• loop (n+1), false || loop n, loop n || true: unreachable code

[Thomas Murrills]

evalConst quickly bottoms out in an extern, so for now, this is as far as I go. :)

[Thomas Murrills]

Wait, I just realized that run_cmd calls elabEvalCoreUnsafe—so maybe my conclusions aren't quite right here.

[Thomas Murrills]

Perhaps this is a bit more convincing, but I'm still unsure if there's any weirdness in elab and the unsafe wrapper.

import Lean

open Lean

partial def loop (n : Nat) : Bool := loop n
def foo : String := if loop 4 then "yes" else "no"
elab "#test" : command => discard <| unsafe evalConst String ``foo

#test -- unreachable code

[Kyle Miller]

#eval changes behavior depending on what's imported; it falls back on some simpler pretty printing methods if certain definitions aren't available.

I don't know why sometimes it's unreachable and sometimes it loops, but the key to why it's ever printing unreachable code is that the compiler is allowed to assume that all functions halt.

If you take a look at the IR when set_option trace.compiler.ir true is enabled, you can see that the _eval definition reduces to

def _eval : obj :=
      ⊥

The first hint of bottom being introduced is the elim_dead_branches pass.