7

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

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)约束。此外，我们没有删除或修改编译器用于详细说明 in 实例的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)不可用。

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

4

3 回答 3

5

这不是一个真正的错误。这是预期的。在 的定义中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) withx ~ a, y ~ a和 (2) with 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。因为这实际上不是 form 的约束Class args...，它没有超类，所以 GHC 不会向上搜索并找到forall ob x y. ob (t x y)破坏一切的全能头。现在唯一能够放电的实例Eq (t a a)是（1），所以我们使用它。

GHC在绝对需要时会搜索新 (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 目前是保守的，出于性能、简单性和可预测性的原因而放弃而不是回溯。

于 2020-07-20T15:49:52.350 回答
2

我认为您遇到了重叠公理的“如有疑问则拒绝”规则。当您将SomeClass t约束纳入范围时，您还引入了新的量化约束forall ob x y. (ob x, ob y) => ob (t x y)。到了 Discharge 时Eq (t a a)，GHC 不知道是使用's 签名中的量化约束还是类中的量化约束Eq2 t，因为两者都适用。（与往常一样，GHC在评估多态实例是否适用时不考虑。）没有机制可以检查后者是否可以“专门化”于前者。fooSomeClassSomeConstraint t ~ ob

如果您Eq2 t从以下位置删除约束foo：

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

那么你会得到一个错误“Couldn't match type SomeConstraint twith Eq”，这表明这正是 GHC 试图解决这个约束的方式。（如果您SomeConstraint t ~ ob从 中删除class，它甚至会进行类型检查！）

这并不能解决您的问题，但我认为它可以解释发生了什么。

于 2020-07-20T15:08:06.670 回答
0

编辑：这个变通办法原来是一种不可行的变通办法，因为它不能在 GHC 8.8.3 中编译。神秘的是，类似的现实世界程序在 GHC 8.6.5 中编译得很好，甚至通过了一系列测试，尽管成功编译是一个错误的结果。

我找到了一种解决方法，其中涉及“分解”我所依赖的附加类中的量化。因此，如果我进行以下更改：

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

它进行foo'类型检查。

我仍然不明白为什么这会使事情奏效，以及它是否以某种方式与我量化变量的方式相关foo'（在这种情况下，它并不是一个真正可行的解决方案）。

此外，在我看来，附加SomeClass约束foo'（无论如何SomeClass定义）会以某种方式导致编译器忘记如何Eq (t a a)从可用的Eq2 t和Eq a. 这种直觉不正确吗？

欢迎补充说明这两点的答案。

于 2020-07-20T09:25:55.040 回答