为什么在具有存在量化的记录上使用严格类型进行独立推导会失败？

Question

我试图将关联类型与存在类型进行比较，并编写了以下片段：

\n

{-# LANGUAGE FlexibleContexts #-}\n{-# LANGUAGE ExistentialQuantification #-}\n{-# LANGUAGE StandaloneDeriving #-}\n\nimport Prelude \n\ndata App = forall t. Eq t => App { f :: t }\n\nderiving instance Eq App  \n

\n

类型检查吠叫：

\n

\n

无法将预期类型 \xe2\x80\x98b\xe2\x80\x99 与实际类型 \xe2\x80\x98b1\xe2\x80\x99 \xe2\x80\x98b1\xe2\x80\x99 匹配\n刚性类型变量绑定

\n

\n

乍一看，相同的代码片段是作为早期堆栈溢出的解决方案提供的。

\n

我发现可能相关的 GHC问题，但禁用 PolyKinds 扩展没有任何效果，Polysemy 插件也没有。

\n

使用 GHC 9.2.5。

\n

聚苯乙烯

\n

因此在实践中这两种方法都不支持推导。

\n

Answer 1

这不是 GHC 错误：首先就没有一个合理的定义(==) :: App -> App -> Bool。

给定a :: App和，我们知道对于某些（具有的某种类型）和某些（具有的某种类型）b :: App它们一定是（不考虑底部）。但是因为您是存在性地定义的，所以绝对没有理由进行比较，因为它们有不同的类型。在每种类型和中，您都可以使用这些方法。所以有道理， 也有道理，但没有意义，因为你会使用at 类型。因此暂定定义a = App xxXEq Xb = App yyYEq YAppxyXYEqx == xy == yx == y(==)X -> Y -> Bool

instance Eq App where App x == App y = x == y

被认为是无意义的，无论它是由生成的deriving还是手写的。从本质上讲，您遇到的类型错误只是“您试图(==)在可能不同类型的对象上使用”。

或者，简而言之，表达式到底应该如何App (5 :: Int) == App ("5" :: String)计算？

如果不同类型的对象总是比较不相等，也许您会喜欢它。然后您需要在AppusingTypeable或中存储类型信息TypeRep。首先比较类型相等性，只有得到“是”后才能比较值。

import Data.Typeable
data App = forall t. (Typeable t, Eq t) => App t
instance Eq App where
  App x == App y = case cast y of -- try to cast y to type of x (type information flows from (1))
    Just y' -> x == y' -- (1) x and y' are (==)'d, so they must be of the same type
    Nothing -> False