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

[Yves Parès]

> 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 at gmail.com>

> On Wed, Jan 4, 2012 at 3:46 AM, Yves Parès <limestrael at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120104/02786674/attachment.htm>