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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
