has_coe_to_fun with implicit arguments

Stream: general

[Neil Strickland]

I am having trouble getting has_coe_to_fun to work with implicit arguments in the way that I would like. Consider the following:

import data.rat.basic linear_algebra.basic

variables {V : Type*} [add_comm_group V] [module ℚ V]

def f : V →ₗ[ℚ] V :=
{ to_fun := λ (v : V), v,
  add := λ (v w : V), rfl,
  smul := λ (c : ℚ) (v : V), rfl }

def f1 : V → V := (f : V →ₗ[ℚ] V)
def f2 (v : V) : V := (f : V →ₗ[ℚ] V) v
def f3 (v : V) : V := f v

Definitions f1 and f2 work (via the has_coe_to_fun instance for linear_map) but they are awkward. Definition f3 does not work: Lean says

function expected at
  f
term has type
  ?m_1 →ₗ[ℚ] ?m_1
Additional information:
c:\Users\Neil Strickland\Google Drive\Lean\lib\src\algebra\linmap.lean:10:22: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  too many arguments

I don't understand where "too many arguments" is coming from. Is there a way around this?

[Chris Hughes]

Too many arguments is because a term of type V →ₗ[ℚ] V takes no arguments before it is coerced, so one argument is too many. I think def f3 (v : V) : V := (f : V -> V) v should work.

[Neil Strickland]

In fact def f3 (v : V) : V := (f : V → V) v gives

invalid type ascription, term has type
  ?m_1 →ₗ[ℚ] ?m_1 : Type ?
but is expected to have type
  V → V : Type u_1

I'm not sure why that is. Anyway, in the situation that led me to this minimal example, the term corresponding to V is rather large, so I want to avoid having to mention it if possible.

[Simon Hudon]

One thing that always gave me trouble with has_coe_to_fun is when I would hope that the type of the argument would help infer some of the parameters of the type of the object being coerced to function. Would thing that would help is make V an explicit parameter and call f as f V v