A no so successful attempt to implement a type-level hanoi, goal: http://www.blogjava.net/sean/archive/2009/11/23/303374.html

Hanoi.hs

{-# LANGUAGE TypeOperators  #-}
{-# LANGUAGE TypeFamilies   #-}
{-# LANGUAGE ScopedTypeVariables #-} -- for Show

data Zero
data Succ a

data from :-> to
data act1 :>> act2
infixr :>>

data Left
data Middle
data Right

type family Hanoi n from to tmp where
    Hanoi (Succ Zero) from to tmp = from :-> to
    Hanoi (Succ (Succ n)) from to tmp =
        Hanoi (Succ n) from tmp to
            :>> Hanoi (Succ Zero) from to tmp
            :>> Hanoi (Succ n) tmp to from

-- Example

proxy = undefined

type Three = Succ (Succ (Succ Zero))

x = proxy :: Hanoi Three Left Right Middle

-- Display

instance Show Left where
    show _ = "Left"
instance Show Middle where
    show _ = "Middle"
instance Show Right where
    show _ = "Right"

instance (Show from, Show to) => Show (from :-> to) where
    show _ = show (proxy::from) ++ " -> " ++ show (proxy::to)
instance (Show a, Show b) => Show  (a :>> b) where
    show _ = show (proxy::a) ++ "\n" ++ show (proxy::b)

HanoiFD.hs

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators  #-}
{-# LANGUAGE ScopedTypeVariables #-}

data Zero
data Succ a

data Left
data Middle
data Right

data from :-> to
data act1 :>> act2
infixr :>>

class Hanoi n from to tmp action | n from to tmp -> action where
    result :: n -> from -> to -> tmp -> action

instance Hanoi (Succ Zero) from to tmp (from :-> to)
instance ( Hanoi (Succ n) from tmp to act1
         , Hanoi (Succ Zero) from to tmp act2
         , Hanoi (Succ n) tmp to from act3
         )
    => Hanoi (Succ (Succ n)) from to tmp (act1 :>> act2 :>> act3)

-- Example
proxy = undefined

type Three = Succ (Succ (Succ Zero))
x = result (proxy::Three) (proxy::Left) (proxy::Right) (proxy::Middle)

-- Display

instance Show Left where
    show _ = "Left"
instance Show Middle where
    show _ = "Middle"
instance Show Right where
    show _ = "Right"

instance (Show from, Show to) => Show (from :-> to) where
    show _ = show (proxy::from) ++ " -> " ++ show (proxy::to)
instance (Show a, Show b) => Show  (a :>> b) where
    show _ = show (proxy::a) ++ "\n" ++ show (proxy::b)

HanoiTypeLit.hs

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-} -- for Show
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-} -- evil?

import GHC.TypeLits

data from :-> to
data act1 :>> act2
infixr :>>

data Left
data Middle
data Right

type family Hanoi (n::Nat) from to tmp where
    Hanoi 1 from to tmp = from :-> to
    Hanoi n from to tmp =
        Hanoi (n - 1) from tmp to
        :>> Hanoi 1 from to tmp
        :>> Hanoi (n - 1) tmp to from