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

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)) ()

请注意，在 foo' 的正文中我们仍然只要求我们在 foo 中所做的事情: 一个 Eq (t a a)约束。此外，我们没有删除或修改编译器用于详细说明 Eq (t a a) 实例的约束。在 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

这不是一个真正的错误。 it's expected .在 foo 的定义中, 上下文有

forall x y. (Eq x, Eq y) => Eq (t x y) (即 Eq2 t )

Eq a

SomeClass t

forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => ob (t x y) (来自“关闭父类(super class)关系”SomeClass t)

我们要 Eq (t a a) .好吧，从上下文来看，有两个公理的头部匹配: (1) 与 x ~ a, y ~ a和 (2) 与 ob ~ Eq, x ~ a, y ~ a .有疑问； GHC 拒绝。 (请注意，由于 SomeConstraint t ~ ob 仅在 (4) 的假设中，它被完全忽略；选择实例只关注实例头。)
明显的前进方法是从 SomeClass 的父类(super class)中删除 (4) .如何？从实际实例“头”中拆分量化:

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... 形式的约束。 ，它没有父类(super class)，所以 GHC 不会向上搜索并找到全能的 forall ob x y. ob (t x y)毁掉一切的脑袋。现在唯一能够放电的实例 Eq (t a a)是(1)，所以我们使用它。
GHC 在绝对需要时会搜索新 (4) 的“父类(super class)”；用户指南实际上使此功能成为上述基本规则的扩展，这些基本规则来自原始论文。也就是说， forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => ob (t x y)仍然可用，但在上下文中的所有“真实”父类(super class)之后都会考虑它(因为它实际上不是任何东西的父类(super class))。

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 目前是保守的，出于性能、简单性和可预测性的原因而只是放弃而不是回溯。