Using Haskell's type system to specify that a class obeys extra properties (i.e. type classes for type classes)

Question

When we create a type class, we usually assume that its functions must obey some properties. Thus we have the Monoid and Monad laws for their respective type classes. But, what if there is some law, like associativity, that I want to specify that multiple classes either may or may not obey that law? Is there a way to do that in Haskell's type system? Is this sort of type classes for type classes idea even feasible in practice?

---

Here's a motivating example from algebra:

class Addition x where
    add :: x -> x -> x

class Multiplication x where
    mult :: x -> x -> x

instance Addition Int where
    add = (+)

instance Multiplication Int where
    add = (*)

Now, if I want to specify that addition over Int's is associative and commutative, I can create the classes and instances:

class (Addition x) => AssociativeAddition x where
class (Addition x) => CommutativeAddition x where

instance AssociativeAddition Int where
instance CommutativeAddition Int where

But this is cumbersome because I have to create all possible combinations for all classes. I can't just create Associative and Commutative classes, because what if addition is commutative, but multiplication is not (like in matrices)?

What I would like to be able to do is say something like:

class Associative x where

instance (Associative Addition, Commutative Addition) => Addition Int where
    add = (+)

instance (Commutative Multiplication) => Multiplication Int where
    mult = (*)

Can this be done?

(Haskell's abstract algebra packages, like algebra and constructive-algebra, do not currently do this, so I'm guessing not. But why not?)

Answer 1

You actually can do this with some recent GHC extensions:

{-# LANGUAGE ConstraintKinds, KindSignatures, MultiParamTypeClasses #-}
import GHC.Exts (Constraint)

class Addition (a :: *) where
    plus :: a -> a -> a

instance Addition Integer where
    plus = (+)

class (c a) => Commutative (a :: *) (c :: * -> Constraint) where
    op :: a -> a -> a

instance Commutative Integer Addition where
    op = plus