haskell - 星型单例中的平等

Question

我在 ghci 中做了:

> :set -XTypeOperators

> import Data.Proxy
> import Data.Type.Equality
> import Data.Singletons.Prelude

> :let p1 = Proxy :: Proxy (Int == Int)
> :let p2 = Proxy :: Proxy (Int :== Int)

> :t p1
p1 :: Proxy 'True
> :t p2
p2 :: Proxy (Int :== Int)

为什么在第二种情况下类型没有被计算？我可以以某种方式解决它吗？我可以为类 PEq 创建一个实例(其中定义了 :==)吗？

(ghc 7.10.3)

更新:我找到了如何制作实例。是否有一些原因导致它没有被包含在内？

> instance PEq ('KProxy :: KProxy *) where { type (:==) x y = x == y }

或简单(如评论中 dfeuer 所指出)

> instance PEq ('KProxy :: KProxy *)

或从 TypeRepStar 导入此实例:

> import Data.Singletons.TypeRepStar()

Answer 1

似乎不包含 singletons 中种类 * 的 PEq 实例的原因类似于不包含base 中的 Eq。描述here 。这样的例子太常见了，如果存在的话我们无法描述。类型参数与类型函数的结果相等。例如:

Succ n == Succ m = n == m

对于单例情况下的解决方法，可以定义它:

instance PEq ('KProxy :: KProxy *)

或者直接使用它:

import Data.Singletons.TypeRepStar()