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

[Brandon Allbery]

On Tue, Jan 3, 2012 at 05:17, Yucheng Zhang <yczhang89 at gmail.com> wrote:

> subsome :: [RRule nt t s] -> Either String ([t], s)
>
> It seems to me that the compiler is not sure the two 'nt' are equal.
> The ScopedTypeVariables can make the compiler believe they are equal.


But ScopedTypeVariables is enabled already.

OTOH, I *think* the embedded Ord constraint is screwing things up (which is
why it's showing up in the error message), because it's embedded and
therefore has its own limited scope which prevents ScopedTypeVariables from
doing the right thing.  This idiosyncrasy is why those embedded constraints
are being removed from the language except in more controllable and useful
ways (namely GADTs; the H98 version is not capable of doing anything
useful, as I understand it, it can only screw up typing in situations like
this without actually adding anything useful to the type system, as it's
not possible to bring the Ord constraint usefully into scope outside the
data declaration itself).

(More technically, and I think this is correct:  the effective data type is

    (forall nt. Ord nt => LegGram (M.Map nt [RRule nt t s]))

Note the outer parentheses; the Ord constraint is *only* active within
those outer parentheses, meaning that it prevents the type of "nt" from
matching that in any other use of the type, even in the same expression,
even with ScopedTypeVariables.)

-- 
brandon s allbery                                      allbery.b at gmail.com
wandering unix systems administrator (available)     (412) 475-9364 vm/sms
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120103/8cf18022/attachment.htm>