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@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of | oleg@pobox.com | Sent: 01 December 2005 05:57 | To: haskell@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@haskell.org | http://www.haskell.org/mailman/listinfo/haskell