inferring arguments for FunLike classes

Stream: mathlib4

[David Loeffler]

If I define a function which depends on some implicit parameters, and then I apply my function to something, Lean will try to figure out the implicit arguments from the types of the explicit ones.

However, when I define, rather than a function, some bundled FunLike thing, it seems that this doesn't apply: the implicit-parameter inference process doesn't "see through" the coercion-to-a-function operation. Is there a way of getting around this?

To be much more concrete: the following works, to define the "shift operator" that sends a function f : A → B to the function a ↦ f (a + 1), where A is a ring and B an abelian addgroup:

variable {A B : Type*} [Ring A] [AddCommGroup B]

/-- Shift-by-1 operator -/
def shift (f : A → B) := fun a ↦ f (a + 1)

variable (f : A → B) in
#check shift f -- works

Here the types A and B are implicit parameters to shift, but it can correctly deduce these from the type of f. However, if I define shiftₗ to be the same thing bundled as a linear operator on functions, not just a bare map, it seems to be unable to use f to figure out the type arguments to shiftₗ:

variable {A B : Type*} [Ring A] [AddCommGroup B]

/-- Shift-by-1 operator bundled as `ℤ`-linear endomorphism -/
def shiftₗ : Module.End ℤ (A → B) where
  toFun f a := f (a + 1)
  map_add' f g := by ext; simp
  map_smul' r f := by ext; simp

variable (f : A → B) in
#check shiftₗ f -- fails: function expected ... term has type Module.End ℤ (?m.5014 → ?m.5015)

variable (f : A → B) in
#check @shiftₗ A B _ _ f -- works, but ugly

Is there some clever hack that will allow me to write shiftₗ f without explicitly giving the types?

[Jireh Loreaux]

I've seen this kind of thing, before, but not for a long time. I think it's something to do with linear maps specifically. Note that the same problem does not exist if you make shiftₗ and AddMonoidHom, for instance.

[David Loeffler]

Interesting! It does indeed work bundled as an AddMonoidHom. Unfortunately I really do need to bundle it in some way that gives a ring structure, since I want to write things like (shiftₗ - 1)^7 f.

[Jireh Loreaux]

certainly, I'm not saying that you shouldn't be able to have the linear map version, I'm just trying to help narrow down where the problem occurs, because Lena definitely should be able to do this. I had similar issues about 10 months ago with star algebra homomorphisms, because those went away (I don't recall what the fix was, but I didn't implement it), so I'm surprised it's back.

[David Loeffler]

(the motivation here is to get Newton's formula for forward differences by applying the binomial theorem inside the ring Module.End ℤ (A → B).)

[David Loeffler]

Another remark about this: oddly, for shiftₗ applied to a function A → B, it seems to be able to figure out A, but not B: that is,

#check shiftₗ (A := A) f  -- fails
#check shiftₗ (B := B) f  -- works