Panic (unreachable code has been reached) with quotients

Stream: lean4

[Snir Broshi]

def space : Type :=
  Quot (α := Bool × Bool) fun ⟨_, _⟩ ⟨_, _⟩ ↦ True

def subspace := { x : space // True }

def foo : subspace → subspace :=
  fun ⟨x, _⟩ ↦ x.lift sorry sorry

I wonder if this is what took down live.lean-lang.org right now (I'd guess it uses containers so no), or if there's an unrelated maintenance.
repros on nightly (4.28.0-nightly-2025-12-16)

PANIC at Lean.Compiler.LCNF.Expr.forFVarM Lean.Compiler.LCNF.FVarUtil:45:38: unreachable code has been reached
backtrace:
PANIC at Lean.Compiler.LCNF.Expr.forFVarM Lean.Compiler.LCNF.FVarUtil:45:38: unreachable code has been reached
backtrace:
PANIC at Lean.Compiler.LCNF.Expr.forFVarM Lean.Compiler.LCNF.FVarUtil:45:38: unreachable code has been reached
backtrace:
PANIC at Lean.Compiler.LCNF.Expr.forFVarM Lean.Compiler.LCNF.FVarUtil:45:38: unreachable code has been reached
backtrace:

[Snir Broshi]

Swapping Bool for a variable type gives a different unreachable panic:

variable (α : Type)

def space : Type :=
  Quot (α := α × α) fun ⟨_, _⟩ ⟨_, _⟩ ↦ True

def subspace := { x : space α // True }

def foo : subspace α → subspace α :=
  fun ⟨x, h⟩ ↦ x.lift sorry sorry

PANIC at _private.Lean.Compiler.LCNF.CompilerM.0.Lean.Compiler.LCNF.normExprImp.go Lean.Compiler.LCNF.CompilerM:204:20: unreachable code has been reached
backtrace:

[Henrik Böving]

Can you open an issue please?

[Snir Broshi]

Henrik Böving said:

Can you open an issue please?

Opened lean4#11719

[Henrik Böving]

lean4#11729 fixed