<br><br><div class="gmail_quote">On Sat, Jul 3, 2010 at 4:24 PM, Yves Parès <span dir="ltr">&lt;<a href="mailto:limestrael@gmail.com">limestrael@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hello everybody,<br><br>I&#39;m trying to implement the type protection used by ST to prevent a monad from returning a certain type.<br>There&#39;s my code:<br><br><span><span></span></span><span><span></span></span><span><span></span></span><span><span></span></span>import Control.Monad.Identity<br>

<br>newtype SomeMonad s a = SomeMonad { unSome :: Identity a }<br>  deriving (Monad)<br><br>newtype SomeType s = SomeType Int<br><br>runSomeMonad :: (forall s. SomeMonad s a) -&gt; a<br>runSomeMonad (SomeMonad x) = runIdentity x<br>

<br>And when compiled, I got this error:<br>phantom.hs:10:14:<br>    Couldn&#39;t match expected type `forall s. PwetMonad s a&#39;<br>           against inferred type `PwetMonad s a1&#39;<br>    In the pattern: PwetMonad x<br>

    In the definition of `runPwetMonad&#39;:<br>        runPwetMonad (PwetMonad x) = runIdentity x<br><br>But when I change line 10 to:<br>runSomeMonad x = runIdentity . unSome $ x<br><br>then it works, so obviously, the trouble is about pattern matching.<br>

What was I doing wrong?<br></blockquote><div><br></div><div>I think it has to do with the order that the foralls are instantiated, but when that comes up it always surprises me and I find it very confusing as well.</div>
<div><br></div><div>The error message is saying that the constructor (SomeMonad) has type forall s1 a1. SomeMonad s1 a1 but that the function signature requires it to have have type forall a. (forall s. SomeMonad s a).</div>
<div><br></div><div>If you introduce a case expression the error goes away:</div><div><div>runSomeMonad :: (forall s. SomeMonad s a) -&gt; a</div><div>runSomeMonad m = case m of</div><div>             SomeMonad x -&gt; runIdentity x</div>
</div><div><br></div><div>My, vague and likely incorrect, understanding is that the order that the type checker/inferencer picks the types for s and a can make examples like this fail and changing the expression so that it must pick them later/differently fixes it.  Perhaps someone can correct my understanding.</div>
<div><br></div><div>In the case where you use unSome, I suspect the reason it works is because unSome works for any s and a so the difference in order of choice doesn&#39;t matter to applications of unSome.  At least, that&#39;s my vague understanding.</div>
<div><br></div><div>I hope that helps,</div><div>Jason</div></div>