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.