I'm generalizing this n-ary complement to an n-ary compose, but I'm having trouble making the interface nice. Namely, I can't figure out how to use numeric literals at the type level while still being able to pattern match on successors.

Rolling my own nats

Using roll-my-own nats, I can make n-ary compose work, but I can only pass n as an iterated successor, not as a literal:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

module RollMyOwnNats where

import Data.List (genericIndex)

-- import Data.Proxy
data Proxy (n::Nat) = Proxy

----------------------------------------------------------------
-- Stuff that works.

data Nat = Z | S Nat

class Compose (n::Nat) b b' t t' where
  compose :: Proxy n -> (b -> b') -> t -> t'

instance Compose Z b b' b b' where
  compose _ f x = f x

instance Compose n b b' t t' => Compose (S n) b b' (a -> t) (a -> t') where
  compose _ g f x = compose (Proxy::Proxy n) g (f x)

-- Complement a binary relation.
compBinRel :: (a -> a -> Bool) -> (a -> a -> Bool)
compBinRel = compose (Proxy::Proxy (S (S Z))) not

----------------------------------------------------------------
-- Stuff that does not work.

instance Num Nat where
  fromInteger n = iterate S Z `genericIndex` n
-- I now have 'Nat' literals:
myTwo :: Nat
myTwo = 2
-- But GHC thinks my type-level nat literal is a 'GHC.TypeLits.Nat',
-- even when I say otherwise:
compBinRel' :: (a -> a -> Bool) -> (a -> a -> Bool)
compBinRel' = compose (Proxy::Proxy (2::Nat)) not
{-
    Kind mis-match
    An enclosing kind signature specified kind `Nat',
    but `2' has kind `GHC.TypeLits.Nat'
    In an expression type signature: Proxy (2 :: Nat)
    In the first argument of `compose', namely
      `(Proxy :: Proxy (2 :: Nat))'
    In the expression: compose (Proxy :: Proxy (2 :: Nat)) not
-}

Using GHC.TypeLits.Nat

Using GHC.TypeLits.Nat, I get type-level nat literals, but there is no successor constructor that I can find, and using the type function (1 +) doesn't work, because GHC (7.6.3) can't reason about injectivity of type functions:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module UseGHCTypeLitsNats where

import GHC.TypeLits

-- import Data.Proxy
data Proxy (t::Nat) = Proxy

----------------------------------------------------------------
-- Stuff that works.

class Compose (n::Nat) b b' t t' where
  compose :: Proxy n -> (b -> b') -> t -> t'

instance Compose 0 b b' b b' where
  compose _ f x = f x

instance (Compose n b b' t t' , sn ~ (1 + n)) => Compose sn b b' (a -> t) (a -> t') where
  compose _ g f x = compose (Proxy::Proxy n) g (f x)

----------------------------------------------------------------
-- Stuff that does not work.

-- Complement a binary relation.
compBinRel , compBinRel' :: (a -> a -> Bool) -> (a -> a -> Bool)
compBinRel = compose (Proxy::Proxy 2) not
{-
    Couldn't match type `1 + (1 + n)' with `2'
    The type variable `n' is ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    In the expression: compose (Proxy :: Proxy 2) not
    In an equation for `compBinRel':
        compBinRel = compose (Proxy :: Proxy 2) not
-}
{-
    No instance for (Compose n Bool Bool Bool Bool)
      arising from a use of `compose'
    The type variable `n' is ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    Note: there is a potential instance available:
      instance Compose 0 b b' b b'
-}
compBinRel' = compose (Proxy::Proxy (1+(1+0))) not
{-
    Couldn't match type `1 + (1 + 0)' with `1 + (1 + n)'
    NB: `+' is a type function, and may not be injective
    The type variable `n' is ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    Expected type: Proxy (1 + (1 + 0))
      Actual type: Proxy (1 + (1 + n))
    In the first argument of `compose', namely
      `(Proxy :: Proxy (1 + (1 + 0)))'
-}

I agree that semantic editor combinators are more elegant and more general here -- and concretely, it will always be easy enough to write (.) . (.) . ... (n times) instead of compose (Proxy::Proxy n) -- but I'm frustrated that I can't make the n-ary composition work as well as I expected. Also, it seems I would run into similar problems for other uses of GHC.TypeLits.Nat, e.g. when trying to define a type function:

type family   T (n::Nat) :: *
type instance T 0     = ...
type instance T (S n) = ...

UPDATE: Summary and adaptation of the accepted answer

There's a lot of interesting stuff going on in the accepted answer, but the key for me is the Template Haskell trick in the GHC 7.6 solution: that effectively lets me add type-level literals to my GHC 7.6.3 version, which already had injective successors.

Using my types above, I define literals via TH:

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DataKinds #-}

module RollMyOwnLiterals where

import Language.Haskell.TH

data Nat = Z | S Nat

nat :: Integer -> Q Type
nat 0 = [t| Z |]
nat n = [t| S $(nat (n-1)) |]

where I've moved my Nat declaration into the new module to avoid an import loop. I then modify my RollMyOwnNats module:

+import RollMyOwnLiterals
...
-data Nat = Z | S Nat
...
+compBinRel'' :: (a -> a -> Bool) -> (a -> a -> Bool)
+compBinRel'' = compose (Proxy::Proxy $(nat 2)) not