如何区分具有不同幻像类型的 GADT 构造函数？

Question

我正在开发一个系统（受lsp-types启发），该系统使用标记有类型信息的 GADT 来表示客户端和服务器交换的不同类型的消息：

{-# 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

我的问题是，给定这些构造函数的列表（在存在性包装器中），我如何选择具有特定类型的它们的子集？

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