[Haskell-cafe] Rank2Types and pattern matching

[Jason Dagit]

On Sat, Jul 3, 2010 at 4:24 PM, Yves Parès <limestrael at gmail.com> wrote:

> Hello everybody,
>
> I'm trying to implement the type protection used by ST to prevent a monad
> from returning a certain type.
> There's my code:
>
> import Control.Monad.Identity
>
> newtype SomeMonad s a = SomeMonad { unSome :: Identity a }
>   deriving (Monad)
>
> newtype SomeType s = SomeType Int
>
> runSomeMonad :: (forall s. SomeMonad s a) -> a
> runSomeMonad (SomeMonad x) = runIdentity x
>
> And when compiled, I got this error:
> phantom.hs:10:14:
>     Couldn't match expected type `forall s. PwetMonad s a'
>            against inferred type `PwetMonad s a1'
>     In the pattern: PwetMonad x
>     In the definition of `runPwetMonad':
>         runPwetMonad (PwetMonad x) = runIdentity x
>
> But when I change line 10 to:
> runSomeMonad x = runIdentity . unSome $ x
>
> then it works, so obviously, the trouble is about pattern matching.
> What was I doing wrong?
>

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.

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).

If you introduce a case expression the error goes away:
runSomeMonad :: (forall s. SomeMonad s a) -> a
runSomeMonad m = case m of
             SomeMonad x -> runIdentity x

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.

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't
matter to applications of unSome.  At least, that's my vague understanding.

I hope that helps,
Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100703/8896a211/attachment.html