Hilco, Your first error arrises, because you’re offering to the caller of `h` that she may demand any type of `a`, but are “hard-wiring” `a :: T E` in the definition of that function. Reflecting that fact in the function type signature eliminates the error: -- h :: H (T a) h :: H (T E) h [] = (E' (E "E"), []) h (head:rest) = (E' (E ("E")), rest) Your second error is explained (I hope) in the comments I’ve added to your original code: tt' :: [Char] -> [T a] tt' = tt h [a, b] -- tt :: H t -> [P Char t] -> TT t -- :: ([Char] -> (t, [Char])) -> [P Char t] -> [Char] -> [t] -- -- h :: [Char] -> (t, [Char]) ~ H (T E) -- h :: [Char] -> (t, [Char]) ~ [Char] -> (T E, [Char]) -- ==> t ~ T E -- -- [a, b] :: [P Char t] -- a :: P Char (T E) /~ P Char (T A) -- b :: P Char (T E) /~ P Char (T B) -db