MIL Ch7 - extends no longer limited

Stream: new members

[Rado Kirov]

I am working through MIL Ch07 S01 and reading about the definition of Modules. They are defined as

class Module₁ (R : Type) [Ring₃ R] (M : Type) [AddCommGroup₃ M] extends SMul₃ R M

and there is an explanation why

class Module₁ (R : Type) [Ring₃ R] (M : Type) extends SMul₃ R M, AddCommGroup₃ M

should fail. But that appears no longer to be true (at least in my experiment the second one works just fine).

The reason given is that during toAddCommGroup generation

it would need to go hunting for a completely unspecified type R and a Ring₃ R instance
but since the type of toAddCommGroup is

(R : Type) → {inst : Ring₃ R} → {M : Type} → [self : Module₁ R M] → AddCommGroup₃ M

It feels to me that R is specified as an parameter and not completely unspecified. Maybe that was fixed and now things just work?

Should I ignore this rule

The rule is easy to remember: each class appearing in the extends clause should mention every type appearing in the parameters.

if extends appears to work now?