> 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 <yczhan...@gmail.com> > On Wed, Jan 4, 2012 at 3:46 AM, Yves Parès <limestr...@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 >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe