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