DataKinds 和类型类实例

下面的例子是我现实生活中问题的简化版本。它似乎在某种程度上类似于从 DataKinds 约束的存在类型中检索信息 https://stackoverflow.com/questions/24387865/retreiving-information-from-datakinds-constrained-existential-types，但我无法完全得到我正在寻找的答案。

假设我们有一个有限的、提升的 DataKindK有类型A and B，以及多类Proxy数据类型，生成类型为 * 的术语。

{-# LANGUAGE DataKinds, PolyKinds, GADTs, FlexibleInstances, FlexibleContexts #-}

data K = A | B

data Proxy :: k -> * where Proxy :: Proxy k

现在我想写Show-每种类型的实例Proxy a where a是善良的K，这恰好是两个：

instance Show (Proxy A) where show Proxy = "A"
instance Show (Proxy B) where show Proxy = "B"

但要使用Show-实例，我必须明确提供上下文，即使类型仅限于K:

test :: Show (Proxy a) => Proxy (a :: K) -> String
test p = show p

我的目标是摆脱类型类约束。这可能看起来不重要，但在我的实际应用中，这具有重大意义。

我也可以定义一个单一的，但更通用的Show-像这样的例子：

instance Show (Proxy (a :: K)) where show p = "?"

这实际上允许我放弃约束，但新的问题是区分这两种类型A and B.

那么，有没有办法既能吃到蛋糕，又能拥有它呢？也就是说，不必在类型中提供类型类约束test（不过，类型注释很好），并且仍然有两个不同的show实现（例如通过以某种方式区分类型）？

实际上，如果我可以简单地将各个类型关联起来，那么删除整个类型类也是可以的（A, B）及其具体值（此处："A", "B"）在我只有类型信息的上下文中。不过，我不知道该怎么做。

我将非常感谢您提供的任何见解。

不，这是不可能的。在运行时“只有类型信息”的上下文中，您确实拥有no信息。类型信息被删除。因此，即使对于封闭类型，原则上可以证明给定所讨论的类型，你总是可以想出一个字典，你仍然需要类约束。类约束确保在编译时，当 GHC 知道类型时，它可以选择适当的实例来传递。在运行时，它的类型信息会丢失，并且没有机会做同样的事情。编写一个“一刀切”的实例确实有效，因为这样确切的类型对于选择就不再重要了。

我不知道完整的情况，但是可以通过将类字典或字符串本身与您传递的值显式捆绑在一起来解决这个问题......