Sigma 中的限制类型

Question

我已经按种类X索引了S几个适用于X. 例如，f转换X S1为X S2（但X S1在这个简化的示例中不使用）。

{-# LANGUAGE DataKinds, GADTs, TemplateHaskell, TypeFamilies #-}

import Data.Singletons
import Data.Singletons.Sigma
import Data.Singletons.TH

singletons [d|
    data S = S1 | S2 | S3 | S4
  |]

data X (s :: S) = X

f :: X S1 -> X S2
f x = X

现在我想定义可能返回X S2或X S3取决于其参数的函数。直接的方法是使用Either.

g1 :: Bool -> X S1 -> Either (X S2) (X S3)
g1 True x = Left X
g1 False x = Right X

但我不想采用这种方法，因为Either当函数返回更多类型时，我需要嵌套s。

另一种方法是这样使用Sigma。

g2 :: Bool -> X S1 -> Sigma S (TyCon X)
g2 True x = SS2 :&: X
g2 False x = SS3 :&: X

但这并没有表达g2只返回X S2or的想法X S3。我可以通过引入一个包装器来表达这个想法X。

data Y (s :: S) where
    Y2 :: X S2 -> Y S2
    Y3 :: X S3 -> Y S3

singletons [d|
    type Z s = Y s
  |]

g3 :: Bool -> X S1 -> Sigma S ZSym0
g3 True x = SS2 :&: Y2 X
g3 False x = SS3 :&: Y3 X

但是为每个组合定义这些包装器并在调用者站点上打开它们是很麻烦的。如果我可以使用g2方法直接限制类型会很好，例如，通过应用类型约束，但我不确定我该怎么做。

如何使用g2方法直接限制类型？

我将 GHC 8.8.4 与singletons-2.6 一起使用。