添加约束会导致其他约束超出范围吗？

Question

考虑以下代码，它进行类型检查：

module Scratch where

import GHC.Exts

ensure :: forall c x. c => x -> x
ensure = id

type Eq2 t = (forall x y. (Eq x, Eq y) => Eq (t x y) :: Constraint)

foo :: forall t a.
  ( Eq2 t
  , Eq a
  ) => ()
foo = ensure @(Eq (a `t` a)) ()

foo在这里没有做任何有用的事情，但让我们想象一下它正在做一些需要Eq (t a a)实例的重要业务。编译器能够接受(Eq2 t, Eq a)约束并详细说明Eq (t a a)字典，因此解除约束并且一切正常。

现在假设我们想要foo做一些额外的工作，这取决于以下相当复杂的类的实例：

-- some class
class (forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => ob (t x y)) =>
  SomeClass t
  where
  type SomeConstraint t :: * -> Constraint

foo' :: forall t a.
  ( Eq2 t
  , Eq a
  , SomeClass t -- <- the extra constraint
  ) => ()
foo' = ensure @(Eq (a `t` a)) ()

请注意，在 body 中，foo'我们仍然只要求我们所做的foo：Eq (t a a)约束。此外，我们还没有删除或修改编译器用来阐述Eq (t a a)in实例的约束foo；我们仍然要求(Eq2 t, Eq a)除了新的约束。所以我也希望foo'进行类型检查。

不幸的是，看起来实际发生的事情是编译器忘记了如何详细说明Eq (t a a). 这是我们在正文中得到的错误foo'：

    • Could not deduce (Eq (t a a)) arising from a use of ‘ensure’
      from the context: (Eq2 t, Eq a, SomeClass t)
        bound by the type signature for:
                   foo' :: forall (t :: * -> * -> *) a.
                           (Eq2 t, Eq a, SomeClass t) =>
                           ()

鉴于编译器可以“Eq (t a a)从上下文(Eq2 t, Eq a)” “推断”得很好，我不明白为什么更丰富的上下文(Eq2 t, Eq a, SomeClass t)会导致Eq (t a a)变得不可用。

这是一个错误，还是我只是做错了什么？在这两种情况下，是否有一些解决方法？

Answer 1

这不是一个真正的错误；这是预期的。在 的定义中foo，上下文有

1. forall x y. (Eq x, Eq y) => Eq (t x y)（即Eq2 t）
2. Eq a
3. SomeClass t
4. forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => ob (t x y)（来自“关闭超类关系” SomeClass t）

我们要Eq (t a a)。好吧，从上下文来看，有两个公理的头部匹配：（1）与x ~ a, y ~ a（2）与ob ~ Eq, x ~ a, y ~ a。有疑问；GHC 拒绝。（请注意，由于SomeConstraint t ~ ob仅在（4）的假设中，它被完全忽略；选择实例只关注实例头。）

显而易见的方法是从 的超类中删除 (4) SomeClass。如何？从实际实例“头部”拆分量化：

class ob (t x y) => SomeClassSuper ob t x y where
instance ob (t x y) => SomeClassSuper ob t x y where
class (forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => SomeClassSuper ob t x y) => SomeClass t where
  type SomeConstraint t :: * -> Constraint

这就是你的forall ob. _ => forall x y. _ => _技巧基本上所做的，除了这不依赖于错误（你的语法是不允许的）。现在，（4）变成forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => SomeClassSuper ob t x y。因为这实际上不是表单的约束Class args...，它没有超类，所以GHC不会向上搜索并找到forall ob x y. ob (t x y)破坏一切的全能头。现在唯一能够放电的实例Eq (t a a)是 (1)，所以我们使用它。

GHC确实在绝对需要时搜索 new (4) 的“超类”；用户指南实际上将此功能作为上述基本规则的扩展，这些规则来自原始论文。也就是说，forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => ob (t x y)仍然可用，但在上下文中的所有“真实”超类之后才考虑它（因为它实际上不是任何东西的超类）。

import Data.Kind

ensure :: forall c x. c => ()
ensure = ()

type Eq2 t = (forall x y. (Eq x, Eq y) => Eq (t x y) :: Constraint)

-- fine
foo :: forall t a. (Eq2 t, Eq a) => ()
foo = ensure @(Eq (t a a))

class ob (t x y) => SomeClassSuper ob t x y where
instance ob (t x y) => SomeClassSuper ob t x y where
class (forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => SomeClassSuper ob t x y) => SomeClass t where
  type SomeConstraint t :: * -> Constraint

-- also fine
bar :: forall t a. (Eq2 t, Eq a, SomeClass t) => ()
bar = ensure @(Eq (t a a))

-- also also fine
qux :: forall t a. (Eq2 t, Eq a, SomeConstraint t a, SomeClass t) => ()
qux = ensure @(SomeConstraint t (t a a))

您可能会争辩说，根据开放世界政策，GHC应该在面对“不连贯”（例如 (1) 和原始 (4) 之间的重叠）时回溯，因为量化的约束可以制造“不连贯”，同时存在没有实际的不连贯性，我们希望您的代码“正常工作”。这是一个完全有效的需求，但 GHC 目前是保守的，出于性能、简单性和可预测性的原因，它只是放弃而不是回溯。