Monoid typeclass with compiler-enforced laws in Haskell

LawfulMonoid.hs

{-# LANGUAGE AllowAmbiguousTypes       #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE LambdaCase                #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TemplateHaskell           #-}
{-# LANGUAGE TypeApplications          #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeInType                #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}

import           Data.Kind
import           Data.Singletons
import           Data.Singletons.TH
import           Data.Singletons.Prelude
import           Data.Type.Equality
import           Prelude hiding          (Monoid(..))

class Monoid (m :: Type) where
    type Mempty  m :: m
    type Mappend m (x :: m) (y :: m) :: m

    sMempty  :: Sing (Mempty m)
    sMappend
        :: forall (x :: m) (y :: m). ()
        => Sing x
        -> Sing y
        -> Sing (Mappend m x y)

    -- the laws
    memptyIdentLeft
        :: forall (x :: m). ()
        => Sing x
        -> Mappend m x (Mempty m) :~: x

    memptyIdentRight
        :: forall (x :: m). ()
        => Sing x
        -> Mappend m (Mempty m) x :~: x

    mappendAssoc
        :: forall (x :: m) (y :: m) (z :: m). ()
        => Sing x
        -> Sing y
        -> Sing z
        -> Mappend m (Mappend m x y) z :~: Mappend m x (Mappend m y z)

-- mempty and mappend to recover the original Monoid

mempty
    :: forall m. (SingKind m, Monoid m)
    => DemoteRep m
mempty = fromSing (sMempty @m)

mappend
    :: forall m. (SingKind m, Monoid m)
    => DemoteRep m -> DemoteRep m -> DemoteRep m
mappend x y = withSomeSing x $ \sx ->
              withSomeSing y $ \sy ->
                fromSing $ sMappend @m sx sy

$(singletons [d|
  data N = Z | S N
    deriving Show
  |])

instance Monoid N where
    type Mempty  N = Z
    type Mappend N Z     y = y
    type Mappend N (S x) y = S (Mappend N x y)

    sMempty  = SZ
    sMappend x y = case x of
      SZ    -> y
      SS x' -> SS (sMappend x' y)

    memptyIdentLeft = \case
      SZ   -> Refl
      SS x -> memptyIdentLeft x `gcastWith` Refl

    memptyIdentRight _ = Refl

    mappendAssoc = \case
      SZ   -> \_ _ -> Refl
      SS x -> \y z ->
        mappendAssoc x y z `gcastWith` Refl

instance Monoid [a] where
    type Mempty  [a] = '[]
    type Mappend [a] '[]       ys = ys
    type Mappend [a] (x ': xs) ys = x ': Mappend [a] xs ys

    sMempty  = SNil
    sMappend xs ys = case xs of
      SNil          -> ys
      x `SCons` xs' -> x `SCons` sMappend xs' ys

    memptyIdentLeft = \case
      SNil         -> Refl
      _ `SCons` xs -> memptyIdentLeft xs `gcastWith` Refl

    memptyIdentRight _ = Refl

    mappendAssoc = \case
      SNil         -> \_ _   -> Refl
      _ `SCons` xs -> \ys zs ->
        mappendAssoc xs ys zs `gcastWith` Refl

main :: IO ()
main = do
    let x :: N
        x = S (S Z)
        y :: N
        y = S (S (S (S (S Z))))
    print x
    print y
    print $ mappend @N x y