这两个实例如何重叠（涉及超出范围的类型）

Question

几天前，我 asked a question 关于在 free-monads 的上下文中注入函子。那里建议的解决方案基于Data Types à la Carte，使用一个表示函子之间的一种包含关系的类。

-- | Class that represents the relationship between a functor 'sup' containing
-- a functor 'sub'.
class (Functor sub, Functor sup) => sub :-<: sup where
    inj :: sub a -> sup a

-- | A functor contains itself.
instance Functor f => f :-<: f where
    inj = id

-- | A functor is contained in the sum of that functor with another.
instance (Functor f, Functor g) => f :-<: (Sum f g) where
    inj = InL

-- | If a functor 'f' is contained in a functor 'g', then f is contained in the
-- sum of a third functor, say 'h', with 'g'.
instance (Functor f, Functor g, Functor h, f :-<: g) => f :-<: (Sum h g) where
    inj = InR . inj

现在考虑以下数据类型：

type WeatherData = String

data WeatherServiceF a = Fetch (WeatherData -> a) deriving (Functor)

data StorageF a = Store WeatherData a deriving (Functor)

还有如下类型的函数

fetch :: (WeatherServiceF :-<: g) => Free g WeatherData

其中Free 来自Control.Monad.Free 模块。

那么如果我尝试使用这个功能如下：

reportWeather :: Free (Sum WeatherServiceF StorageF) ()
reportWeather = do
    _ <- fetch
    return ()

我得到一个重叠实例错误，说：

• Overlapping instances for WeatherServiceF
                            :-<: Sum WeatherServiceF StorageF
    arising from a use of ‘fetch’
  Matching instances:
    two instances involving out-of-scope types
      instance (Functor f, Functor g) => f :-<: Sum f g

      instance (Functor f, Functor g, Functor h, f :-<: g) =>
               f :-<: Sum h g

现在，我知道第一个是有效实例，但为什么第二个也被视为有效实例？如果我在第二种情况下实例化变量，我会得到 ​​p>

instance ( Functor WeatherServiceF
         , Functor StorageF
         , Functor WeatherServiceF
         , WeatherServiceF :-<: StorageF
         ) => WeatherServiceF :-<: Sum WeatherServiceF g

这不应该是一个实例，因为WeatherServiceF :-<: StorageF 不是真的。为什么 GHC 会推断出这样一个实例？

我启用了以下实例：

{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators         #-}

Answer 1

编译器必须能够通过仅考虑实例的“头部”来选择实例，而不需要查看约束。仅在选择了适用的实例后才考虑约束。如果它不能在两个只看头部的实例之间做出决定，那么它们就会重叠。

原因是不能保证最终完整程序中使用的所有实例都将导入到 this 模块中。如果编译器曾经基于无法看到一个实例满足另一个实例的约束而承诺选择一个实例，那么不同的模块可能会根据不同的选择对两个重叠实例中的哪一个用于同一类型做出不同的选择。每个实例都有一组可用的实例。

重叠检查旨在阻止这种情况发生。因此，它可以做到这一点的唯一方法是，当 GHC 在查看哪些实例可能适用于给定情况时，将所有约束视为至少潜在可满足。当只剩下一个候选人时，无论在程序的其他地方添加或删除了哪些其他实例，该候选人都将保留。然后它可以检查该模块中是否有必要的实例来满足约束。