[Haskell-cafe] Learning GADT types to simulate dependent types

[Paul Johnson]

I'm trying to understand how to use GADT types to simulate dependent 
types.  I'm trying to write  a version of list that uses Peano numbers 
in the types to keep track of how many elements are in the list.  Like this:

{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

module Plist where


infixr 3 :|

data Zero

data S a

class Add n1 n2 t | n1 n2 -> t, n1 t -> n2

instance Add Zero n n
instance Add (S n1) n2 (S t)

data Plist n a where
    Nil :: Plist Zero a
    (:|) :: a -> Plist n a -> Plist (S n) a

instance (Show a) => Show (Plist n a) where
    show Nil = "Nil"
    show (x :| xs) = show x ++ " :| " ++ show xs

pHead :: Plist (S n) a -> a
pHead (x :| _) = x

pTail :: Plist (S n) a -> Plist n a
pTail (_ :| xs) = xs


pConcat Nil ys = ys
pConcat (x :| xs) ys = x :| pConcat xs ys


Everything works except the last function (pConcat).  I figured that it 
should add the lengths of its arguments together, so I created a class 
Add as shown in the Haskell Wiki at 
http://www.haskell.org/haskellwiki/Type_arithmetic.  But now I'm stuck.  
When I try to load this module I get:

Plist.hs:32:8:
    GADT pattern match in non-rigid context for `Nil'
      Tell GHC HQ if you'd like this to unify the context
    In the pattern: Nil
    In the definition of `pConcat': pConcat Nil ys = ys
Failed, modules loaded: none.

(Line 32 is "pConcat Nil ys = ys")

So how do I do this?  Am I on the right track?  Can someone help improve 
my Oleg rating?

Thanks,

Paul.