# [Haskell-cafe] Solved but strange error in type inference

Antoine Latter aslatter at gmail.com
Wed Jan 4 16:24:33 CET 2012

```On Wed, Jan 4, 2012 at 9:08 AM, Thiago Negri <evohunz at gmail.com> wrote:
> Do not compile:
>
> f :: a -> a
> f x = x :: a
>
>    Couldn't match type `a' with `a1'
>      `a' is a rigid type variable bound by
>          the type signature for f :: a -> a at C:\teste.hs:4:1
>      `a1' is a rigid type variable bound by
>           an expression type signature: a1 at C:\teste.hs:4:7
>    In the expression: x :: a
>    In an equation for `f': f x = x :: a
>
>
> Any of these compiles:
>
> f :: a -> a
> f x = undefined :: a

Re-written:

f :: forall a . a -> a
f x = undefined :: forall a . a

f :: forall a . a -> a
f x = undefined :: forall b . b

Which is allowed.

The rest of your examples are similar - a new value is introduced with
a new type that can unify with the required type.

This is different from the failing case:

g :: a -> a
g x = x :: a

Let's go through the same process.

Insert foralls:

g :: forall a . a -> a
g x = x :: forall a . a

g :: forall a . a -> a
g x = x :: forall b . b

In the function body we have declared that the value 'x' may take on
any value. But that's not true! The value 'x' comes from the input to
the function, which is a fixed 'a' decided by the caller.

So it does not type-check.

Antoine

>
> f :: Num a => a -> a
> f x = undefined :: a
>
> f :: Int -> Int
> f x = undefined :: a
>
> f :: Int -> Int
> f x = 3 :: (Num a => a)
>
>
> Can someone explain case by case?
>
> Thanks,
> Thiago.
>
> 2012/1/4 Yves Parès <limestrael at gmail.com>:
>>> I don't see the point in universally quantifying over types which are
>> already present in the environment
>>
>> I think it reduces the indeterminacy you come across when you read your
>> program ("where does this type variable come from, btw?")
>>
>>
>>> So is there anyway to "force" the scoping of variables, so that
>>> f :: a -> a
>>> f x = x :: a
>>> becomes valid?
>>
>> You mean either than compiling with ScopedTypeVariables and adding the
>> explicit forall a. on f? I don't think.
>>
>> 2012/1/4 Brandon Allbery <allbery.b at gmail.com>
>>
>> On Wed, Jan 4, 2012 at 08:41, Yves Parès <limestrael at gmail.com> wrote:
>>>
>>> Would you try:
>>>
>>> f :: a -> a
>>>
>>> f x = undefined :: a
>>>
>>> And tell me if it works? IMO it doesn't.
>>
>>>  It won't
>>
>> Apparently, Yucheng says it does.
>>
>> _______________________________________________