{-
This code shows how to check if a type-level list contains a given type.
It first shows the approach required for older versions of GHC (< 7.6.x)
and then a version using closed type families supported in GHC 7.8.1 and greater.
-}

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

-- The data structure used the for the examples below.

-- elements of a type level list
data A a
data B a
data C a
data D a
data E a
data F a

-- an example of a heterogenous list
type TypeLevelList = (A (B (C (D (E ())))))

-- Everything from here to the closing comment "Old way ends here"
-- shows the old way.

-- First we need to test for equality at the type level
-- so we can test if some type is what we are looking for.
data Yes
data No
class TypeEqual x y b | x y -> b
instance {-# OVERLAPPING #-} TypeEqual a a Yes
instance {-# OVERLAPPABLE #-} No ~ b => TypeEqual x y b

-- a runner that tests that the type passed in matches
-- (A ())
runTypeEqual :: (TypeEqual a (A ()) Yes) => a -> IO ()
runTypeEqual _ = print "ran!"

{-
> runTypeEqual (undefined :: (A ()))
"ran!"
> runTypeEqual (undefined :: (B ()))
<interactive>:35:1:
    Couldn't match type ‘No’ with ‘Yes’
    In the expression: runTypeEqual (undefined :: B ())
    In an equation for ‘it’: it = runTypeEqual (undefined :: B ())
-}

-- In order ot get to the next element of the list we need to
-- pop its head.
class Tail aas as | aas -> as
instance Tail (a as) as
instance (r ~ ()) => Tail () r

-- a runner that returns the tail of a type-level list
runTail :: (Tail aas as) => aas -> as -> IO ()
runTail _ _ = print "ran!"

{-
> :t runTail (undefined :: (A (B (C (D ())))))
runTail (undefined :: (A (B (C (D ()))))) :: B (C (D ())) -> IO ()
-}

-- Now we can check if the type is in the list
class Contains' a b match r | a b match -> r
instance (Tail aas as, Contains as b r) => Contains' aas b No r
instance (r ~ Yes) => Contains' a b Yes r

class Contains as a r | as a -> r
instance (TypeEqual (a ()) b match, Contains' (a as) b match r) => Contains (a as) b r
instance Contains () b No

-- A runner that checks if the type of the argument is one of (A (B (C (D (E ())))))
runContains :: (Contains (A (B (C (D (E ()))))) a Yes) => a -> IO ()
runContains _ = print "ran!"

{-
> runContains (undefined :: B ())
"ran!"

> runContains (undefined :: F ())
<interactive>:38:1:
    Couldn't match type ‘No’ with ‘Yes’
    arising from a functional dependency between:
      constraint ‘Contains () (F ()) Yes’
        arising from a use of ‘runContains’
      instance ‘Contains () b No’
        at /home/deech/Haskell/TypeLevelLiterals/TypeFamily.hs:59:10-25
    In the expression: runContains (undefined :: F ())
    In an equation for ‘it’: it = runContains (undefined :: F ())
-}

-- Old way ends here

-- The new way with closed type families

type family ClosedContains haystack (needle :: *) where
  ClosedContains (x xs) (x ()) = Yes
  ClosedContains () (x ()) = No
  ClosedContains (x xs) (y ()) = ClosedContains xs (y ())

-- a runner that test for type-level list membership just like 'runContains'.
runClosedContains :: (Yes ~ ClosedContains (A (B (C (D (E ()))))) a) => a -> IO ()
runClosedContains _ = print "ran!"

{-
runClosedContains (undefined :: (A ()))
"ran!"
*Main> runClosedContains (undefined :: (F ()))
<interactive>:53:1:
    Couldn't match type ‘No’ with ‘Yes’
    Expected type: ClosedContains (A (B (C (D (E ()))))) (F ())
      Actual type: Yes
    In the expression: runClosedContains (undefined :: F ())
    In an equation for ‘it’: it = runClosedContains (undefined :: F ())
-}