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

[Yucheng Zhang]

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.