# [Haskell-cafe] Inferred type is less polymorphic than expected, depends on order

Jason Dagit dagit at codersbase.com
Mon Oct 6 14:24:10 EDT 2008

Originally I sent this to glasgow-haskell where I was hoping someone by the
name of Simon would comment on the error message.  No one commented at all,
so I'm resending to haskell-cafe.  Thanks!

I was wondering if someone could help me understand why reordering 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...