Regression in function coercion inference

Stream: lean4

[Floris van Doorn]

I noticed a regression with function coercion inference compared to Lean 3.
It is not hard to work around it by giving some extra typing information, but this is a common occurrence in mathlib, and the workaround already occurs a few times in Mathlib4.

structure Equiv (α : Sort _) (β : Sort _) :=
(toFun    : α → β)
(invFun   : β → α)

local infix:25 " ≃ " => Equiv

variable {α β γ : Sort _}

instance : CoeFun (α ≃ β) (λ _ => α → β) := ⟨Equiv.toFun⟩

def Equiv.symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun⟩

protected def Equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩ -- both fields raise an error

[Scott Morrison]

I've been running into this too.

[Gabriel Ebner]

Filed as lean4#1725. It's not entirely trivial to fix this though, since the coercion code is scattered and partly duplicated over a couple of files right now.