[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)

    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