PANIC at Lean.Compiler.LCNF.Simp.inlineProjInst?.visit

[semorrison]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Code below causes a PANIC

Steps to Reproduce

class F (α : Sort _) extends Inhabited α

instance : F True where
  default := trivial

example : False := by simp -- PANIC doesn't happen under `lake` unless there is an error earlier in the file.

def X (α β) [F α] : (α → β) → β :=
  fun f => f default

def Y (α : Sort _) : (True → α) → α :=
  X _ _ -- PANIC

Expected behavior: [What you expect to happen]

An error at example : False := by simp, but no panic.

Actual behavior: [What actually happens]

PANIC at Lean.Compiler.LCNF.Simp.inlineProjInst?.visit Lean.Compiler.LCNF.Simp.InlineProj:59:34: unreachable code has been reached

Versions

Lean (version 4.0.0-nightly-2022-11-10, commit 2386c40, Release)