instance breaking FunLike

Stream: mathlib4

[Kevin Buzzard]

In this code

import Mathlib.Data.Polynomial.Derivative
import Mathlib.LinearAlgebra.Dual

-- uncomment this line to fix the file
--attribute [-instance] Module.Dual.instFunLikeDual

--set_option trace.Meta.synthInstance true in
noncomputable example (R : Type) [CommSemiring R] (f : Polynomial R) : Polynomial R :=
  Polynomial.derivative f -- error: function expected at derivative

the example doesn't work, but if you remove the instance which is breaking it then it does work. With the "bad" instance removed, set_option trace.Meta.synthInstance finds LinearMap.instFunLikeLinearMap. But with the bad instance present Lean seems to use it and then give up. Any ideas about how to fix this?

[Jireh Loreaux]

Kevin, see also this thread. The docs#Module.Dual.instFunLikeDual instance is not actually necessary (because Module.Dual is reducible), but it still shouldn't cause this breakage. I think there are other instances like this breaking things in the library.

[Kevin Buzzard]

Oh weird that we both found this issue this week!

[Kyle Miller]

At some point during porting in #3659, Module.dual went from being semireducible (like in mathlib3) to reducible, just in case anyone is wondering why this instance exists.

[Eric Wieser]

docs3#module.dual is also reducible (but in mathlib3 it was changed to be so during the port)

[Kyle Miller]

Right, I meant to say "like in mathlib3 at the time". It was backported in mathlib#18963