DefEq transitivity failure for function eta #12520
Description
The type-checker applies function eta only when one side of the equation is a manifest lambda. But there are other forms where eta-expanding would be productive, e.g. partially applied Eq.rec. This leads to a intransitivity of defeq checking:
variable (a : true = true → Bool)
example : (@Eq.rec Bool true (fun _ _ => Bool) (a (Eq.refl true)) _) = fun h => a h := rfl
example : (fun h => a h) = a := rfl
/--
error: Type mismatch
rfl
has type
?m.8 = ?m.8
but is expected to have type
Eq.rec (a ⋯) = a
-/
#guard_msgs in
example : (@Eq.rec Bool true (fun _ _ => Bool) (a (Eq.refl true)) _) = a := rfl
This is similar in spirit to #2258. It seems to have low practical impact, reporting it here for reference.