avigad
7.1: Module `extends` example that's supposed to fail doesn't
From the text:
class Module₁ (R : Type) [Ring₃ R] (M : Type) [AddCommGroup₃ M] extends SMul₃ R M where
...
There is something interesting going on here. While it isn’t too surprising that the ring structure on R is a parameter in this definition, you probably expected AddCommGroup₃ M to be part of the extends clause just as SMul₃ R M is. Trying to do that would lead to a mysterious sounding error message: cannot find synthesization order for instance Module₁.toAddCommGroup₃ with type (R : Type) → [inst : Ring₃ R] ...
Changing the definition above to:
class Module₁ (R : Type) [Ring₃ R] (M : Type) extends SMul₃ R M, AddCommGroup₃ M where
causes no issues for me locally, so it's unclear to me if this example is no longer valid in newer versions, or if I'm misunderstanding.
(Somewhat related to #185, both are in 7.1 and it's not clear what the "broken example" we are trying to avoid is.)
