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

Question

几天前，我问了一个关于在自由单子背景下注入函子的问题。那里建议的解决方案基于数据类型 \xc3\xa0 la Carte使用一个表示函子之间某种包含关系的类。

\n\n

-- | Class that represents the relationship between a functor \'sup\' containing\n-- a functor \'sub\'.\nclass (Functor sub, Functor sup) => sub :-<: sup where\n    inj :: sub a -> sup a\n\n-- | A functor contains itself.\ninstance Functor f => f :-<: f where\n    inj = id\n\n-- | A functor is contained in the sum of that functor with another.\ninstance (Functor f, Functor g) => f :-<: (Sum f g) where\n    inj = InL\n\n-- | If a functor \'f\' is contained in a functor \'g\', then f is contained in the\n-- sum of a third functor, say \'h\', with \'g\'.\ninstance (Functor f, Functor g, Functor h, f :-<: g) => f :-<: (Sum h g) where\n    inj = InR . inj\n

\n\n

现在考虑以下数据类型：

\n\n

type WeatherData = String\n\ndata WeatherServiceF a = Fetch (WeatherData -> a) deriving (Functor)\n\ndata StorageF a = Store WeatherData a deriving (Functor)\n

\n\n

以及具有以下类型的函数

\n\n

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

\n\n

从哪里来Free的Control.Monad.Free模块。

\n\n

然后，如果我尝试按如下方式使用此函数：

\n\n

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

\n\n

我收到重叠实例错误，内容如下：

\n\n

\xe2\x80\xa2 Overlapping instances for WeatherServiceF\n                            :-<: Sum WeatherServiceF StorageF\n    arising from a use of \xe2\x80\x98fetch\xe2\x80\x99\n  Matching instances:\n    two instances involving out-of-scope types\n      instance (Functor f, Functor g) => f :-<: Sum f g\n\n      instance (Functor f, Functor g, Functor h, f :-<: g) =>\n               f :-<: Sum h g\n

\n\n

现在，我明白第一个是有效实例，但为什么第二个也被认为是有效实例？如果我在第二种情况下实例化变量，我会得到

\n\n

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

\n\n

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

\n\n

我启用了以下实例：

\n\n

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

\n

Answer 1

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

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

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