Polynomial.aeval broke

Stream: mathlib4

[Yongyi Chen]

Importing all of mathlib breaks usage of aeval:

import Mathlib

open Polynomial

/-
function expected at
  aeval 1
term has type
  ?m.5[X] →ₐ[?m.5] ℤ
-/
theorem t1 : aeval (1 : ℤ) (0 : ℤ[X]) = 0 := by exact (aeval 1).map_zero'

/-- Fine -/
theorem t2 : (aeval (1 : ℤ)).toFun (0 : ℤ[X]) = 0 := by exact (aeval 1).map_zero'

Not importing all of Mathlib does not give that error.

import Mathlib.Data.Polynomial.AlgebraMap

open Polynomial

/-- Fine -/
theorem t1 : aeval (1 : ℤ) (0 : ℤ[X]) = 0 := by exact (aeval 1).map_zero'

/-- Fine -/
theorem t2 : (aeval (1 : ℤ)).toFun (0 : ℤ[X]) = 0 := by exact (aeval 1).map_zero'

[Eric Wieser]

This shortcut instance seems to fix it:

instance {R A B} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :
  FunLike (A →ₐ[R] B) A (fun _ => B) := inferInstance

[Jireh Loreaux]

@Eric Wieser this has been a problem for a while, but I haven't had time / remembered to track it down. I think this is caused by a bad instance somewhere (like we had for Module.Dual a while back that also caused breakage). Do you have any idea what the problem is here?

[Eric Wieser]

No, but note that the shortcut instance above matches a pattern of instances that we had in lean 3 but made a mess of (and deleted) during the port

[Eric Wieser]

It would be good to track down exactly which import causes it

[Eric Rodriguez]

import Mathlib.Analysis.NormedSpace.Spectrum

open Polynomial

/-
function expected at
  aeval 1
term has type
  ?m.5[X] →ₐ[?m.5] ℤ
-/
theorem t1 : aeval (1 : ℤ) (0 : ℤ[X]) = 0 := sorry

seems to be one minima

[Eric Rodriguez]

is there any way to get the list of all files that do _not_ transitively import a file?

[Eric Rodriguez]

(i.e. everything that does not have NormedSpace.Spectrum as a parent)

[Eric Rodriguez]

it'd be nice for making sure it's specifically this file

[Eric Rodriguez]

instance (priority := 100) [AlgHomClass F 𝕜 A 𝕜] : ContinuousLinearMapClass F 𝕜 A 𝕜 := seems to be the culprit

[Eric Rodriguez]

another workaround is the direct

instance : CoeFun (A →ₐ[R] B) (fun _ ↦ A → B) where
  coe := fun x ↦ x.toFun

which would line up with my proposed fix to FunLike

[Eric Wieser]

That instance you propose is bad without the context of a huge refactor

[Eric Rodriguez]

I am indeed proposing that refactor (making FunLike.coe not an instance, and requiring all FunLike to require their own CoeFun instance) - see here