Defining a Typeclass with Multiple Type Parameters

Stream: new members

[Nick Attkiss]

In the Mathematics in Lean tutorial, the following is given as a definition of a module:

class Module₁ (R : Type) [Ring₃ R] (M : Type) [AddCommGroup₃ M] extends SMul₃ R M where
  zero_smul : ∀ m : M, (0 : R) • m = 0
  one_smul : ∀ m : M, (1 : R) • m = m
  mul_smul : ∀ (a b : R) (m : M), (a * b) • m = a • b • m
  add_smul : ∀ (a b : R) (m : M), (a + b) • m = a • m + b • m
  smul_add : ∀ (a : R) (m n : M), a • (m + n) = a • m + a • n

Here the ring structure on R and the abelian group structure on M are given as arguments, which aligns with a plain-English definition for module like "Let R be a ring and M be an abelian group. Then M is an R-module if there is a scalar multiplication such that..."

But what if I want to define a module analogously to a definition like "Let R and M be sets. A module structure on (R,M) is the following: a ring structure on R, an abelian group structure on M, and a scalar multiplication such that..."? I would naively think to write the class definition like this:

class Module₂ (R : Type) (M : Type)  extends  Ring₃ R,  AddCommGroup₃ M,  SMul₃ R M where
  zero_smul : ∀ m : M, (0 : R) • m = 0
  one_smul : ∀ m : M, (1 : R) • m = m
  mul_smul : ∀ (a b : R) (m : M), (a * b) • m = a • b • m
  add_smul : ∀ (a b : R) (m : M), (a + b) • m = a • m + b • m
  smul_add : ∀ (a : R) (m n : M), a • (m + n) = a • m + a • n

This throws an error and I'm not sure why. After all, the following manual example does work (albeit without any type class inference magic), and it's what I'm trying to create with Module₂:

class Module₃ (R : Type) (M : Type) where
  toRing₃ : Ring₃ R
  toAddCommGroup₃ : AddCommGroup₃ M
  toSMul₃ : SMul₃ R M
  zero_smul : ∀ m : M, (0 : R) • m = 0
  one_smul : ∀ m : M, (1 : R) • m = m
  mul_smul : ∀ (a b : R) (m : M), (a * b) • m = a • b • m
  add_smul : ∀ (a b : R) (m : M), (a + b) • m = a • m + b • m
  smul_add : ∀ (a : R) (m n : M), a • (m + n) = a • m + a • n

I can't seem to get my head around the problem with Module₂. What's going on?

[Eric Wieser]

Module₂ is Module₃ combined with attribute [instance] Module₃.toRing₃ etc

[Eric Wieser]

It's this second step that fails; I think mathematics in lean explains the issue here?

[Nick Attkiss]

@Eric Wieser Yep, definitely should've read the next paragraph! To clarify, the error thrown by the improper extends or improper attribute [instance] doesn't mean that Lean had trouble with a type class instance resolution in that line, but rather that Lean is smart enough to know that the created instance will lead to trouble down the road?