> f :: a -> a
> f x = x :: a  -- invalid

Perfect example indeed.

> The confusing point to me is that the 'a' from 'f' type signature on
> its own is not universally quantified as I expected,
> and it is dependent on the type of 'f'.

> This dependence is not obvious for a beginner like me.

It's indeed counterintuitive, as you'd expect type variables to be scoped, but just note that:
You have only one simple rule to remember: "All type variables appearing in a type expression get automatically universally quantified at the beginning of this expression".
Practically : When you see an type variable v, then GHC automatically puts a 'forall v' at the beginning of the whole expression. No exceptions done, no ambiguity at all as long as ScopedTypeVariables stays unactivated.
Following this one rule, it's clear that the example above cannot but become:

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

Which is obviously wrong: when you have entered f, x has been instatiated to a specific type 'a', and then you want it to x to be of any type? That doesn't make sense.

It's only logical.


2012/1/4 Yucheng Zhang <yczhang89@gmail.com>
On Wed, Jan 4, 2012 at 3:46 AM, Yves Parès <limestrael@gmail.com> wrote:
> Because without ScopedTypeVariable, both types got expanded to :
>
> legSome :: forall nt t s. LegGram nt t s -> nt -> Either String ([t], s)
>
> subsome :: forall nt t s. [RRule nt t s] ->  Either String ([t], s)
>
> So you see subsome declare new variables, which do not match the rigid ones
> declared by legSome signature, hence the incompatibility.
>

It's not obvious to see the incompatibility. I looked into the Haskell
2010 Language
Report, and found my question answered in Section 4.4.1, along with a minimal
reproducing example:

f :: a -> a
f x = x :: a  -- invalid

The confusing point to me is that the 'a' from 'f' type signature on
its own is not
universally quantified as I expected, and it is dependent on the type of 'f'.

This dependence is not obvious for a beginner like me.

ScopedTypeVariables will help to express the dependence exactly. And moving
'subsome' to top-level will prevent from bringing in the dependent type.

> Now, concerning the error I asked you to deliberately provoke, that's the
> quickest way I found to know what is the output of the type inferer, and
> maybe the only simple one.

I find this one of the most interesting tricks I've seen.

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe