simp fails with "application type mismatch"

Stream: lean4

[Sven Manthe]

After updating Lean from 4.11rc2 to 4.13rc3, simp caused an application type mismatch. It was fixed by removing a simp annotation that made no sense anyway, but since https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp.20failing.20with.20.22application.20type.20mismatch.20.20.20Eq.2Endrec.20.2E.2E.2E.22 suggests that such an error may be a bug, I decided to post a MWE:

def f (_ : List Empty) (b : Bool) := b
@[simp] theorem lem1 (a : Bool) : f [] a = a := rfl
@[simp] theorem lem2 (a b : Bool) (x y : List Empty)
  (h : f x a = f y b) : x = y := by rcases x with _ | ⟨⟨⟩, _⟩; rcases y with _ | ⟨⟨⟩, _⟩; rfl
example : (([] : List Empty).take 0) = [] := by simp

[Jannis Limperg]

lean4#5702

[Jannis Limperg]

Thanks! Please feel free to report clear bugs like this one directly as Lean issues.