Problem with instances of new class

Stream: new members

[Laurent Bartholdi]

I'm trying to declare a class that bundles numerous properties (a group, a topological space, an action, the fact that the space is T2 (Hausdorff), etc.); here is an oversimplified example of what I'm trying to do, and fail:

import Mathlib.GroupTheory.GroupAction.Basic

class GroupMulAction (G : Type _) (α : Type _) where
  group : Group G
  act : MulAction G α

instance [GroupMulAction G α] : Group G := GroupMulAction.group
instance [GroupMulAction G α] : MulAction G α := GroupMulAction.act

(the error messages are different for both instances: the first complains cannot find synthesization order for instance @instGroup with type, and the second says type mismatch GroupMulAction.act has type @MulAction G α (@DivInvMonoid.toMonoid G (@Group.toDivInvMonoid G (GroupMulAction.group α))) : Type (max ?u.2019 ?u.2018) but is expected to have type @MulAction G α (@DivInvMonoid.toMonoid G (@Group.toDivInvMonoid G instGroup)) : Type (max ?u.2019 ?u.2018))

By contrast, the following works like a charm:

class TestSpace (α : Type _) where
  isspace : TopologicalSpace α
  isT2 : T2Space α
  isNE : Nonempty α

instance [TestSpace α] : TopologicalSpace α := TestSpace.isspace
instance [TestSpace α] : T2Space α := TestSpace.isT2
instance [TestSpace α] : Nonempty α := TestSpace.isNE

I read https://leanprover.github.io/lean4/doc/typeclass.html which I found enlightening, but obviously not enough...

[Eric Wieser]

The short answer is that you can't combine typeclasses that take different numbers of types

[Eric Wieser]

Soo Foo A B can only ever extend / contain / imply Bar A B, not Baz A or Bar A A

[Patrick Massot]

Laurent, you can read Chapter 7 of #mil that contains a lengthy discussion of that error message.

[Kevin Buzzard]

You can see how docs#MulAction is defined (with Monoid \alpha "outside") -- can you do the same in your example, with the group structure etc all outside the class itself?

[Laurent Bartholdi]

:tada: I marked G as outParam and I can do almost everything I want (except infer "Group G"). My code now reads

import Mathlib.GroupTheory.GroupAction.Basic

class GroupMulAction (G : outParam (Type _)) (α : Type _) [Group G] where
  act : MulAction G α

instance [Group G] [GroupMulAction G α] : MulAction G α := GroupMulAction.act

[Adam Topaz]

There was a recent discussion about essentially the same problem kind of mathematics quite recently. Let me dig it up No, I was wrong. It was about something different

[Eric Wieser]

Using an outParam here is a bad idea, as it means "there will never be any type that acts on α other than G"