Unreachable code with precompileModules

Stream: lean4

[Christian Merten]

I am hitting a

INTERNAL PANIC: unreachable code has been reached
error: external command `/home/christian/.elan/toolchains/leanprover--lean4---stable/bin/lean` exited with code 1

error with latest stable release when using precompileModules. This is my lakefile.lean:

import Lake
open System Lake DSL

package unreachable {
  /- Setting this to `false` makes it work -/
  precompileModules := true
}

lean_lib Unreachable

@[default_target] lean_exe test {
  root := `Main
}

Main.lean is

import Unreachable.Fails

def main : IO Unit := do
  IO.println "hi"

and Unreachable/Fails.lean is

inductive World where
  | elementary
  | composed

/- Dropping the elementary constructor makes it work.-/
inductive EType : World → Type where
  | elementary : EType .elementary
  | composed (name : String) : EType .composed

def Composed : Type := EType .composed

/- Changing this to `def` makes it work. -/
abbrev Composed.name (s : Composed) : String :=
  match s with
  | .composed name => name

/- Dropping this def makes it work. -/
def Composed.toString (c : Composed) : String :=
  s!"column {c.name}"

[Kim Morrison]

Could you please open an issue with this repro?

[Christian Merten]

lean4#3251