## Stream: general

### Topic: Coercing linear maps to functions

#### Anne Baanen (Jan 21 2020 at 14:33):

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 (Jan 21 2020 at 14:34):

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 (Jan 21 2020 at 15:07):

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 (Jan 21 2020 at 15:08):

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

Last updated: Aug 03 2023 at 10:10 UTC