<div dir="ltr">I was wondering if someone could help me understand why reording 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&#39;t understand why it&#39;s a problem in one order and not the<br>

other.<br><br>I&#39;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.&nbsp; This happens with or<br>without GADTs, this version doesn&#39;t have them but they don&#39;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>

--&nbsp;&nbsp; Sealed :: a x -&gt; Sealed a<br>\end{code}<br><br><br>Originally, I noticed this in a monad context...The original was much<br>more complicated.&nbsp; But, we can simplify it even more, so keep reading.<br><br>goodOrder :: Monad m =&gt; (forall y z. p x y -&gt; q y z -&gt; q x z)<br>

&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; -&gt; m (Sealed (p x)) -&gt; (forall b. m (Sealed (q b))) -&gt; m (Sealed (q x))<br>goodOrder f mx my = do Sealed x &lt;- mx<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Sealed y &lt;- my<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; return (Sealed (f x y))<br>

<br>badOrder :: Monad m =&gt; (forall y z. p x y -&gt; q y z -&gt; q x z)<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; -&gt; m (Sealed (p x)) -&gt; (forall b. m (Sealed (q b))) -&gt; m (Sealed (q x))<br>badOrder f mx my = do Sealed y &lt;- my<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Sealed x &lt;- mx<br>

&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 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 -&gt; q y z -&gt; q x z<br>f = undefined<br>

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

\end{code}<br><br>\begin{code}<br>goodOrder :: (Sealed (p x)) -&gt; (forall b. (Sealed (q b))) -&gt; (Sealed (q x))<br>goodOrder sx sy = case sx of<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Sealed x -&gt; case sy of<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Sealed y -&gt; 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 Reorder.lhs <br>[1 of 1] Compiling Main&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; ( Reorder.lhs, Reorder.o )<br><br>Reorder.lhs:52:29:<br>

&nbsp;&nbsp;&nbsp; Inferred type is less polymorphic than expected<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Quantified type variable `x&#39; is mentioned in the environment:<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; y :: q x x1 (bound at Reorder.lhs:51:24)<br>&nbsp;&nbsp;&nbsp; When checking an existential match that binds<br>

&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; x :: p x2 x<br>&nbsp;&nbsp;&nbsp; The pattern(s) have type(s): Sealed (p x2)<br>&nbsp;&nbsp;&nbsp; The body has type: Sealed (q x2)<br>&nbsp;&nbsp;&nbsp; In a case alternative: Sealed x -&gt; Sealed (f x y)<br>&nbsp;&nbsp;&nbsp; In the expression: case sx of Sealed x -&gt; 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&#39; in the type of y, leading to the error message.<br><br>I would appreciate help understanding this, even if the help is, &quot;Go<br>

read paper X, Y, and Z.&quot;<br><br>Thanks!<br>Jason<br></div>