logic.equiv.defs causing elaboration issues in Simps tests

Stream: mathlib4

[Yakov Pechersky]

https://github.com/leanprover-community/mathlib4/actions/runs/3458597486/jobs/5773179498#step:6:204
An example of the offending test is:

example {α} (x y : α) (h : x = y) : foo.rfl.toFun x = y := by simp <;> rw [h]
/-
application type mismatch
  Eq
argument has type
  Sort u_1
but function has type
  {α : Prop} → α → α → Prop
-/

Strangely, changing to a named theorem makes it work:

theorem bar {α} (x y : α) (h : x = y) : foo.rfl.toFun x = y := by simp <;> rw [h]

[Yakov Pechersky]

Partial mwe:

import Mathlib.Tactic.Simps.Basic
import Mathlib.Init.Function

class Unique (α : Sort u) extends Inhabited α where
  uniq : ∀ a : α, a = default

/- comment out following lemma to make the example at the bottom work-/
attribute [simp] eq_iff_true_of_subsingleton in
theorem Unique.bijective {A B} [Unique A] [Unique B] {f : A → B} : Function.Bijective f := sorry

structure Equiv' (α : Sort _) (β : Sort _) :=
(toFun    : α → β)
(invFun   : β → α)
(left_inv  : invFun.LeftInverse toFun)
(right_inv : invFun.RightInverse toFun)

namespace foo
@[simps] protected def rfl {α} : Equiv' α α :=
⟨id, λ x => x, λ _ => rfl, λ _ => rfl⟩

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

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

end foo

[Yakov Pechersky]

Minimized in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/application.20type.20mismatch.20in.20example/near/309532841.2E01

[Kevin Buzzard]

lean4#1814 also mentioned eq_iff_true_of_subsingleton but I don't know if this is a red herring