application type mismatch in example

Stream: lean4

[Yakov Pechersky]

Consider the following MWE:

theorem iff_of_true (ha : a) (hb : b) : a ↔ b := ⟨fun _ => hb, fun _ => ha⟩
theorem iff_true_intro (h : a) : a ↔ True := iff_of_true h ⟨⟩
theorem eq_iff_true_of_subsingleton [Subsingleton α] (x y : α) : x = y ↔ True :=
  iff_true_intro (Subsingleton.elim ..)

/- comment out following `attribute [simp]` to make the example at the bottom work-/
attribute [simp] eq_iff_true_of_subsingleton in
theorem problem : True := trivial

structure Func' (α : Sort _) (β : Sort _) :=
(toFun    : α → β)

namespace foo

protected def rfl {α} : Func' α α := ⟨id⟩

@[simp] theorem foo.rfl_toFun {α : Sort u_1} (a : α) : Func'.toFun foo.rfl a = id a := rfl

example {α} (x y : α) (h : x = y) : foo.rfl.toFun x = y := by simp <;> rw [h]
/-
in the presence of `attribute [simp] eq_iff_true_of_subsingleton in`, one gets

application type mismatch
  Eq
argument has type
  Sort u_1
but function has type
  {α : Prop} → α → α → Prop
-/

theorem noissue {α} (x y : α) (h : x = y) : foo.rfl.toFun x = y := by simp <;> rw [h]
-- this doesn't complain!

end foo

Commenting out the attribute [simp] eq_iff_true_of_subsingleton in line makes the example work. The theorem noissue always works.

[Yakov Pechersky]

This is in the 2022-11-10 nightly.

[Scott Morrison]

This sort of thing can go direct to https://github.com/leanprover/lean4/issues

[Scott Morrison]

I reported it as lean4#1829