Weird.hs

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

type family Head x where
  Head (x ': xs) = x


type family Append (x::[*]) (y :: *) :: [*] where
  Append '[] x = '[x]
  Append (x ': xs) y = x ': Append xs y

type family Roll (x::[*]) where
  Roll (x ': xs) = Append xs x

data Q (xs::[*]) q where
  N :: Q xs q
  (:-) :: (CHeadT q xs ~ t, CTailT q xs ~ z) => t -> Q z q -> Q xs q

class CHead q where
  type CHeadT q (xs::[*]) :: *

class CTail q where
  type CTailT q (xs :: [*]) :: [*]

data Cycle
instance CHead Cycle where
  type CHeadT Cycle xs = Head xs
instance CTail Cycle where
  type CTailT Cycle xs = Roll xs

test1 :: Q '[] Cycle
test1 = N
test2,test3,test4 :: Q '[Int] Cycle
test2 = N
test3 = 1 :- N
test4 = 1 :- (2 :- N)
test5,test6,test7,test8 :: Q [Int, String] Cycle
test5 = N
test6 = 1 :- N
test7 = 1 :- ("foo" :- N)
test8 = 1 :- ("foo" :- (3 :- N))

data Cnt
instance CHead Cnt where
  type CHeadT Cnt (x ': y) = x
instance CTail Cnt where
  type CTailT Cnt xs =xs

test9 :: Q '[Int, String] Cnt
test9 = 1 :- (2 :- N)