[Haskell] GADT type inference problem

[Simon Peyton-Jones]

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: haskell-bounces at haskell.org [mailto:haskell-bounces 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 -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...
| 
| _______________________________________________
| Haskell mailing list
| Haskell at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell