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

[Brandon Allbery]

This doesn't look like GADT related, just a common misunderstanding of how
types work.

"h :: H (T a)" means the *caller* determines what type 'a will be, and "h"
will work with that type. But "h" is instead using its own specific 'a.

On Mon, Feb 18, 2019 at 12:22 AM Hilco Wijbenga <hilco.wijbenga at gmail.com>
wrote:

> Hi all,
>
> I created some GADT code (see https://pastebin.com/vkJ3RzNA and
> below). When compiling this I get these errors:
>
> $ stack build
> parser-0.1.0.0: build (exe)
> Preprocessing executable 'parser' for parser-0.1.0.0..
> Building executable 'parser' for parser-0.1.0.0..
> [2 of 2] Compiling Main             ( src/Main.hs,
>
> .stack-work/dist/x86_64-linux-tinfo6/Cabal-2.2.0.1/build/parser/parser-tmp/Main.o
> )
>
> /home/hilco/workspaces/haskell/parser/src/Main.hs:30:18: error:
>    • Couldn't match type ‘a’ with ‘E’
>      ‘a’ is a rigid type variable bound by
>        the type signature for:
>          h :: forall a. H (T a)
>        at src/Main.hs:29:1-12
>      Expected type: T a
>        Actual type: T E
>    • In the expression: E' (E "E")
>      In the expression: (E' (E "E"), [])
>      In an equation for ‘h’: h [] = (E' (E "E"), [])
>    • Relevant bindings include
>        h :: H (T a) (bound at src/Main.hs:30:1)
>   |
> 30 | h []          = (E' (E "E"), [])
>   |                  ^^^^^^^^^^
>
> /home/hilco/workspaces/haskell/parser/src/Main.hs:34:16: error:
>    • Couldn't match type ‘B’ with ‘A’
>      Expected type: P Char (T A)
>        Actual type: P Char (T B)
>    • In the expression: b
>      In the second argument of ‘tt’, namely ‘[a, b]’
>      In the expression: tt h [a, b]
>   |
> 34 | tt' = tt h [a, b]
>   |                ^
>
> --  While building custom Setup.hs for package parser-0.1.0.0 using:
>
>  /home/hilco/.stack/setup-exe-cache/x86_64-linux-tinfo6/Cabal-simple_mPHDZzAJ_2.2.0.1_ghc-8.4.3
> --builddir=.stack-work/dist/x86_64-linux-tinfo6/Cabal-2.2.0.1 build
> exe:parser --ghc-options " -ddump-hi -ddump-to-file
> -fdiagnostics-color=always"
>    Process exited with code: ExitFailure 1
>
> Why is "T a" not a more generic version of "T E"? Why doesn't "T E + T
> A + TB" yield "T a" as a generic type?
>
> Cheers,
> Hilco
>
>  1 {-# LANGUAGE GADTs #-}
>  2
>  3 module Main where
>  4
>  5 data PR t a = PR (Maybe ([t], a))
>  6 data P  t a = P  ([t] -> PR t a)
>  7
>  8 a :: P Char (T A)
>  9 a = undefined
> 10
> 11 b :: P Char (T B)
> 12 b = undefined
> 13
> 14 data A = A
> 15 data B = B
> 16 data E = E String
> 17
> 18 data T a where
> 19     A' :: T A
> 20     B' :: T B
> 21     E' :: E -> T E
> 22
> 23 type H t = [Char] -> (t, [Char])
> 24 type TT t = [Char] -> [t]
> 25
> 26 tt :: H t -> [P Char t] -> TT t
> 27 tt = undefined
> 28
> 29 h :: H (T a)
> 30 h []          = (E' (E "E"), [])
> 31 h (head:rest) = (E' (E ("E")), rest)
> 32
> 33 tt' :: [Char] -> [T a]
> 34 tt' = tt h [a, b]
> 35
> 36 main :: IO ()
> 37 main = putStrLn "Hello"
> _______________________________________________
> 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.



-- 
brandon s allbery kf8nh
allbery.b at gmail.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20190218/cba98f91/attachment.html>