[Haskell-cafe] Limits of deduction

[Roberto Zunino]

Christopher L Conway wrote:

> On 5/14/07, Roberto Zunino <zunino at di.unipi.it> wrote:
> 
>> Also, using only rank-1:
>>
>> polyf :: Int -> a -> Int
>> polyf x y = if x==0 then 0
>>              else if x==1 then polyf (x-1) (\z->z)
>>              else polyf (x-2) 3
>>
>> Here passing both 3 and (\z->z) as y confuses the type inference.
> 
> 
> Actually, I tried this in ghci... Should this work?
> 
> polyf.hs:
> polyf x y = if x==0 then 0
>            else if x==1 then polyf (x-1) (\z->z)
>            else polyf (x-2) 3
> 
> NOTE: no type signature

I forgot to mention a *use* of that as in

test = polyf 1 2

Then:    No instance for (Num (t -> t))
(see also below)

Also, we can avoid type classes and _still_ have inference problems:
using (3 :: Int) in polyf yields:
   Couldn't match expected type `Int' against inferred type `t -> t'

which is actually the type mismatch error I had in mind.

So, even in Haskell - type classes, we need signatures in some cases.

> Prelude> :l polyf
> [1 of 1] Compiling Main             ( polyf.hs, interpreted )
> Ok, modules loaded: Main.
> *Main> :t polyf
> 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?

Yes, because Haskell natural literals are overloaded:
  3 :: forall a. Num a => a

So 3 :: (t1 -> t1) is "fine" provided you supply a Num instance for 
that. Alas, only trivial instances exists (0=1=2=..=id).

Zun.