instances for `Rep R G`

Stream: maths

[Richard Hill]

I'm confused about the following code:

import Mathlib

variable {R : Type} [CommRing R]
variable {G : Type} [Group G]
open Rep

instance myInstance (A B : Rep R G) : MulActionHomClass (Action.HomSubtype _ _ A B)
    R A B where
  map_smulₛₗ f := map_smul f.val


instance (A : Rep R G) : MulActionHomClass (Action.HomSubtype _ _ A (leftRegular R G))
    R A (leftRegular R G) :=
  myInstance _ _

why is the second instance needed, since it seems to be just a special case of the first ?

[Aaron Liu]

Where is this code coming from?

[Richard Hill]

it's my code. I just don't know why I need the second instance which looks like a hack.
The same thing happens with AddMonoidHomClass.

[Aaron Liu]

#discr_tree_key for myInstance reveals

MulActionSemiHomClass
  (@Subtype (@LinearMap _ _ _ _ (RingHom.id _ _) _.1.1 _.1.1 _ _ _ _) <other>)
  _
  _
  (@id _)
  _.1.1
  _.1.1
  _
  _
  _

and for the other instance it is

MulActionSemiHomClass
  (@Subtype (@LinearMap _ _ _ _ (RingHom.id _ _) _.1.1 (Finsupp _ _ _) _ _ _ _) <other>)
  _
  _
  (@id _)
  _.1.1
  (Finsupp _ _ _)
  _
  _
  _

[Aaron Liu]

So presumably _.1.1 didn't match Finsupp _ _ _

[Richard Hill]

Thanks. So I guess I'll get the same problem with any representation made in the same way as leftRegular R G.
This would include things constructed as ofMulAction R G H.

Is there any way I can make the first instance more general to cover these cases?

[Matthew Ballard]

Abstraction boundaries seem to have completely collapsed here…