Function coercion does not trigger if types require unification

[gebner]

As reported on Zulip. This used to be supported in Lean 3 (community edition), and is used pretty heavily in mathlib:

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

Slightly simpler repro:

structure Fun (α β : Type) : Type where
  toFun : α → β

instance : CoeFun (Fun α β) (fun _ => α → β) where
  coe := Fun.toFun

example (f : Fun α β) : ∃ γ δ, γ → δ :=
  ⟨_, _, f⟩

The issue is that we try to synthesize the instance CoeT (Fun α β) f (?m → ?n), but that does not find anything since we can't assign ?m or ?n during TC search (and the last argument of CoeT is not an out param). In Lean 3, we used to check for has_coe_to_fn instances separately.

[gebner]

@leodemoura I can look into this, unless you have concerns about the feature.

[leodemoura]

@leodemoura I can look into this, unless you have concerns about the feature.

Thanks. If you have time, please go ahead.