[Haskell-cafe] Limits of deduction

[Matthew Brecknell]

Roberto Zunino:
> Here passing both 3 and (\z->z) as y confuses the type inference.

Christopher L Conway:
> polyf :: forall a t1 t.
> (Num (t1 -> t1), Num a, Num t) =>
> a -> (t1 -> t1) -> t
> 
> The inference assigns y the type (t1 -> t1) even though it is assigned
> the value 3?

Almost. It assigns y the type (Num (t1 -> t1) => t1 -> t1). If you're
wondering where the Num context came from, note that the literal "3" is
read as "fromInteger 3", which has type (Num a => a). Unifying (t1 ->
t1) with (Num a => a) gives (Num (t1 -> t1) => t1 -> t1).

So the type inference is not really confused at all. It just gives a
not-very-useful type. To demonstrate the perfectly logical behaviour of
the typechecker, we just need a little more absurd code:

> {-# OPTIONS_GHC -fglasgow-exts #-}
> 
> -- ^ Extensions are needed for relaxed instances only,
> --   no rank-n polymorphism here.
> 
> instance Show (t -> t) where
>   show _ = "<function>"
> 
> instance Eq (t -> t) where
>   _ == _ = False
> 
> instance Num (t -> t) where
>   _ + _ = id
>   _ - _ = id
>   _ * _ = id
>   abs _ = id
>   signum _ = id
>   fromInteger _ = id

Et, voila:

*PolyF> :t polyf
polyf :: (Num a, Num t) => a -> (t1 -> t1) -> t
*PolyF> polyf 3 3
0