<div dir="ltr">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!<br><br>I was wondering if someone could help me understand why reordering the<br>
case statements changes the type inference for this code.<br><br>1) I find the error message a bit confusing.<br>2) I don't understand why it's a problem in one order and not the<br>
other.<br><br>I've tried to send this as literate haskell in hopes that you can just<br>copy and paste to a file and run the example. This happens with or<br>without GADTs, this version doesn't have them but they don't turn out<br>
to make any difference.<br><br>\begin{code}<br>{-# LANGUAGE ExistentialQuantification, RankNTypes #-}<br>module Main where<br><br>data Sealed a = forall x. Sealed (a x)<br>-- Or equivalently:<br>-- data Sealed a where<br>
-- Sealed :: a x -> Sealed a<br>\end{code}<br><br><br>Originally, I noticed this in a monad context...The original was much<br>more complicated. But, we can simplify it even more, so keep reading.<br><br>goodOrder :: Monad m => (forall y z. p x y -> q y z -> q x z)<br>
-> m (Sealed (p x)) -> (forall b. m (Sealed (q b))) -> m (Sealed (q x))<br>goodOrder f mx my = do Sealed x <- mx<br> Sealed y <- my<br> return (Sealed (f x y))<br>
<br>badOrder :: Monad m => (forall y z. p x y -> q y z -> q x z)<br> -> m (Sealed (p x)) -> (forall b. m (Sealed (q b))) -> m (Sealed (q x))<br>badOrder f mx my = do Sealed y <- my<br> Sealed x <- mx<br>
return (Sealed (f x y))<br><br><br>Several helpful people in #haskell helped me converge on this greatly<br>simplified version below.<br><br>\begin{code}<br>f :: p x y -> q y z -> q x z<br>f = undefined<br>
\end{code}<br><br>\begin{code}<br>badOrder :: (Sealed (p x)) -> (forall b. (Sealed (q b))) -> (Sealed (q x))<br>badOrder sx sy = case sy of<br> Sealed y -> case sx of<br> Sealed x -> Sealed (f x y)<br>
\end{code}<br><br>\begin{code}<br>goodOrder :: (Sealed (p x)) -> (forall b. (Sealed (q b))) -> (Sealed (q x))<br>goodOrder sx sy = case sx of<br> Sealed x -> case sy of<br> Sealed y -> Sealed (f x y)<br>
\end{code}<br><br><br>\begin{code}<br>main = return ()<br>\end{code}<br><br>This gives the error:<br>$ ghc --make <span class="nfakPe">Reorder</span>.lhs <br>[1 of 1] Compiling Main ( <span class="nfakPe">Reorder</span>.lhs, <span class="nfakPe">Reorder</span>.o )<br>
<br><span class="nfakPe">Reorder</span>.lhs:52:29:<br>
Inferred type is less polymorphic than expected<br> Quantified type variable `x' is mentioned in the environment:<br> y :: q x x1 (bound at <span class="nfakPe">Reorder</span>.lhs:51:24)<br> When checking an existential match that binds<br>
x :: p x2 x<br> The pattern(s) have type(s): Sealed (p x2)<br> The body has type: Sealed (q x2)<br> In a case alternative: Sealed x -> Sealed (f x y)<br> In the expression: case sx of Sealed x -> Sealed (f x y)<br>
<br>After discussing this a bit, I think what may be happening in the<br>badOrder case is that the existentially bound type of x is bound after<br>the type `b' in the type of y, leading to the error message.<br><br>I would appreciate help understanding this, even if the help is, "Go<br>
read paper X, Y, and Z."<br><br>Thanks!<br>Jason</div>