MulActionHomClass cannot find synthesization order

Stream: mathlib4

[Kevin Buzzard]

tl;dr: I don't understand the cannot find synthesization order for instance error.

When diagnosing a timeout in an FLT PR I ran into the following thing. If S,R are commutative rings and R is an S-algebra, and if A and B are R-modules (and hence S-modules via IsScalarTower), then any R-linear map from A to B is S-linear. Typeclass inference was timing out when trying to prove an instance of this unless synthInstance.maxheartbeats were bumped. So I figured I'd try and add the instance myself. The general case felt like

instance (S R A B : Type*) [CommSemiring S]
    [CommSemiring R] [Algebra S R]
    [AddCommMonoid A] [Module R A] [Module S A] [IsScalarTower S R A]
    [AddCommMonoid B] [Module R B] [Module S B] [IsScalarTower S R B]
    (F : Type*) [FunLike F A B] [MulActionHomClass F R A B] : MulActionHomClass F S A B where
  map_smulₛₗ φ m a := by
    rw [← IsScalarTower.algebraMap_smul R, map_smul, IsScalarTower.algebraMap_smul, id_def]

which works fine as a def but Lean won't buy it as an instance, moaning that it can't find a good synthesization order. Well on the face of it this weems reasonable: when faced with a goal of MulActionHomClass F S A B Lean cannot really guess an R. So I figured that instead of working with a general LinearMapClass F I should just work with linear maps, and tried this:

instance (S R A B : Type*) [CommSemiring S]
    [CommSemiring R] [Algebra S R]
    [AddCommMonoid A] [Module R A] [Module S A] [IsScalarTower S R A]
    [AddCommMonoid B] [Module R B] [Module S B] [IsScalarTower S R B] :
    MulActionHomClass (A →ₗ[R] B) S A B where
  map_smulₛₗ φ m a := by
    rw [← IsScalarTower.algebraMap_smul R, map_smul, IsScalarTower.algebraMap_smul, id_def]

Again this compiles fine as a def but fails as an instance. This one I was more surprised by because surely all of the type information is in MulActionHomClass (A →ₗ[R] B) S A B this time? The error is

cannot find synthesization order for instance instMulActionHomClassLinearMapIdOfIsScalarTower_fLT with type
  ∀ (S : Type u_5) (R : Type u_6) (A : Type u_7) (B : Type u_8) [inst : CommSemiring S] [inst_1 : CommSemiring R]
    [inst_2 : Algebra S R] [inst_3 : AddCommMonoid A] [inst_4 : Module R A] [inst_5 : Module S A]
    [inst_6 : IsScalarTower S R A] [inst_7 : AddCommMonoid B] [inst_8 : Module R B] [inst_9 : Module S B]
    [inst_10 : IsScalarTower S R B], MulActionHomClass (A →ₗ[R] B) S A B
all remaining arguments have metavariables:
  CommSemiring ?S
  @Algebra ?S R ?inst✝ CommSemiring.toSemiring
  @Module ?S A CommSemiring.toSemiring inst✝⁷
  @IsScalarTower ?S R A Algebra.toSMul SMulZeroClass.toSMul SMulZeroClass.toSMul
  @Module ?S B CommSemiring.toSemiring inst✝³
  @IsScalarTower ?S R B Algebra.toSMul SMulZeroClass.toSMul SMulZeroClass.toSMul

And then I tried it with the specific case which was causing the slowdown in FLT:

instance : MulActionHomClass
    (L ⊗[K] adicCompletion K v →ₐ[L] (w : Extension B v) → adicCompletion L w.1) B
    (L ⊗[K] adicCompletion K v) ((w : Extension B v) → adicCompletion L w.1) where
  map_smulₛₗ φ b x := by
    rw [← IsScalarTower.algebraMap_smul L, map_smul,
      IsScalarTower.algebraMap_smul, id_def]

and it worked fine :-) So clearly I'm giving Lean enough clues with my convoluted special case. I am wondering what the big difference is between my convoluted special case and my attempt to make a general instance. The algebra version of the general also fails:

instance (S R A B : Type*) [CommSemiring S]
    [CommSemiring R] [Algebra S R]
    [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower S R A]
    [Semiring B] [Algebra R B] [Algebra S B] [IsScalarTower S R B] :
    MulActionHomClass (A →ₐ[R] B) S A B where
  map_smulₛₗ φ m a := by
    rw [← IsScalarTower.algebraMap_smul R, map_smul, IsScalarTower.algebraMap_smul, id_def]

[Edward van de Meent]

the issue is that other than the first argument, MulActionHomClasss arguments are outParams, meaning that since S does not occur in A →ₐ[R] B or A →ₗ[R] B, lean is unable to choose a value

[Edward van de Meent]

(i think)

[Edward van de Meent]

indeed, the first argument to MulActionHomClass in the instance from the FLT slowdown mentions all of L,K,v,B, so it does not complain

[Kevin Buzzard]

Yeah that sounds like a plausible explanation! Thanks!

[Antoine Chambert-Loir]

Oops, I feel responsible for this design of docs#MulActionHomClass, which was indeed borrowed from what existed for docs#LinearMapClass… Is there any suggestion to make?

[Antoine Chambert-Loir]

Slightly off-topic, I had resisted defining MulActionEquiv, on which docs#LinearEquiv and docs#AlgEquiv could build. Should I try?

[Edward van de Meent]

Antoine Chambert-Loir said:

Oops, I feel responsible for this design of docs#MulActionHomClass, which was indeed borrowed from what existed for docs#LinearMapClass… Is there any suggestion to make?

i don't think there's an issue with this design at all?

[Kevin Buzzard]

The design question is whether typeclass inference should be able to figure out that an R-linear map is S-linear, and you can see that in general this is a very risky idea because given a map which typeclass inference conjectures is S-linear for some S which is easily discoverable by looking at the context, using such an instance would now mean that typeclass inference has to try and prove it's R-linear but it doesn't know what R is, which sounds bad. I'm happy with the design -- I was just confused about why it was working in one case but not in another, and now I understand this (the key point is that in my case everything including R can be read from F, by coincidence).

[Yuyang Zhao]

I noticed some unification issues in the current design. E.g. MulActionSemiHomClass F ⇑f M N ≟ MulActionHomClass F R M N for f : R →+* R.

[Edward van de Meent]

that doesn't make sense? ⇑f is not a type?

[Edward van de Meent]

oh wait, nvm

[Edward van de Meent]

i missed the Semi in MulActionSemiHomClass F ⇑f M N

[Yuyang Zhao]

I experimented with a refactor that replaced docs#LinearMapClass with more basic typeclasses several months ago. It was completely blocked by unification issues like this.