[Haskell] GADT type inference problem
Simon PeytonJones
simonpj at microsoft.com
Thu Dec 1 03:55:29 EST 2005
This is a bug, thank you.
I've added it to the test suite, but I'm in the middle of revising the
GADT impl so I won't fix it right off.
Simon
 Original Message
 From: haskellbounces at haskell.org [mailto:haskellbounces at haskell.org]
On Behalf Of
 oleg at pobox.com
 Sent: 01 December 2005 05:57
 To: haskell at haskell.org
 Subject: [Haskell] GADT type inference problem


 Let us consider the following simple code

 > {# OPTIONS fglasgowexts #}
 >
 > module Foo where
 >
 > data Term a where
 > B :: Bool > Term Bool
 > C :: Term Bool > Term t > Term t
 > I :: Int > Term Int
 >
 > shw (I t) = ("I "++) . shows t
 > shw (B t) = ("B "++) . shows t
 > shw (C p q) = ("Cnd "++) . (shw p) . (shw q)

 It loads in GHCi 6.4 and 6.4.1:

 Prelude> :l /tmp/g.hs
 Compiling Foo ( /tmp/g.hs, interpreted )
 Ok, modules loaded: Foo.
 *Foo> :t I 1
 I 1 :: Term Int
 *Foo> :t B True
 B True :: Term Bool

 However, when we do

 *Foo> :t shw
 shw :: Term Bool > String > [Char]

 The inferred type of shw shows that it takes the values of
 Term *Bool*. And yet the very first clause of shw mentions (I t),
which
 GHCi correctly reports to be of the type Term Int...

 It seems the last clause of shw confuses GHCi: if we remove it, the
 inferred type of shw is "Term a > String > [Char]", as one would
expect.

 That is not a type expression printing problem:

 *Foo> shw (I 1)

 <interactive>:1:5:
 Couldn't match `Bool' against `Int'
 Expected type: Term Bool
 Inferred type: Term Int
 In the application `I 1'

 the first clause of shw notwithstanding...

 _______________________________________________
 Haskell mailing list
 Haskell at haskell.org
 http://www.haskell.org/mailman/listinfo/haskell
More information about the Haskell
mailing list