<div dir="ltr">This doesn't look like GADT related, just a common misunderstanding of how types work.<div><br></div><div>"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.</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Feb 18, 2019 at 12:22 AM Hilco Wijbenga <<a href="mailto:hilco.wijbenga@gmail.com">hilco.wijbenga@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi all,<br>
<br>
I created some GADT code (see <a href="https://pastebin.com/vkJ3RzNA" rel="noreferrer" target="_blank">https://pastebin.com/vkJ3RzNA</a> and<br>
below). When compiling this I get these errors:<br>
<br>
$ stack build<br>
parser-0.1.0.0: build (exe)<br>
Preprocessing executable 'parser' for parser-0.1.0.0..<br>
Building executable 'parser' for parser-0.1.0.0..<br>
[2 of 2] Compiling Main ( src/Main.hs,<br>
.stack-work/dist/x86_64-linux-tinfo6/Cabal-2.2.0.1/build/parser/parser-tmp/Main.o<br>
)<br>
<br>
/home/hilco/workspaces/haskell/parser/src/Main.hs:30:18: error:<br>
• Couldn't match type ‘a’ with ‘E’<br>
‘a’ is a rigid type variable bound by<br>
the type signature for:<br>
h :: forall a. H (T a)<br>
at src/Main.hs:29:1-12<br>
Expected type: T a<br>
Actual type: T E<br>
• In the expression: E' (E "E")<br>
In the expression: (E' (E "E"), [])<br>
In an equation for ‘h’: h [] = (E' (E "E"), [])<br>
• Relevant bindings include<br>
h :: H (T a) (bound at src/Main.hs:30:1)<br>
|<br>
30 | h [] = (E' (E "E"), [])<br>
| ^^^^^^^^^^<br>
<br>
/home/hilco/workspaces/haskell/parser/src/Main.hs:34:16: error:<br>
• Couldn't match type ‘B’ with ‘A’<br>
Expected type: P Char (T A)<br>
Actual type: P Char (T B)<br>
• In the expression: b<br>
In the second argument of ‘tt’, namely ‘[a, b]’<br>
In the expression: tt h [a, b]<br>
|<br>
34 | tt' = tt h [a, b]<br>
| ^<br>
<br>
-- While building custom Setup.hs for package parser-0.1.0.0 using:<br>
/home/hilco/.stack/setup-exe-cache/x86_64-linux-tinfo6/Cabal-simple_mPHDZzAJ_2.2.0.1_ghc-8.4.3<br>
--builddir=.stack-work/dist/x86_64-linux-tinfo6/Cabal-2.2.0.1 build<br>
exe:parser --ghc-options " -ddump-hi -ddump-to-file<br>
-fdiagnostics-color=always"<br>
Process exited with code: ExitFailure 1<br>
<br>
Why is "T a" not a more generic version of "T E"? Why doesn't "T E + T<br>
A + TB" yield "T a" as a generic type?<br>
<br>
Cheers,<br>
Hilco<br>
<br>
1 {-# LANGUAGE GADTs #-}<br>
2<br>
3 module Main where<br>
4<br>
5 data PR t a = PR (Maybe ([t], a))<br>
6 data P t a = P ([t] -> PR t a)<br>
7<br>
8 a :: P Char (T A)<br>
9 a = undefined<br>
10<br>
11 b :: P Char (T B)<br>
12 b = undefined<br>
13<br>
14 data A = A<br>
15 data B = B<br>
16 data E = E String<br>
17<br>
18 data T a where<br>
19 A' :: T A<br>
20 B' :: T B<br>
21 E' :: E -> T E<br>
22<br>
23 type H t = [Char] -> (t, [Char])<br>
24 type TT t = [Char] -> [t]<br>
25<br>
26 tt :: H t -> [P Char t] -> TT t<br>
27 tt = undefined<br>
28<br>
29 h :: H (T a)<br>
30 h [] = (E' (E "E"), [])<br>
31 h (head:rest) = (E' (E ("E")), rest)<br>
32<br>
33 tt' :: [Char] -> [T a]<br>
34 tt' = tt h [a, b]<br>
35<br>
36 main :: IO ()<br>
37 main = putStrLn "Hello"<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>brandon s allbery kf8nh</div><div><a href="mailto:allbery.b@gmail.com" target="_blank">allbery.b@gmail.com</a></div></div></div></div></div>