!4#4228 cannot find synthesization order for instance

Stream: mathlib4

[Xavier Roblot]

A local instance

attribute [local instance] GradedModule.isModule

fails in this file with the error:

cannot find synthesization order for instance @isModule with type
  {ι : Type u_1} →
    {A : Type u_2} →
      {M : Type u_3} →
        {σ : Type u_4} →
          {σ' : Type u_5} →
            [inst : AddMonoid ι] →
              [inst_1 : Semiring A] →
                (𝓐 : ι → σ') →
                  [inst_2 : SetLike σ' A] →
                    (𝓜 : ι → σ) →
                      [inst_3 : AddCommMonoid M] →
                        [inst_4 : Module A M] →
                          [inst_5 : SetLike σ M] →
                            [inst_6 : AddSubmonoidClass σ' A] →
                              [inst_7 : AddSubmonoidClass σ M] →
                                [inst_8 : SetLike.GradedMonoid 𝓐] →
                                  [inst_9 : SetLike.GradedSmul 𝓐 𝓜] →
                                    [inst_10 : DecidableEq ι] →
                                      [inst : GradedRing 𝓐] → Module A (DirectSum ι fun i ↦ { x // x ∈ 𝓜 i })
all remaining arguments have metavariables:
  SetLike ?σ' A
  @AddSubmonoidClass ?σ' A AddMonoid.toAddZeroClass ?inst✝
  @SetLike.GradedMonoid ι A ?σ' ?inst✝ MonoidWithZero.toMonoid inst✝¹¹ ?𝓐
  @SetLike.GradedSmul ι ?σ' A σ M ?inst✝ inst✝⁶ SMulZeroClass.toSMul AddZeroClass.toAdd ?𝓐 𝓜
  @GradedRing ι A ?σ' (fun a b ↦ inst✝¹ a b) inst✝¹¹ inst✝¹⁰ ?inst✝ ?inst✝¹ ?𝓐

with

def isModule [DecidableEq ι] [GradedRing 𝓐] : Module A (⨁ i, 𝓜 i) :=
{ Module.compHom _ (DirectSum.decomposeRingEquiv 𝓐 : A ≃+* ⨁ i, 𝓐 i).toRingHom with
  smul := fun a b => DirectSum.decompose 𝓐 a • b }

Note that this definition takes a long time to elaborate (maxHeartbeats set to 300000).

[Kevin Buzzard]

Note what looks to me to be a related question here. The key part of error says

all remaining arguments have metavariables:
  SetLike ?σ' A
  @AddSubmonoidClass ?σ' A AddMonoid.toAddZeroClass ?inst✝
  @SetLike.GradedMonoid ι A ?σ' ?inst✝ MonoidWithZero.toMonoid inst✝¹¹ ?𝓐
  @SetLike.GradedSmul ι ?σ' A σ M ?inst✝ inst✝⁶ SMulZeroClass.toSMul AddZeroClass.toAdd ?𝓐 𝓜
  @GradedRing ι A ?σ' (fun a b ↦ inst✝¹ a b) inst✝¹¹ inst✝¹⁰ ?inst✝ ?inst✝¹ ?𝓐

This is the situation that typeclass inference finds itself in. It hasn't figured out how what type you actually want σ' to be. This is funny because you can read σ' off from the type of the first explicit input, but I have no idea in what order things happen when the system is doing all this unification and typeclass inference stuff. And what it's really trying to put off is using typeclass inference on any of the above goals, because it might end up in a loop or searching in a very large tree for something that isn't there.

[Kevin Buzzard]

Oh there are two similar errors: the second one has shorter output.

  @SetLike.GradedMonoid ι A σ' inst✝⁹ MonoidWithZero.toMonoid inst✝¹¹ ?𝓐
  @SetLike.GradedSmul ι σ' A σ M inst✝⁹ inst✝⁶ SMulZeroClass.toSMul AddZeroClass.toAdd ?𝓐 𝓜
  @GradedRing ι A σ' (fun a b ↦ inst✝¹ a b) inst✝¹¹ inst✝¹⁰ inst✝⁹ inst✝⁵ ?𝓐

So this indicates that the system doesn't know what 𝓐 is but now needs to know that whatever it is, it's a graded ring, and that will make typeclass inference go on a wild goose chase.

[Kevin Buzzard]

I think this translates down to the following statement:

def is_module [decidable_eq ι] [graded_ring 𝓐] :
  module A (⨁ i, 𝓜 i) :=

If typeclass inference gets its hands on this declaration then it realises that it will have to figure out what 𝓐 is in order to check it's a graded ring, but it has no hope. Hopefully the experts will fix which parts of the explanation I mangled.

[Kevin Buzzard]

It might have just been an unnoticed dangerous instance in Lean 3

[Kevin Buzzard]

Yeah the Lean 3 linter has the following to say about that instance:

/- The `dangerous_instance` linter reports: -/
/- DANGEROUS INSTANCES FOUND.
These instances are recursive, and create a new type-class problem which will have metavariables.
Possible solution: remove the instance attribute or make it a local instance instead.

Currently this linter does not check whether the metavariables only occur in arguments marked with `out_param`, in which case this linter gives a false positive. -/
#check @graded_module.is_module /- The following arguments become metavariables. argument 5: {σ' : Type u_6}, argument 8: (𝓐 : ι → σ') -/

[Kevin Buzzard]

Bottom line though is that I don't know how to fix it.

[Gabriel Ebner]

Yes, Lean complains because it can't reliably figure out the 𝓐. I would just put in a letI := GradedModule.isModule 𝓐 𝓜.

[Gabriel Ebner]

If one of the type class assumptions reliably determines the 𝓐, you could mark that argument of that type class as outparam. But I think there is more than one choice for the scalar multiplication usually.