First class checkable laws using the free-functors package

laws.hs

{-# LANGUAGE 
    TypeFamilies
  , KindSignatures
  , ScopedTypeVariables
  , ConstraintKinds
  , FlexibleInstances
  , FlexibleContexts
  , DeriveGeneric
  , DeriveAnyClass
  , TypeApplications
  , AllowAmbiguousTypes
  #-}

import GHC.Types (Constraint)
import GHC.Generics (Generic)
import Data.Functor.Free
import Test.QuickCheck

import Data.Monoid (Sum)

data EQ a = a :=: a deriving (Eq, Show)
infix 4 :=:

class Laws (c :: * -> Constraint) where
  type Var c :: *
  laws :: [EQ (Free c (Var c))]

data VAR = X | Y | Z deriving (Eq, Show, Generic, CoArbitrary)

instance Show a => Show (VAR -> a) where
  show f = unlines $ map show [(X, f X), (Y, f Y), (Z, f Z)]
  
x, y, z :: Free c VAR
x = unit X
y = unit Y
z = unit Z

instance Laws Semigroup where
  type Var Semigroup = VAR
  laws = [x <> (y <> z) :=: (x <> y) <> z]
  
instance Laws Monoid where
  type Var Monoid = VAR
  laws = 
    [ x <> mempty :=: x
    , mempty <> x :=: x
    ]
    
props :: forall c a. (Laws c, c a, Eq a) => (Var c -> a) -> Bool
props f = and $ (\(l :=: r) -> rightAdjunct f l == rightAdjunct f r) <$> laws @c

checkLaws :: forall c a. (Laws c, c a, CoArbitrary (Var c), Arbitrary a, Eq a, Show (Var c -> a)) => IO ()
checkLaws = quickCheck (props @c @a)

main :: IO ()
main = checkLaws @Semigroup @(Sum Double)