1

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

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

如果我打开UndecidableInstances，则 GHC 无法将变量与 kind 统一起来Nat。

如果我进一步打开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但是，我从来没有peelA在定义中使用由 PeelableAnnPeelableAST Literal ann定义的，我希望这个实例作为默认行为并且能够通过直接提供一个PeelableAST (Predicate n) ann实例来覆盖它。换句话说，剥离可能本质上是上下文相关的。

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

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

4

1 回答 1

3

在您的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，但UndecidableInstances仍然需要，因为PeelableAnn PredicateAnn ann在结构上显然不小于PeelableAST Literal ann.

于 2018-08-17T14:45:11.067 回答