1

我Bar在类型类中有一个关联的类型族Foo。Foo'要求Bar f ~ Bar (f a)所有a，但在另一个函数中test我得到一个错误Couldn't match type 'Bar f' with 'Bar (f a)'，即使它取决于Foo' f. 编码：

{-# LANGUAGE TypeFamilies, PolyKinds, QuantifiedConstraints #-}

import Data.Proxy

class Foo f where
  type Bar f

class (Foo f, forall a. Foo (f a), forall a. Bar f ~ Bar (f a)) => Foo' f where

test :: Foo' f => Proxy (f a) -> Bar (f a) -> Bar f
test _ = id

为什么 GHC 不能弄清楚这种类型的相等性，有没有办法在不断言具体相等的情况下帮助类型检查器test？

4

1 回答 1

2

类型族和量化约束不混合。类型等式则更少。但是有一种方法可以将它们分开以达到或多或少相同的结果。

量化约束实际上在其使用方式上受到限制。仅知道约束适用于所有类型是不够的，您还需要一种方法来了解需要将其专门化到哪些类型。GHC 通过将量化约束表示为一种受实例解析通用规则约束的“本地实例”来实现这一点。我不确定量化类型等式是否意味着什么。总之，仅仅实例化一个量化的约束来做我们想做的事情是不够的；该实例化必须在实例解析的常规过程中发生，并且限制了量化约束的允许形式。

诀窍是为量化约束的主体定义一个类同义词：

class    (Bar f ~ Bar (f a)) => EBar f a
instance (Bar f ~ Bar (f a)) => EBar f a

这样我们就可以将量化约束重写为forall x. EBar f x，看不到类型族：

class (Foo f, forall a. Foo (f a), forall x. EBar f x) => Foo' f where

要使用这个类，我们需要一个显式函数来专门化量化约束（问题是，如果我们直接使用相等Bar f ~ Bar (f a)，类型检查器无法将其与量化约束相关联forall x. EBar f x，这看起来一点也不像）：

-- Morally a function on constraints `(forall x. EBar f x) => EBar f a`
-- in continuation-passing style: (x => y) is isomorphic to forall r. (y => r) -> (x => r)
ebar :: forall f a r. (EBar f a => Proxy (f a) -> r) -> (forall x. EBar f x) => Proxy (f a) -> r
ebar f = f

test :: Foo' f => Proxy (f a) -> Bar (f a) -> Bar f
test = ebar (\_ -> id)

{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FlexibleInstances, TypeFamilies, PolyKinds, QuantifiedConstraints #-}

import Data.Proxy

class Foo f where
  type Bar f

class (Foo f, forall a. Foo (f a), forall a. EBar f a) => Foo' f where

class    (Bar f ~ Bar (f a)) => EBar f a
instance (Bar f ~ Bar (f a)) => EBar f a

ebar :: forall f a r. (EBar f a => Proxy (f a) -> r) -> (forall x. EBar f x) => Proxy (f a) -> r
ebar f = f

test :: Foo' f => Proxy (f a) -> Bar (f a) -> Bar f
test = ebar (\_ -> id)
于 2020-07-15T16:04:52.850 回答