Inferred type is less polymorphic than expected, depends on order

[Jason Dagit]

I was wondering if someone could help me understand why reording the
case statements changes the type inference for this code.

1) I find the error message a bit confusing.
2) I don't understand why it's a problem in one order and not the
other.

I've tried to send this as literate haskell in hopes that you can just
copy and paste to a file and run the example.  This happens with or
without GADTs, this version doesn't have them but they don't turn out
to make any difference.

\begin{code}
{-# LANGUAGE ExistentialQuantification, RankNTypes #-}
module Main where

data Sealed a = forall x. Sealed (a x)
-- Or equivalently:
-- data Sealed a where
--   Sealed :: a x -> Sealed a
\end{code}


Originally, I noticed this in a monad context...The original was much
more complicated.  But, we can simplify it even more, so keep reading.

goodOrder :: Monad m => (forall y z. p x y -> q y z -> q x z)
          -> m (Sealed (p x)) -> (forall b. m (Sealed (q b))) -> m (Sealed
(q x))
goodOrder f mx my = do Sealed x <- mx
                       Sealed y <- my
                       return (Sealed (f x y))

badOrder :: Monad m => (forall y z. p x y -> q y z -> q x z)
         -> m (Sealed (p x)) -> (forall b. m (Sealed (q b))) -> m (Sealed (q
x))
badOrder f mx my = do Sealed y <- my
                      Sealed x <- mx
                      return (Sealed (f x y))


Several helpful people in #haskell helped me converge on this greatly
simplified version below.

\begin{code}
f :: p x y -> q y z -> q x z
f = undefined
\end{code}

\begin{code}
badOrder :: (Sealed (p x)) -> (forall b. (Sealed (q b))) -> (Sealed (q x))
badOrder sx sy = case sy of
                 Sealed y -> case sx of
                             Sealed x -> Sealed (f x y)
\end{code}

\begin{code}
goodOrder :: (Sealed (p x)) -> (forall b. (Sealed (q b))) -> (Sealed (q x))
goodOrder sx sy = case sx of
                  Sealed x -> case sy of
                              Sealed y -> Sealed (f x y)
\end{code}


\begin{code}
main = return ()
\end{code}

This gives the error:
$ ghc --make Reorder.lhs
[1 of 1] Compiling Main             ( Reorder.lhs, Reorder.o )

Reorder.lhs:52:29:
    Inferred type is less polymorphic than expected
      Quantified type variable `x' is mentioned in the environment:
        y :: q x x1 (bound at Reorder.lhs:51:24)
    When checking an existential match that binds
        x :: p x2 x
    The pattern(s) have type(s): Sealed (p x2)
    The body has type: Sealed (q x2)
    In a case alternative: Sealed x -> Sealed (f x y)
    In the expression: case sx of Sealed x -> Sealed (f x y)

After discussing this a bit, I think what may be happening in the
badOrder case is that the existentially bound type of x is bound after
the type `b' in the type of y, leading to the error message.

I would appreciate help understanding this, even if the help is, "Go
read paper X, Y, and Z."

Thanks!
Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20081001/ec2e4262/attachment-0001.htm