GHC 7.4.1

GADT syntax, compiler error

{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}

data Expr :: * -> * where
  Int :: Int -> Expr Int
  Bool :: Bool -> Expr Bool
  IsZero :: Expr Int -> Expr Bool
--  Plus :: (* -> *) -> (* -> *) -> (* ->
  If :: Expr Bool -> Expr a -> Expr a -> Expr a

data Zero
data Succ a

type family Sum m n
type instance Sum Zero n = n
type instance Sum (Succ p) n = Succ(Sum p n)

data Nat :: * -> * where
  Zero :: Nat Zero
  Succ :: Nat n -> Nat (Succ n) --Why is the declaration of data Succ
a needed? (above)

data Vec :: * -> * -> * where
  Nil :: Vec a Zero
  Cons :: a -> Vec a n -> Vec a (Succ n)

instance (Show a,Show n) => Show (Vec a n) where
  show Nil = "Vec0()"
  show (Cons a Nil) = "Vec(" ++ (show a) ++ ")"
  show (Cons a (Cons a2 v)) = "Vec(" ++ (show a) ++ "," ++ (show a2) ++ ")"

instance (Show a) -> Nat a where
  show Zero = "Zero"
  show (Succ a) = "Succ " ++ (show a)


vechead :: Vec a (Succ n) -> a
vechead (Cons x xs) = x

vectail :: Vec a (Succ n) -> Vec a n
vectail (Cons x xs) = xs