How to differentiate GADT constructors with different phantom types?

Question

I'm working on a system (inspired by lsp-types) that uses GADTs tagged with type information to represent the different types of messages exchanged by a client and server:

{-# LANGUAGE GADTs, DataKinds, KindSignatures, RankNTypes #-}

data From = FromClient | FromServer
data MessageType = Request | Notification

data Message (from :: From) (typ :: MessageType) where
  Request1 :: Message FromClient Request
  Request2 :: Message FromClient Request
  Request3 :: Message FromServer Request
  Notification1 :: Message FromClient Notification

My question is, given a list of these constructors (in an existential wrapper), how can I select a subset of them that have a certain type?

data SomeMessage where
  SomeMessage :: forall f t. Message f t -> SomeMessage

allMessages = [SomeMessage Request1
              , SomeMessage Request2
              , SomeMessage Request3
              , SomeMessage Notification1]

-- Desired output: [SomeMessage Request1, SomeMessage Request2, SomeMessage Request3]
filterToRequests :: [SomeMessage] -> [SomeMessage]
filterToRequests allMessages = undefined 

-- Desired output: [SomeMessage Request1, SomeMessage Request2]
filterToClientRequests :: [SomeMessage] -> [SomeMessage]
filterToClientRequests allMessages = undefined

Answer 1

You should be able to do this just using cast from Data.Typeable. In particular, if you have:

data SomeMessage where
  SomeMessage :: forall f t. (Typeable f, Typeable t) => Message f t -> SomeMessage

data SomeMessageRequest where
  SomeMessageRequest :: forall f. Message f Request -> SomeMessageRequest

(noting the Typeable dictionaries in SomeMessage), you can use scoped type variables and type applications to write:

maybeRequest :: SomeMessage -> Maybe SomeMessageRequest
maybeRequest (SomeMessage (msg :: Message f t))
  = SomeMessageRequest <$> cast @_ @(Message f Request) msg

to get:

allRequests :: [SomeMessageRequest]
allRequests = catMaybes $ map maybeRequest allMessages

Full code:

{-# LANGUAGE GADTs, DataKinds, KindSignatures, RankNTypes, ScopedTypeVariables, TypeApplications #-}

import Data.Typeable
import Data.Maybe

data From = FromClient | FromServer
data MessageType = Request | Notification

data Message (from :: From) (typ :: MessageType) where
  Request1 :: Message FromClient Request
  Request2 :: Message FromClient Request
  Request3 :: Message FromServer Request
  Notification1 :: Message FromClient Notification

data SomeMessage where
  SomeMessage :: forall f t. (Typeable f, Typeable t) => Message f t -> SomeMessage

data SomeMessageRequest where
  SomeMessageRequest :: forall f. Message f Request -> SomeMessageRequest

allMessages = [ SomeMessage Request1
              , SomeMessage Request2
              , SomeMessage Request3
              , SomeMessage Notification1]

maybeRequest :: SomeMessage -> Maybe SomeMessageRequest
maybeRequest (SomeMessage (msg :: Message f t))
  = SomeMessageRequest <$> cast @_ @(Message f Request) msg

allRequests :: [SomeMessageRequest]
allRequests = catMaybes $ map maybeRequest allMessages