如果您的程序真的对您来说似乎是有效的，那么您将能够编写 get 的类型，在 Haskell 中完成您想要的工作，而不是在 handwave 中。让我帮你提高你的手波水平，揭开你在棍子上要月亮的原因。
我要表达的是：get :: (Convert a_contained_by_D b) => D -> b，这似乎是不可能的。
如上所述，这并不像您需要的那样精确。事实上，这就是 Haskell 现在为您提供的，在那个
get :: (Convert A b, Convert B b, Convert C b) => D -> b
需要D 包含的任何a，一次一个，才能转换为b。这就是为什么您要获得经典的系统管理员逻辑：不允许获得 D，除非他们都可以获得 b。
问题是您需要知道的状态不是可能包含在 any 旧 D 中的类型，而是您收到的特定 D 中包含的类型输入。正确的？你想要的
print (get (DB B) :: A) -- this to work
print (get (DC C) :: A) -- this to fail
但是DB B 和DC C 只是D 的两个不同元素，并且就Haskell 类型系统而言，在每种类型中所有不同之处都是相同的。如果要区分D 的元素，则需要D-pendent 类型。这是我在 handwave 中的写法。
DInner :: D -> *
DInner (DA a) = A
DInner (DB b) = B
DInner (DC c) = C
get :: forall x. pi (d :: D) -> (Convert (DInner d) x) => x
get (DA x) = convert x
get (DB x) = convert x
get (DC x) = convert x
其中pi 是在运行时传递的数据的绑定形式（与forall 不同），但取决于哪些类型（与-> 不同）。现在约束不是在谈论任意的Ds，而是在你手中的非常d :: D，并且约束可以通过检查其DInner来准确计算所需的内容。
除了我的pi之外，没有什么可以让它消失的。
遗憾的是，虽然pi 正在迅速从天而降，但它还没有降落。尽管如此，与月亮不同，它可以用一根棍子到达。毫无疑问，您会抱怨我正在更改设置，但实际上我只是将您的程序从大约 2017 年的 Haskell 翻译到 2015 年的 Haskell。您将在某一天将 get 用我挥手的那种类型返回。
你无话可说，但你可以唱歌。
第 1 步。打开 DataKinds 和 KindSignatures 并为您的类型构建单例（或让 Richard Eisenberg 为您完成）。
data A = A deriving Show
data Aey :: A -> * where -- think of "-ey" as an adjectival suffix
Aey :: Aey 'A -- as in "tomatoey"
data B = B deriving Show
data Bey :: B -> * where
Bey :: Bey 'B
data C = C deriving Show
data Cey :: C -> * where
Cey :: Cey 'C
data D = DA A | DB B | DC C deriving Show
data Dey :: D -> * where
DAey :: Aey a -> Dey (DA a)
DBey :: Bey b -> Dey (DB b)
DCey :: Cey c -> Dey (DC c)
这个想法是（i）数据类型变成种类，以及（ii）单例表征具有运行时表示的类型级数据。所以类型级别 DA a 存在于运行时，前提是 a 存在，等等。
第 2 步。猜猜谁来DInner。开启TypeFamilies。
type family DInner (d :: D) :: * where
DInner (DA a) = A
DInner (DB b) = B
DInner (DC c) = C
第 3 步。给你一些RankNTypes，现在你可以写了
get :: forall x. forall d. Dey d -> (Convert (DInner d) x) => x
-- ^^^^^^^^^^^^^^^^^^
-- this is a plausible fake of pi (d :: D) ->
第 4 步。尝试写 get 并搞砸。我们必须匹配类型级别d 是可表示的运行时证据。我们需要它来获得专门用于计算DInner 的类型级别d。如果我们有正确的pi，我们可以匹配一个具有双重职责的D 值，但现在，改为匹配Dey d。
get (DAey x) = convert x -- have x :: Aey a, need x :: A
get (DBey x) = convert x -- and so on
get (DCey x) = convert x -- and so forth
令人发指的是，我们的xes 现在是单例，对于convert，我们需要基础数据。我们需要更多的单例设备。
第 5 步。引入并实例化单例类，以“降级”类型级别的值（只要我们知道它们的运行时代表）。同样，Richard Eisenberg 的 singletons 库可以从 Template-Haskell 中提取样板，但让我们看看发生了什么
class Sing (s :: k -> *) where -- s is the singleton family for some k
type Sung s :: * -- Sung s is the type-level version of k
sung :: s x -> Sung s -- sung is the demotion function
instance Sing Aey where
type Sung Aey = A
sung Aey = A
instance Sing Bey where
type Sung Bey = B
sung Bey = B
instance Sing Cey where
type Sung Cey = C
sung Cey = C
instance Sing Dey where
type Sung Dey = D
sung (DAey aey) = DA (sung aey)
sung (DBey bey) = DB (sung bey)
sung (DCey cey) = DC (sung cey)
第 6 步。做吧。
get :: forall x. forall d. Dey d -> (Convert (DInner d) x) => x
get (DAey x) = convert (sung x)
get (DBey x) = convert (sung x)
get (DCey x) = convert (sung x)
请放心，当我们有正确的pi 时，那些DAeys 将是实际的DAs，而那些xs 将不再需要是sung。我的get 的handwave 类型将是Haskell，而get 的代码会很好。但与此同时
main = do
print (get (DCey Cey) :: B)
print (get (DBey Bey) :: A)
类型检查就好了。也就是说，您的程序（加上 DInner 和 get 的正确类型）看起来像是有效的 Dependent Haskell，我们快到了。