[Haskell-cafe] Rank2Types and pattern matching

Dan Doel dan.doel at gmail.com
Sat Jul 3 20:12:50 EDT 2010

On Saturday 03 July 2010 7:24:17 pm Yves Parès wrote:
> 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?

The problem is instantiation. SomeMonad is a constructor for the type

  SomeMonad s a

for any *particular* s and a. But the type:

  forall s. SomeMonad s a

is not that type. That type doesn't have constructors (proper) at all, and 
hence you cannot match against it. If types were passed explicitly, then 
values of the second type would look like:

  /\s -> ...

Where the big lambda is type abstraction. But you can't match against this, of 
course (just as you can't match against functions as lambda expressions), you 
can only apply values of this type.

In the second case, when you write:

  runIdentity . unSome $ x

you are implicitly instantiating x to some particular s (which? I can't say; I 
suppose it doesn't matter), which allows you to to match against it, or use 
unSome as you are. If type passing were explicit, it'd look like:

  runIdentity . unSome $ x@()

picking s = (), for example. You could also do a case like:

  case x@() of
    SomeMonad m -> ...

which in GHC would just look like:

  case x of
    SomeMonad m -> ...

which can be confusing, because one would expect to be able to collapse that 
into a direct match in the function definition, but you cannot, because you 
have to apply x to a type before you match on it.

-- Dan

More information about the Haskell-Cafe mailing list