INTERNAL PANIC: unreachable code has been reached

[gyk]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [X] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [ ] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

My code #evals to correct result, but running the executable built from it triggers a panic: "INTERNAL PANIC: unreachable code has been reached".

Steps to Reproduce

1. lake new Tree

2. Edit the code:

   -- ./Tree/Basic.lean
   inductive Tree : Nat → Type where
     | leaf : Nat → Tree 0
     | branch : {d: Nat} → Tree d → Tree d → Tree (d + 1)
   
   instance : ToString (Tree 0) where
     toString : Tree 0 → String
     | .leaf k => s!"Leaf({k})"
   
   instance [ToString (Tree d)] : ToString (Tree (d + 1)) where
     toString : Tree (d + 1) → String
     | .branch l r => s!"Branch({toString l}, {toString r})"
   

   -- ./Main.lean
   import Tree
   
   def myTree :=
     Tree.branch
       (Tree.branch (Tree.leaf 0) (Tree.leaf 1))
       (Tree.branch (Tree.leaf 2) (Tree.leaf 3))
   
   def main : IO Unit :=
     IO.println s!"{myTree}"
   

3. lake build

4. Run the executable:

   Tree> .\.lake\build\bin\tree.exe
   INTERNAL PANIC: unreachable code has been reached
   

Versions

Lean 4.9.0, 4.12.0 (x86_64-w64-windows-gnu, commit dc2533473114, Release) Windows 11 23H2

[tydeu]

To elaborate on the problem here a bit: there are empty closed terms in main, so the underlying problem is similar to #1965.

set_option trace.compiler.ir.result true in
def main : IO Unit :=
  IO.println s!"{myTree}"

[result]
def main._closed_1 : obj :=
  let x_1 : obj := "";
  ret x_1
def main._closed_2 : obj :=
  ⊥
def main._closed_3 : obj :=
  let x_1 : obj := main._closed_2;
  let x_2 : obj := main._closed_1;
  let x_3 : obj := String.append x_1 x_2;
  dec x_2;
  ret x_3
...

[zwarich]

This is now fixed by the new compiler. I think something slightly different from #1965 was going on here.