Zulip Chat Archive

Stream: general

Topic: has_coe_to_fun with implicit arguments

view this post on Zulip Neil Strickland (Jul 15 2019 at 10:46):

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
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?

view this post on Zulip Chris Hughes (Jul 15 2019 at 11:06):

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.

view this post on Zulip Neil Strickland (Jul 15 2019 at 11:20):

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.

view this post on Zulip Simon Hudon (Jul 15 2019 at 13:23):

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

Last updated: May 13 2021 at 05:21 UTC