regression in dot notation

Stream: lean4

[Kevin Buzzard]

In Lean 3 this works:

import data.polynomial.derivative

#check @polynomial.derivative
/-
polynomial.derivative : Π {R : Type u_1} [_inst_1 : semiring R], polynomial R →ₗ[R] polynomial R
-/

variables (R : Type) [comm_ring R] (f : polynomial R)
#check f.derivative -- works fine

In Lean 4 it doesn't work any more:

import Mathlib.Data.Polynomial.Derivative

#check Polynomial.derivative
/-
Polynomial.derivative.{u} {R : Type u} [inst✝ : Semiring R] : Polynomial R →ₗ[R] Polynomial R
-/

variable (R : Type) [CommRing R] (f : Polynomial R) in
#check f.derivative
/-
invalid field notation, function 'Polynomial.derivative' does not have argument with type
(Polynomial ...) that can be used, it must be explicit or implicit with a unique name
-/

IIRC it worked in mathlib3 because someone (@Kyle Miller ?) made a change to core Lean so that dot notation would spot that this was OK -- it sees that there's a coercion to function from Polynomial R →ₗ[R] Polynomial R to Polynomial R → Polynomial R. Is there any chance that this is coming back in Lean 4? It's making the port of Hermite polynomials !4#3967 look a lot more verbose than the corresponding Lean 3 file. I'm assuming that it can't be fixed in mathlib?

[Kyle Miller]

That was already a Lean 3 feature before me (I just made it more reliable as part of making dot notation work somewhat more like Lean 4's; lean#757).

I'm not sure what's the current state of the discussion about how to support this in Lean 4, but I know that there's an issue for it.

[Eric Rodriguez]

this feature is kind of still unreliable in lean3; I think a really robust way to write this would be quite nice.

[Eric Rodriguez]

(for example: in neither Lean3 or Lean4 can you write p.aeval - I understand why this is but I think it would be very nice to be able to write it)

[Eric Rodriguez]

I guess the issue with what I'm asking is that p.aeval is not super well defined (it'd be like (\lam x, Polynomial.aeval x p))