W-types, following the Agde code here: http://www.e-pig.org/epilogue/?p=324

W-types.hs

{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, UndecidableInstances #-}

-- Type level functions
type family Apply f a :: *
data f :.: g -- function composition
type instance Apply (f :.: g) a = Apply f (Apply g a)
data Fst
type instance Apply Fst (a, b) = a
data Snd
type instance Apply Snd (a, b) = b

-- W-types
-- s is a GADT limiting which types i are allowed
data W s p where
  (:<:) :: s i -> (Apply p i -> W s p) -> W s p


data Void
magic :: Void -> a
magic x = x `seq` error "we never get this far"

data F
data T
data T2 i where
  F :: T2 F
  T :: T2 T
data f :+: t -- Type level functions from T2
type instance Apply (f :+: t) F = f
type instance Apply (f :+: t) T = t


-- Natural numbers
type Nat = W T2 (Void :+: ())

zero :: Nat
zero = F :<: magic
suc :: Nat -> Nat
suc n = T :<: const n


-- Binary trees (without labels)
type Tree = W T2 (Void :+: Bool)

leaf :: Tree
leaf = F :<: magic
node :: Tree -> Tree -> Tree
node l r = T :<: (\b -> case b of True -> l; False -> r)  


-- Labeled W-types
data Sigma a b i where
  S :: a i -> Apply b i -> Sigma a b (i, Apply b i)
type LW s lp = W (Sigma s (Fst :.: lp)) (Snd :.: lp :.: Fst)


-- Lists
type List x = LW T2 (((), Void) :+: (x, ()))

nil :: List x
nil = S F () :<: magic
cons :: x -> List x -> List x
cons x xs = S T x :<: const xs


-- Checking that we can actually compute with these types.
append :: List x -> List x -> List x
append (S F () :<: _) ys = ys
append (S T x  :<: f) ys = x `cons` f () `append` ys