Question1.hs

{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE KindSignatures    #-}
{-# LANGUAGE TypeOperators     #-}

module Data.HyperRelation.Internal.Question1 where
import Data.Functor.Identity

data Relation :: (* -> *) -> [*] -> * where
  EndR    :: Relation f '[]
  (:<->:) :: f a -> Relation f as -> Relation f (a ': as)

infixr 4 :<->:
instance Eq (Relation f '[]) where
  EndR == EndR = True
instance (Eq (f a), Eq (Relation f as)) => Eq (Relation f (a ': as)) where
  (a :<->: as) == (b :<->: bs) = a == b && as == bs

class HRC (as :: [*]) where
  -- omitted
instance HRC '[] where
  -- omitted
instance (Eq a, HRC as) => HRC (a ': as) where
  -- omitted

foo :: (HRC as) => Relation Identity as -> Relation Identity as -> Bool
foo r1 r2 = r1 == r2

-- The error I get is:

-- src/Data/HyperRelation/Internal/Question1.hs:30:16: Could not deduce (Eq (Relation Identity as)) …
--       arising from a use of ‘==’
--     from the context (HRC as)
--       bound by the type signature for
--                  foo :: HRC as =>
--                         Relation Identity as -> Relation Identity as -> Bool
--       at /home/carlo/code/haskell/hyper-relation/src/Data/HyperRelation/Internal/Question1.hs:29:8-71
--     In the expression: r1 == r2
--     In an equation for ‘foo’: foo r1 r2 = r1 == r2
-- Compilation failed.

-- Why is this?