Ashley Yakeley wrote:

In article 
<r02010400-1040-A0BE089CBF6111D99910000393758032@[10.0.1.2]>,
 David Menendez <zednenem@psualum.com> wrote:

data Vec 0   a = Nil
data Vec s v a = Cons a (v a)

Some aliases for convenience:

type Vec 1 = Vec s Vec 0
type Vec 2 = Vec s Vec 1
type Vec 3 = Vec s Vec 2
type Vec 4 = Vec s Vec 3


I don't understand this at all, and neither does GHC.

You seem to have lost the underscores :-)
It can be written without underscores as:

data Vec0 a = Nil
data VecS v a = Cons a (v a)

type Vec1 = VecS Vec0
type Vec2 = VecS Vec1

All the best,
Daan Leijen

Btw. David: nice example of useful GADT use!