关联类型族的量化类型相等

Question

我在类型 class Foo 中有一个关联的类型族 Bar。 Foo' 要求对所有 a 使用 Bar f ~ Bar (f 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 中的具体相等性的情况下帮助类型检查器？

Answer 1

Type families and quantified constraints don't mix. 更不用说类型相等了。但是有一种方法可以将它们分开来实现或多或少相同的结果。

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

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

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

要使用这个 class，我们需要一个显式函数来专门化量化约束（问题是如果我们直接使用等式 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)

关联类型族的量化类型相等

Quantified type equality of associated type families

haskell

type-families

quantified-constraints