[Haskell-cafe] GADTs and bar :: Foo t1 -> Foo t2

Hello, I have a recursive type

data Foo = A | B [Foo] | C [Foo]

that I would like to restrict so that a C can only contain Bs, and a B can only contain As. If I use a GADT as follows the bar function, understandably, will not type check.

data AType data BType data CType

data Foo a where A :: Foo AType B :: [Foo AType] -> Foo BType C :: [Foo BType] -> Foo CType

--get the successor of the Foo bar c@(C [] ) = c bar (C (b:_)) = b bar b@(B [] ) = b bar (B (a:_)) = a bar a@A = a

How do I achieve this restriction? Do I need to have some sort of successor class with dependent types? Ta Daniel