Application type mismatch in simp involving dsimp theorem

Prerequisites

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

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• 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

Internal error in simp. MWE:

def f (_ : List Empty) (b : Bool) := b

-- It matters that this is a `dsimp` lemma.
@[simp] theorem lem1 (a : Bool) : f [] a = a := rfl

@[simp] axiom lem2 (a b : Bool) (x y : List Empty)
  (h : f x a = f y b) : x = y

example : (([] : List Empty).take 0) = [] := by simp
/-
application type mismatch
  Eq.mpr (congrArg (fun x => f x (f ?y ?b) = f ?y ?b) List.take_nil) rfl
argument
  rfl
has type
  f ?y ?b = f ?y ?b : Prop
but is expected to have type
  f [] (f ?y ?b) = f ?y ?b : Prop
-/

Versions

"4.12.0-nightly-2024-10-13"

According to the original report, this is a regression from 4.11rc2.

Additional Information

Originally reported on Zulip.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the self-contained reproducer from the issue against Lean nightly 4.12.0-nightly-2024-10-13 and a known-good 4.11rc2 to confirm the regression. Investigate the simp handling of dsimp lemmas, especially lem1 and lem2, and use the reported application type mismatch as the failure criterion. Done means the example no longer produces an internal error while preserving the intended simplification.