[prev in list] [next in list] [prev in thread] [next in thread] 

List:       haskell-cafe
Subject:    Re: [Haskell-cafe] Need help understanding a GADT related error
From:       David Banas <capn.freako () gmail ! com>
Date:       2019-02-18 15:53:20
Message-ID: 2046D7D9-059E-48A2-A0F7-09ED66DEC357 () gmail ! com
[Download RAW message or body]

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



_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


[prev in list] [next in list] [prev in thread] [next in thread]