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

Question

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

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE StandaloneDeriving #-}

import Prelude 

data App = forall t. Eq t => App { f :: t }

deriving instance Eq App  

键入检查吠叫：

无法将预期类型“b”与实际类型“b1”匹配“b1”是 a 刚性类型变量受

约束

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

我发现可能相关的 GHC

问题，但禁用 PolyKinds 扩展没有任何效果，Polysemy 插件也没有。

使用GHC 9.2.5。

附注

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

Answer 1

这不是 GHC bug：首先就没有一个合理的

(==) :: App -> App -> Bool

 定义。

给定

a :: App

 和 

b :: App

，我们知道对于某些 

a = App x

（某种类型的 

x

 与 

X

），它们一定是 

Eq X

（不考虑底部），对于某些 

b = App y

（的某种类型 

y

 与 

Y

）。但是因为您定义了 

Eq Y

 存在，所以 

App

 和 

x

 绝对没有理由具有可比性，因为它们具有不同的类型。 

在

每种类型 

y 和 X

 中，您可以使用 

Y

 方法。所以 

Eq

 有意义，

x == x

 也有意义，但是 

y == y

 没有意义，因为您将在 

x == y

 类型中使用 

(==)

。因此暂定定义

X -> Y -> Bool

被认为是废话，不管它是由

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

生成的还是手写的。从本质上讲，您遇到的类型错误只是“您试图在可能不同类型的对象上使用

deriving

。”

或者，简而言之，表达式 

(==)

到底应该如何计算？

如果不同类型的对象总是比较不相等，也许您会喜欢它。然后您需要使用 

App (5 :: Int) == App ("5" :: String)

或

App

 将类型信息存储在 

Typeable

 中。您首先比较类型相等性，只有得到“是”后才能比较值。

TypeRep