GeneralisedPatternSynonyms.md

Consider an extensible sum type:

data Union (es :: [Type]) where
  Here  :: e        -> Union (e ': es)
  There :: Union es -> Union (e ': es)

We define a few functions for taking it apart and doing operations on it

type family Delete (n :: Nat) (es :: [k]) :: [k] where
  Delete ZN     (e ': es) = es
  Delete (SN n) (e ': es) = e ': Delete n es

data Elem (es :: [Type]) (e :: Type) n where
  EZ :: Elem (e ': es) e ZN
  ES :: Elem es e n -> Elem (e1 ': es) e (SN n)
class Member (es :: [Type]) (e :: Type) n | es e -> n where
  member :: Elem es e n
instance (n ~ ZN) => Member (e ': es) e n where member = EZ
...

uCase
  :: Elem es e n
  -> (e -> r)
  -> (Union (Delete n es) -> r)
  -> Union es -> r
uCase EZ     here _there (Here x)  = here x
uCase EZ     _here there (There u) = there u
...

uMatch :: forall (e :: Type) es n r. Member es e n
  => (e -> r)
  -> (Union (Delete n es) -> r)
  -> Union es -> r
uMatch = uCase (member @es @e)

uInject :: forall (e :: Type) es n. Member es e n => e -> Union es
uInject = ...

We can then write code like

foo :: Union '[Int, Bool, Char] -> String
foo = uMatch @Int (\x -> show (x+1))
    $ uMatch @Char (\x -> show (c:[]))
    $ uMatch @Bool (\x -> show (not x))
    $ \case{}

You might consider writing a pattern synonym so that this looks like a normal case

pattern U :: forall (e :: Type) {es} {n}. Member es e n
          => e -> Union es
pattern U <- ( (uMatch @e Just (const Nothing)) -> Just x) 
  where U @e x -> uInject @e x
  
foo :: Union '[Int, Bool, Char] -> String
foo x = case x of
  U @Int x -> ...
  U @Bool x -> ...
  U @Char x -> ...

But we lose exhaustivity checking (via uMatch), because uMatch refines the "residual" type in the failure continuation, but pattern synonym just throws the residual away.

There is also no {-# COMPLETE #-} pragma that will help us here

Currently GHC desugars pattern U to a matcher function

$mU :: forall (r :: ?) (e :: Type) {es} {n}. Member es e n
    => Union es -- scrutinee
    -> (e -> r) -- success cont
    -> (Void# -> r) -- failure cont
    -> r

Proposal

Allow something like:

pattern U
  ::  forall (e :: Type) {es} {n}. Member es e n
  => e -> Union es
        | Union (Delete n es) -- The residual type
pattern U via uMatch -- directly supplying the matcher
  where U @e x = uInject @e x

This lets you

1. Supply a "residual" type, which is going to be used for subsequent cases
2. Supply the matcher function directly

The "residual" takes the place of Void# in the failure continuation in the matcher function.

foo :: Union '[Int, Bool, Char] -> String
foo x = case x of
  U @Int  n -> show n
  U @Bool b -> show b
  U @Char c -> show c

desugaring to

foo = uMatch @Int show (uMatch @Bool show (uMatch @Char show (\case{})))

and we recover exhaustiveness checking via the regular pattern match checker, which warns if the residual (Union '[]) is still inhabited when we get to \case {}

questions

This is very (maybe too) general, allowing you to supply basically anything as the "residual".

For example, you can do very weird things

pattern Foo :: Int -> Int | Bool
pattern Foo via (\ks kf x -> if even x then ks x else kf False)

foo :: Int
foo = case 1 of
  Foo i -> i*10
  True -> 100
  False -> 200

maybe we want to restrict the shape of the residual type, not sure how though.