fun with data kinds

dataKinds.hs

{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}

import Prelude hiding (lookup)
import qualified Data.Map as Map

type family Equal a b :: Bool where
  Equal a a = 'True
  Equal a b = 'False

data Proxy k = Proxy deriving Show

foo :: Proxy 'True
foo = Proxy :: Proxy (Equal Int Int)
-- fails to compile: foo = Proxy :: Proxy Bool (Equal Int Char)

data N = Z | S N

type family Arity (f :: *) :: N where
  Arity (a -> b) = 'S (Arity b)
  Arity z = 'Z

eq1 :: Proxy 'True
eq1 = Proxy :: Proxy (Equal (Arity (a -> b -> c)) (Arity (a -> b -> c)))
-- FAILS: eq1 = Proxy :: Proxy (Equal (Arity (a -> b -> c)) (Arity (a -> b)))

data HList :: [*] -> * where
  HNil  :: HList '[]
  HCons :: a -> HList as -> HList (a ': as)

hnil :: HList '[]
hnil = HNil

infixr 1 `hcons`

hcons :: a -> HList as -> HList (a ': as)
hcons = HCons

foo1 :: HList '[Int]
foo1 = 3 `hcons` hnil

foo2 :: HList '[Int, Bool]
foo2 = 3 `hcons` True `hcons` hnil

main = do
  return ()