[Haskell] GADT type inference problem
oleg at pobox.com
oleg at pobox.com
Thu Dec 1 00:57:06 EST 2005
Let us consider the following simple code
> {-# OPTIONS -fglasgow-exts #-}
>
> 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...
More information about the Haskell
mailing list