[Haskell-cafe] Need help understanding a GADT related error

[David Banas]

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