不连贯的实例选择了错误的实例

Question

当我在构造函数中使用符号创建新类型时，打开了 IncoherentInstances，只有在编译时填写符号时，才会选择该类型的正确实例......

{-# LANGUAGE DataKinds, GADTs, KindSignatures, FlexibleInstances, IncoherentInstances #-}
import GHC.TypeLits
data Object:: Symbol -> * where
    Object :: Object sy
instance Show (Object "dog") where
    show _ = "dog"
instance Show (Object x) where
    show _ = "other"
main = do
    let name = "dog"
    print (undefined :: Object "dog") -- outputs "dog", as expected
    print (undefined :: Object "cat") -- outputs "other", as expected
    print (undefined :: Object name) -- outputs "other", I expected "dog"

有没有办法在运行时提供字符串符号值？ 如果不允许这样做，为什么它甚至会编译（即 - 如果它没有解析为默认情况之外的任何内容，那么什么时候有人甚至想在第三次打印中使用作业？

Answer 1

Haskell[GHC]有两个[三个]完全独立的命名空间：术语和类型[和种类]。这就是为什么你总是看到这种事情：

data Foo a = Foo a | Bar Int

它声明（除其他事项外）两个单独的名称Foo;一个是类型级名称Foo它是类型构造函数，另一个是术语级名称Foo它是数据构造函数。同样，在

foo :: a -> a
foo a = a

有两个单独的名称a：一个是类型级名称a它是类型变量，另一个是术语级名称a术语变量。

这两个级别之间的唯一交互是键入判断：一个级别的名称可能在上一个级别中具有已知的分类。例如，术语级别的名称Just按类型a -> Maybe a类型级别分类;但是，即使在这里，名称也不会相互作用。如果要连接术语级名称和类型级名称，则必须执行一些非常奇特的技巧。

所以当你写let name = "dog" in undefined :: Object name时，你应该把它读成let TermLevel.name = "dog" in undefined :: Object TypeLevel.name;那么很明显，let没有帮助，你不妨写undefined :: forall name. Object name。由于有许多实例与此类型匹配，并且您告诉GHC您不在乎在这种情况下选择哪个实例，因此它继续选择一个实例。这不是你想要的，但这是你为不连贯的实例付出的代价。