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

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

On Wed, Jan 4, 2012 at 3:46 AM, Yves Parès 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