simp not unifying partial application of structure projection

[Vierkantor]

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

In the mathlib4 port, certain simp lemmas that would apply in Lean 3 no longer apply in Lean 4 in the same case. It looks like this happens whenever we have a structure containing a field with a function, and a simp lemma is defined on the partially applied function in that field. simp has no trouble with partial application if it's on other definitions.

Steps to Reproduce

The following code contains two failing simp calls where rw succeeds. Equivalent code works fine in Lean 3.

structure BundledFunction (α β : Sort _) :=
(toFun : α → β)

namespace BundledFunction

-- `simp` doesn't seem to unify partial applications of structure projections:
-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60simp.60.20failing.20on.20partial.20application.20of.20projections
def id (α) : BundledFunction α α := ⟨λ a => a⟩

@[simp] theorem coe_id : (id α).toFun = _root_.id := rfl

example (x : α) : (id α).toFun x = x :=
by simp only [coe_id, id_eq] -- does not simplify anything
example (x : α) : (id α).toFun x = x :=
by rw [coe_id, id_eq] -- succeeds

-- seems to be another instance of the same behaviour:
-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60simp.60.20calls.20broken.20in.20mathlib4.23922/near/314790371

def otherProjection (f : BundledFunction α β) : α → β := f.toFun

@[simp] theorem toFun_eq_otherProjection : @toFun α β = otherProjection := rfl
@[simp] theorem id_apply : (id α).otherProjection x = x := rfl

example : (id α).toFun x = x := by simp only [toFun_eq_otherProjection, id_apply] -- does not simplify anything
example : (id α).toFun x = x := by rw [toFun_eq_otherProjection, id_apply] -- succeeds

end BundledFunction

-- `simp` is happy with partial applications in other functions:
def id2 (x : α) := x

@[simp] theorem id2_eq_id : @id2 α = id := rfl

example : id2 x = x := by simp only [id2_eq_id, id_eq] -- works fine
example : id2 x = x := by rw [id2_eq_id, id_eq] -- succeeds

Expected behavior: the simp calls on both lines marked -- does not simplify anything should solve the goal

Actual behavior: simp fails to rewrite. With trace.Meta.Tactic.simp on, the first simp call gives the following trace:

[Meta.Tactic.simp.unify] @BundledFunction.coe_id:1000, failed to unify
      (BundledFunction.id ?α).toFun
    with
      BundledFunction.toFun (BundledFunction.id α) x

Reproduces how often: always

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

$ lean --version
Lean (version 4.0.0-nightly-2022-12-09, commit 57a6aefb9240, Release)
$ uname -a
Linux vouwvervorming 6.0.10-arch2-1 #1 SMP PREEMPT_DYNAMIC Sat, 26 Nov 2022 16:51:18 +0000 x86_64 GNU/Linux

[leodemoura]

The commit above adds support for projection functions to our indexing data structure.
Note that @[simp] theorem toFun_eq_otherProjection : @toFun α β = otherProjection := rfl must be written as

@[simp] theorem toFun_eq_otherProjection : a.toFun = otherProjection a := rfl

to ensure the LHS is represented using a Expr.proj object (kernel projection) in our indexing data structure (i.e., discrimination tree).