> Actually, my question is why the different type can't be unified with the inferred type?

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.

As we said before, you have three ways to work it out:
1) Use scoped type variables with explicit forall nt on legSome and no forall on subsome, so that nt in subsome matches nt declared in legSome.
2) Don't give a type signature for subsome and let GHC find out which is its correct type.
3) Extract subsome so that it becomes a top-level function with a polymorphic type (Recommended).


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.
So this error is:
> Couldn't match expected type `Int'
>               with actual type `[([Symbols nt t], [s] -> t0)]
>                                 -> Either [Char] ([t], t0)'
>   In the expression: subsome :: Int
GHC tells you the type it infers for subsome: [([Symbols nt t], [s] -> t0)] -> Either [Char] ([t], t0)
The nt you see is the one from legSome, those messages show scoped variables. (You'd get something like 'nt1' or 'nt0' if it was another variable, meant to be instanciated to a different type).
This accords with your previous error message, which happens to give you more details about where the rigid type variable nt comes from:
>      `nt' is a rigid type variable bound by
>           the type signature for
>             legSome :: LegGram nt t s -> nt -> Either String ([t], s)

HTH.

2012/1/3 Yucheng Zhang <yczhang89@gmail.com>
On Wed, Jan 4, 2012 at 2:48 AM, Bardur Arantsson <spam@scientician.net> wrote:
> 'subsome' to a different type than the one you intended -- and indeed one
> which can't be unified with the inferred type. (Unless you use
> ScopedTypeVariables.)

Thanks for the reply.

Actually, my question is why the different type can't be unified with
the inferred type? Could you point me some related resources?

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe