意外的重叠实例错误

Question

我有以下代码。 Class1 实例说明一个类的直接超类是什么，SuperClass1 自动遍历 Class1 以查找所有超类。 （我省略了这些类的实际方法，因为它们与我的问题无关。）

{-# LANGUAGE PolyKinds, RankNTypes, ConstraintKinds, FlexibleInstances, UndecidableInstances, MultiParamTypeClasses, FunctionalDependencies #-}

class Class1 b h | h -> b
instance Class1 Functor Applicative
instance Class1 Applicative Monad

class SuperClass1 b h
instance {-# OVERLAPPING #-} SuperClass1 b b
instance {-# OVERLAPPABLE #-} (SuperClass1 b c, Class1 c h) => SuperClass1 b h

这很好用！现在我想这样使用它：

newtype HFree c f a = HFree { runHFree :: forall g. c g => (forall b. f b -> g b) -> g a }

instance SuperClass1 Functor c => Functor (HFree c f)
instance SuperClass1 Applicative c => Applicative (HFree c f)
instance SuperClass1 Monad c => Monad (HFree c f)

test :: (a -> b) -> HFree Monad f a -> HFree Monad f b
test = fmap

（即，只要Functor 是c 的超类，我就可以为Hfree c f 提供Functor 的实例。）

这会在 Applicative 实例中产生此错误（对于 Monad 实例也是如此）：

• Overlapping instances for SuperClass1 Functor c1
    arising from the superclasses of an instance declaration
  Matching instances:
    instance [overlappable] forall k k k (b :: k) (c :: k) (h :: k).
                            (SuperClass1 b c, Class1 c h) =>
                            SuperClass1 b h
      -- Defined at superclass.hs:17:31
    instance [overlapping] forall k (b :: k). SuperClass1 b b
      -- Defined at superclass.hs:16:30
  (The choice depends on the instantiation of ‘c1, k1’
   To pick the first instance above, use IncoherentInstances
   when compiling the other instance declarations)
• In the instance declaration for ‘Applicative (HFree c f)’

据我了解，Applicative 实例需要 Functor 实例，因此 Applicative 实例还需要来自 Functor 的 SuperClass1 Functor c 约束。事实上，如果我添加这个，错误就会消失。 （这是我目前拥有的：http://hackage.haskell.org/package/free-functors-0.7/docs/Data-Functor-HFree.html）

但不知何故，GHC 足够聪明，可以理解SuperClass1 Applicative c 隐含SuperClass1 Functor c，因为它不会抱怨缺少约束。相反，它会卡在重叠实例错误上。如果有办法修复错误，那就太好了，但我不知道如何解决！

Answer 1

但不知何故，GHC 足够聪明，可以理解SuperClass1 Applicative c 隐含SuperClass1 Functor c，因为它不会抱怨缺少约束。

我担心你太有希望了 - GHC 可能正在从另一端开始工作并立即放弃：它看到fmap 并尝试检查HFree 是否是Functor。它只有一个实例可供选择：SuperClass1 Functor c => Functor (HFree c f)。然后，它开始尝试满足对该实例 (SuperClass1 Functor c) 的约束并突然意识到它不知道该做什么——它可以选择两个实例：

• SuperClass1 b b
• SuperClass1 b h

请注意，我忽略了这些实例的约束 - 这是因为 GHC 需要在查看左侧的约束之前提交到实例。话虽如此，@user2407038 的评论是非常正确的：您的实例重叠非常严重 - GHC 不知道是否应该尝试统一 b ~ Functor 和 b ~ c 或 b ~ Functor 和 h ~ c。两者都可以。

如果选择任一都可以，您应该打开IncoherentInstances。不幸的是，这里不是这种情况。你知道你想要选择第二个实例，但 GHC 没有。

---

我最近一直在toying around with a similar sort of problem but in relation to subtyping，但不管你怎么做，实例解析真的很难。我对你的建议是尽可能使用类型族。

编辑

这是一个让您的代码编译的解决方案，除了依赖类型族而不是类型类。设置机制是

{-# LANGUAGE PolyKinds, ConstraintKinds, TypeFamilies, UndecidableInstances, DataKinds, TypeOperators #-}

import Data.Kind (Constraint)

-- Find transitively all the superclasses of a constraint (including itself)
type family SuperClasses (x :: k -> Constraint) :: [k -> Constraint]
type instance SuperClasses Functor = '[Functor]
type instance SuperClasses Applicative = Applicative ': SuperClasses Functor
type instance SuperClasses Monad = Monad ': SuperClasses Applicative

-- Type level version of `elem` which is a Constraint
type family Elem (x :: k) (xs :: [k]) :: Constraint where
  Elem a (a ': bs) = ()
  Elem a (b ': bs) = Elem a bs

-- Type level version of checking the first list is a subset of the second
type family Subset (xs :: [k]) (ys :: [k]) :: Constraint where
  Subset '[] bs = ()
  Subset (a ': as) bs = (Elem a bs, Subset as bs)

-- Tell us whether the constraint x is a sub-constraint (thereby implied by) y
type x <: y = SuperClasses x `Subset` SuperClasses y

那么，应用于Functor、Applicative和Monad，我们需要

-- I've cropped the body of HFree since it is of no interest here
data HFree c f a

instance Functor     <: c => Functor     (HFree c f)
instance Applicative <: c => Applicative (HFree c f)
instance Monad       <: c  => Monad      (HFree c f)

这里有一些测试

-- Compiles
test1 :: (a -> b) -> HFree Monad f a -> HFree Monad f b
test1 = fmap

-- Compiles
test2 :: a -> HFree Monad f a
test2 = pure

-- Doesn't compile
test3 :: a -> HFree Functor f a
test3 = pure