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