[Haskell-cafe] Solved but strange error in type inference
yczhang89 at gmail.com
Wed Jan 4 12:35:26 CET 2012
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
Report, and found my question answered in Section 4.4.1, along with a minimal
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.
More information about the Haskell-Cafe