Importing Mathlib breaks `Polynomial.aeval`

Stream: mathlib4

[Oliver Nash]

Can anyone explain this:

[Oliver Nash]

import Mathlib.Data.Polynomial.AlgebraMap
import Mathlib

variable {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] {a : A} {p : Polynomial R}

#check Polynomial.aeval a p -- Works only when `import Mathlib` omitted
#check Polynomial.aeval (R := R) a p -- Always works

[Ruben Van de Velde]

With error

function expected at
  Polynomial.aeval a
term has type
  Polynomial ?m.539 →ₐ[?m.539] A

Is this related to the big FunLike refactor?

[Oliver Nash]

Not to my knowledge. The above is on master FWIW.

[Ruben Van de Velde]

Oh, look: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Polynomial.2Eaeval.20broke

[Jireh Loreaux]

See here:
Jireh Loreaux said:

Perhaps you've had problems elaborating AlgHoms or StarAlgHoms. If so, I've come across two instances (I think I added them) that are causing the pain.

[Jireh Loreaux]

That's the only way I can figure out how to link to a thread on mobile.

[Oliver Nash]

Thank you both!

[Jireh Loreaux]

Upshot, it's fixed with #8386 but you could temporarily disable those instances.

[Oliver Nash]

(This isn't even hitting me, I just wanted to run #find_home with everything imported.)

[Oliver Nash]

For posterity I will record that adding:

attribute [-instance] AlgHom.instContinuousLinearMapClassToSemiringToDivisionSemiringToSemifieldToFieldToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToNonUnitalSeminormedCommRingToModuleToSeminormedAddCommGroupToNonUnitalSeminormedRingToNonUnitalNormedRingToNormedSpace'ToModuleToSeminormedAddCommGroupToNonUnitalSeminormedRingToNormedSpace

fixes this issue.