# [Haskell-cafe] Rank2Types and pattern matching

Dan Doel dan.doel at gmail.com
Sat Jul 3 23:33:56 EDT 2010

```On Saturday 03 July 2010 10:52:31 pm Felipe Lessa wrote:
> I understood your explanation.  However, is this an implementation
> detail/bug or is it an intended feature?

Well, I wouldn't call it a bug. Perhaps it could be called a lack of a
feature, because one can imagine such pattern matches being desugared into
case statements where instantiation is allowed to happen....

But, the example here is very simple, and I can raise some issues that might
convince you that this isn't a simple issue in general, and the GHC devs are
somewhat justified in not bothering to sort it out, at your expense. :)

First, what if we write:

What type does m have? We need to instantiate the argument to do the match on
the right, so is m bound to the instantiated value, or the polymorphic value?
I guess this comes down to whether the above desugars to:

runSomeMonad m = case m of

or:

runSomeMonad v = case v of

Second, the original example is uniform regardless of how 's' is instantiated,
but that might not be true in general. If we use data families for instance:

data family T a :: *

data instance T Int  = I1 Int | I2 Char
data instance T ()   = U1 Int | U2
data instance T Char = C1 | C2 Int

f :: (forall a. T a) -> Int
...

Now, how are we going to be allowed to match in this function?

f (I1 i) = ...
f (I2 c) = ...

This, so far, desugars fine into something like:

f t = case t :: T Int of
I1 i -> ...
I2 c -> ...

but adding a third case makes the situation trickier:

f (U1 i) = ...

because that'd require instantiating t to a different type. Of course, you
could still desugar that to:

f t = case t :: T Int of
I1 i -> ...
I2 c -> ...
_    -> case t :: T () of
U1 i -> ...

but that third case is dead code. Or, should we allow mixing and matching, and
instantiate separately even at the same type:

f (I1 i) = ...
f (C2 i) = ...
f (U1 i) = ...
f (I2 i) = ...

becomes:

f t = case t :: T Int of
I1 i -> ...
_ -> case t :: T Char of
C2 i -> ...
_ -> case t :: T () of
U1 i -> ...
_ -> case t :: T Int of
I2 i -> ...

although that could be consolidated a bit.

That's off the top of my head. There may be other issues. Treating values with
polymorphic type as if they were some particular instantiation isn't a simple
matter, though.

-- Dan
```