[Haskell] GADT type inference problem

[David Menendez]

oleg at pobox.com writes:

> 
> 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)
...
> 
> 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*. 

As I understand it, GHC can't infer the most general type signature when
GADTs are involved. It should work if shw has an explicit type
signature, e.g. shw :: Term a -> ShowS

What's strange is that GHC accepted the code at all. There would
probably be less confusion if GADT arguments always required a
signature, like arguments involving higher-rank polymorphism.
-- 
David Menendez <zednenem at psualum.com> | "In this house, we obey the laws
<http://www.eyrie.org/~zednenem>      |        of thermodynamics!"