Question1.hs

{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}


module Data.HyperRelation.Internal.Question1 where
import           Data.Functor.Classes
import           Data.Functor.Identity
import           GHC.Exts              (Constraint)


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 Forall Eq as => 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

type family Foralla (f :: k -> Constraint) (xs :: [k]) :: Constraint where
  Foralla f '[] = ()
  Foralla f (x ': xs) = (f x, Foralla f xs)

class Foralla f xs => Forall f xs
instance Foralla f xs => Forall f xs

-- The error I get is:

-- src/Data/HyperRelation/Internal/Question1.hs:38: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:37:8-71
--     In the expression: r1 == r2
--     In an equation for ‘foo’: foo r1 r2 = r1 == r2
-- Compilation failed.