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

[Hilco Wijbenga]

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"