Coercing linear maps to functions

Stream: general

[Anne Baanen]

I'm experiencing problems coercing linear maps to functions. For example:

import algebra.module
set_option pp.all true
def foo {α : Type} [ring α] (x : α) : α →ₗ[α] α := sorry
example {α} [ring α] (x y : α) : (foo x).to_fun y = (foo x).to_fun y := sorry -- works
example {α} [ring α] (x y : α) : @foo α _ x y = @foo α _ x y := sorry -- works
example {α} [ring α] (x y : α) : foo x y = foo x y := sorry -- error at `foo`: function expected
example {α} [ring α] (x y : α) : coe_fn foo x y = coe_fn foo x y := sorry -- error at `coe_fn` is the same

The error for foo x y is, with pp.all enabled:

function expected at
  @foo α ?m_1 x
term has type
  @linear_map.{0 0 0} α α α ?m_1 (@ring.to_add_comm_group.{0} α ?m_1) (@ring.to_add_comm_group.{0} α ?m_1)
    (@ring.to_module.{0} α ?m_1)
    (@ring.to_module.{0} α ?m_1)

Passing α (or the comm_ring instance) explicitly does fix the issue as the second working example shows, but shouldn't α be determined automatically from the type of x? And if not, why is it shown with pp.all enabled? I don't really understand what I'm doing wrong here.

[Anne Baanen]

The linear_algebra lemmas all use coercion to go from linear maps to functions, so I'd prefer that over writing (foo x).to_fun.

[Reid Barton]

This is the same as the equiv coercion issue. If you have e : equiv a b and you want to form the application e x where x : a, it only works if a and b don't contain metavariables. But often e is some term (like your foo) in which you want to determine a metavariable from the type of x, but that's impossible because then the coercion cannot fire yet.

[Reid Barton]

I think the core problem was that type instance search won't fire when the goal type still contains metavariables.