[Haskell-cafe] Rank2Types and pattern matching

[Dan Doel]

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:

  runSomeMonad m@(SomeMonad x) = ...

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
                     SomeMonad x -> ...

or:

  runSomeMonad v = case v of
                     m@(SomeMonad x) -> ...

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