cannot find synthesization order for instance

Stream: mathlib4

[Yury G. Kudryashov]

In #5662, Lean doesn't accept the definition of class ModularFormClass with the following error message:

cannot find synthesization order for instance @ModularFormClass.toSlashInvariantFormClass with type
  {F : Type u_1} → {Γ : Subgroup SL(2, ℤ)} → {k : ℤ} → [self : ModularFormClass F Γ k] → SlashInvariantFormClass F Γ k
all remaining arguments have metavariables:
  ModularFormClass F ?Γ ?k

Here is an #mwe:

import Mathlib.NumberTheory.ModularForms.SlashInvariantForms
import Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

open Complex UpperHalfPlane

open scoped Topology Manifold UpperHalfPlane

local notation "SL(" n ", " R ")" => Matrix.SpecialLinearGroup (Fin n) R

class ModularFormClass (F : Type _) (Γ : Subgroup SL(2, ℤ)) (k : ℤ)
  extends SlashInvariantFormClass F Γ k where

[Yury G. Kudryashov]

Ah, adding outParams helps.

[Denis Gorbachev]

For those coming from search: you can find a minimal example with solution here: https://github.com/DenisGorbachev/lean-error-resolutions/blob/main/errors/cannot-find-synthesization-order.md