{-# LANGUAGE GADTs, EmptyDataDecls, RankNTypes #-}
-- {-# OPTIONS_GHC -F -pgmF she #-}
data Z
data S n

-- only works on ghc6 but not on ghc7
type Const a b = a

{-
data List a n where
  Nil :: List a Z
  Cons :: a -> List a n -> List a (S n)
-}

data L a l n where
  N :: L a l Z
  C :: a -> l n -> L a l (S n)

newtype Fix f n = In { out :: f (Fix f) n }

mcata :: (forall x a . (forall a' . x a' -> Const b a') -> f x a -> Const b a)
      -> Fix f a -> Const b a
mcata f = f (mcata f) . out

-- lengthList :: Fix (L e) n -> Int
lengthList = mcata phi
 where
  phi :: (forall n . x n -> Int) -> L e x n -> Int
  phi len N        = 0
  phi len (C x xs) = 1 + len xs