Combine inductive typeclasses

Question

I have a permutation types with has a fixed sizes. Now permutations form a group so I would like to make them an instance of a Group class. Semigroup is easy enough:

instance
  ( Integral i
  )
    => Semigroup (Permutation n i)
  where
    (<>) = ...

However when I get to Monoid I'm a bit stuck. I can't seem to make mempty polymorphic on n. For (<>) the type information of the size of the output was provided as a part of the input, but for mempty there is no input.

What I can do is define the class in terms of induction.

instance
  ( Integral i
  )
    => Monoid (Permutation Zr i)
  where
    mempty = ...

instance
  ( Integral i
  , Monoid (Permutation n i)
  )
    => Monoid (Permutation (Nx n) i)
  where
    mempty = ...

But this is not quite the same. For example if I do the following with Semigroup:

test ::
  ( Integral i
  )
    => Permutation n i -> Permutation n i -> Permutation n i
test =
  (<>)

It compiles just fine, but if I do the following with Monoid:

test ::
  ( Integral i
  )
    => Permutation n i
test =
  mempty

    • Could not deduce (Monoid (Permutation n i))
        arising from a use of ‘mempty’
      from the context: Integral i
        bound by the type signature for:
                   test :: forall i n. Integral i => Permutation n i
    • In the expression: mempty
      In an equation for ‘test’: test = mempty
    |
123 |   mempty
    |   ^^^^^^

Because we cannot infer that Permutation n i is always a Monoid. Even more troublesome is that if I try and take my Monoid instance and make a Group instance, I need to split that in two as well, since Group (Permutation n i) would require Monoid (Permutation n i) which cannot be inferred.

This is less than desirable. I would like to just have 1 instance for Monoid and Group, just like I have for Semigroup.

Is there some way to define a single complete monoid instance? It seems like there might be I just can't think of it.

---

The definition of permutation is just a wrapper around a type level vector:

newtype Permutation n a =
  Perm (Vector n a)

data Vector n a where
  EmptyVec :: Vector Zr a
  (:++) :: a -> Vector n a -> Vector (Nx n) a

But really I'm interested in a general mechanism that would allow me to make a polymorphic object.