Inferred type is less polymorphic than expected, depends on order

2 Oct 2008

      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

Inferred type is less polymorphic than expected, depends on order

Jason Dagit