由于帕特森的条件，无法解析 Haskell 类型类约束

Question

我正在尝试使用索引嵌套注释构建AST。我添加了一个用于在顶层剥离注释的 typeclass，并尝试提供默认实例，该实例有效地表示"如果您知道如何自行剥离注释，那么您知道如何在特定 AST 节点剥离注释。

由于我的一个树节点是一个Nat索引谓词，并且它的父节点存在地量化了这个变量，当我尝试为父节点编写实例时，我陷入了帕特森的条件。也就是说，我的断言中的类型变量比我在头部中的类型变量多。

如果我打开UndecidableInstances，那么 GHC 无法将变量与 kindNat统一起来。

如果我进一步打开AllowAmbiguousTypes，那么我会收到一个更荒谬的错误，它说它找不到实例，尽管它正在寻找的实例在类型实例的断言中。

我的问题是：

1. 这实际上是一个不好写的实例，还是类型检查器太保守了？
2. 如果它不好或没有办法解决问题，我还能如何提供这种默认剥离行为？

这是最小的代码(我去除了对类型错误不重要的位，所以有些位可能看起来是多余的(：

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Constraint where
data AnnType = ABase
data family PredicateAnn (a :: AnnType)
data instance PredicateAnn (a :: AnnType) = PABase
data Nat = Zero | Succ Nat
data Predicate (n :: Nat) (a :: AnnType) = Predicate
data Literal   (a :: AnnType) = forall n. Literal (Predicate n a)
class PeelableAST (ast :: AnnType -> *) (ann :: AnnType -> AnnType) where
peel :: ast (ann a) -> ast a
class PeelableAnn (f :: AnnType -> *) (ann :: AnnType -> AnnType) where
peelA :: f (ann a) -> f a
instance PeelableAST (Predicate n) ann
=> PeelableAST Literal ann where
peel (Literal predicate) = Literal (peel predicate)
instance PeelableAnn PredicateAnn ann => PeelableAST (Predicate n) ann where
peel Predicate = Predicate

这是没有UndecidableInstances的确切错误：

src/Constraint.hs:27:10: error:
• Variable ‘n’ occurs more often
in the constraint ‘PeelableAST (Predicate n) ann’
than in the instance head
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘PeelableAST Literal ann’
|
27 | instance PeelableAST (Predicate n) ann
|          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

这是它的那个：

src/Constraint.hs:28:10: error:
• Could not deduce (PeelableAST (Predicate n0) ann)
from the context: PeelableAST (Predicate n) ann
bound by an instance declaration:
forall (n :: Nat) (ann :: AnnType -> AnnType).
PeelableAST (Predicate n) ann =>
PeelableAST Literal ann
at src/Constraint.hs:(28,10)-(29,35)
The type variable ‘n0’ is ambiguous
• In the ambiguity check for an instance declaration
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the instance declaration for ‘PeelableAST Literal ann’
|
28 | instance PeelableAST (Predicate n) ann
|          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

这是带有AllowAmbiguousTypes的那个：

src/Constraint.hs:31:39: error:
• Could not deduce (PeelableAnn PredicateAnn ann)
arising from a use of ‘peel’
from the context: PeelableAST (Predicate n) ann
bound by the instance declaration
at src/Constraint.hs:(29,10)-(30,35)
• In the first argument of ‘Literal’, namely ‘(peel predicate)’
In the expression: Literal (peel predicate)
In an equation for ‘peel’:
peel (Literal predicate) = Literal (peel predicate)
|
31 |   peel (Literal predicate) = Literal (peel predicate)
|                                       ^^^^^^^^^^^^^^

编辑：

正如丹尼尔·瓦格纳(Daniel Wagner(所建议的那样，一种解决方案是在这种情况下PeelableAnn PredicateAnn ann断言PeelableAST Literal ann。但是，我从不使用 PeelableAnn 定义的peelAPeelableAST Literal ann，我希望这个实例表现为默认行为，并能够通过直接提供一个PeelableAST (Predicate n) ann实例来覆盖它。换句话说，剥离可能本质上是上下文相关的。

既然PeelableAnn PredicateAnn ann是PeelableAST (Predicate n) ann的要求，我觉得GHC应该能够找到并满足这个条件。

我可以简单地有一个虚假的PeelableAnn PredicateAnn ann实例，只是被更具体的实例忽略，但这很笨拙

Answer 1

在PeelableAST Literal ann实例中，您可以使用PeelableAST (Predicate n) ann实例。如果类型检查器想要使用该实例，则必须验证其前提条件，即PeelableAnn PredicateAnn ann成立。但它不知道这一点，因为您尚未将其作为PeelableAST Literal ann实例的先决条件。

没关系;它很容易修复，并且可以完全避免模棱两可的类型。只需添加它担心的前提条件作为您PeelableAST Literal ann实例的前提条件。事实上，由于它现在是两个实例的前提条件，你也可以放弃PeelableAnn PredicateAnn ann前提条件，因为它是由这个新的和更强的条件所暗示的。所以：

instance PeelableAnn PredicateAnn ann => PeelableAST Literal ann where
peel (Literal predicate) = Literal (peel predicate)

然后你可以删除AllowAmbiguousTypes，尽管仍然需要UndecidableInstancesPeelableAnn PredicateAnn ann因为它在结构上并不明显小于PeelableAST Literal ann。