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

[Thiago Negri]

Got it. Thanks. :)

The gotcha for me is that I was thinking as "a generic type 'a' that I
may " and not in terms "if something is typed a generic 'a', then it
must fit in ANY type". I think this is a common mistake, as I did read
about it more than once.

I.e.,

undefined :: a means a value that can fit in any type.

(Num a => a) means a value that can fit int any type that has an
instance for Num.

My O.O. mind reacted to that as: Num a => a is a numeric type, it may
or may not be a Int.
Like type hierarchy in Java. A variable declared as "Object" does not
mean that it fits in any type. It just means that you have no
information about it's real type.

Thiago.

2012/1/4 Antoine Latter <aslatter at gmail.com>:
> 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
>
> Renaming variables to avoid shadowing:
>
> 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
>
> Rename shadowed variables:
>
> 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.
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe