在Haskell中检测冗余约束？
有没有办法检测 Haskell 中的冗余约束？
例如：
class (A a, B a) => C1 a -- C1 ~ A AND B
instance (A a, B a) => C1 a
class (A a, B a, C a) => C2 a
instance (A a, B a, C a) => C2 a
f :: (C1 a, C2 a) => a
f = ...
这里，C2 暗指C1，并且在签名中使用C1f是多余的，即重言式。
在现实世界的元编程的情况下，这将是waaaay更加复杂，并会显著帮助去杂波签名头，以及帮助我了解和跟踪是怎么回事的。
鉴于 GHC 的形式主义，这在逻辑上是否可行？
GHC 内的基础设施是否可用？
回答
如果我把你的存根放在一个文件中：
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
class A a
class B a
class C a
class (A a, B a) => C1 a -- C1 ~ A AND B
instance (A a, B a) => C1 a
class (A a, B a, C a) => C2 a
instance (A a, B a, C a) => C2 a
然后，您可以通过将变量绑定到undefined您想在 ghci 中减少的类型来了解冗余约束：
> x = undefined :: (C1 a, C2 a) => a
<interactive>:1:18: warning: [-Wsimplifiable-class-constraints]
• The constraint ‘C1 a’ matches
instance forall a. (A a, B a) => C1 a -- Defined at test.hs:8:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In an expression type signature: (C1 a, C2 a) => a
In the expression: undefined :: (C1 a, C2 a) => a
In an equation for ‘x’: x = undefined :: (C1 a, C2 a) => a
<interactive>:1:18: warning: [-Wsimplifiable-class-constraints]
• The constraint ‘C2 a’ matches
instance forall a. (A a, B a, C a) => C2 a
-- Defined at test.hs:11:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In an expression type signature: (C1 a, C2 a) => a
In the expression: undefined :: (C1 a, C2 a) => a
In an equation for ‘x’: x = undefined :: (C1 a, C2 a) => a
*Main
> :t x
x :: forall {a}. (A a, B a, C a) => a
这种情况下的前两个警告实际上只是一个愉快的意外，与您的存根有多简单有关；你不会总是得到它们。真正有趣的一点是第二个查询 ，:t x它减少了对您需要了解的基本事实的限制a。