Compiler ICE

Stream: lean4

[Henrik Böving]

The 24-03 nightly has an ICE when declaring some module with the content:

inductive Step (α : Type u) where
  | impossible : α → Step α
  deriving Hashable

and importing it in some other module, the panic is:

error: PANIC at Lean.Expr.constName! Lean.Expr:624:19: constant expected

and most likely inside the Hashable derive handler since it disappears once that is removed

[Notification Bot]

Henrik Böving has marked this topic as resolved.

[Notification Bot]

Henrik Böving has marked this topic as unresolved.

[Leonardo de Moura]

Thanks for reporting the issue. Pushed a fix for this.

[Leonardo de Moura]

https://github.com/leanprover/lean4/commit/370e9c421f03ff93820909a30c602380725f1394