在之前使用UndecidableInstances编写一些代码时，我遇到了一些我觉得很奇怪的事情。我设法无意中创建了一些代码，当我认为不应该进行类型检查时：
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
data Foo = Foo
class ConvertFoo a b where
convertFoo :: a -> b
instance (ConvertFoo a Foo, ConvertFoo Foo b) => ConvertFoo a b where
convertFoo = convertFoo . (convertFoo :: a -> Foo)
evil :: Int -> String
evil = convertFoo
具体而言，convertFoo函数在给定任何输入时进行类型检查以生成任何输出，如evil函数所示。起初，我认为也许我设法意外地实现了unsafeCoerce，但这并不完全正确：实际上尝试调用我的convertFoo函数(例如，通过执行类似evil 3的事情)只是进入无限循环。
我有点模糊地理解发生了什么。我对这个问题的理解是这样的：
- 我定义的
ConvertFoo实例适用于任何输入和输出，a和b，仅受转换函数必须存在于a -> Foo和Foo -> b的两个附加约束的限制。 - 不知何故，该定义能够匹配任何输入和输出类型，因此似乎对
convertFoo :: a -> Foo的调用正在选择convertFoo本身的定义，因为它是唯一可用的定义。 - 由于
convertFoo无限调用自身，因此该函数进入一个永不终止的无限循环。 - 由于
convertFoo永远不会终止，因此该定义的类型是底部的，因此从技术上讲，不会违反任何类型，并且程序会进行类型检查。
现在，即使上述理解是正确的，我仍然对为什么整个程序进行类型检查感到困惑。具体来说，鉴于不存在此类实例，我预计ConvertFoo a Foo和ConvertFoo Foo b约束将失败。
我确实理解(至少模糊地)在选择实例时约束无关紧要 - 仅根据实例头选择实例，然后检查约束 - 所以我可以看到这些约束可能会很好地解决，因为我的ConvertFoo a b实例，它尽可能宽松。但是，这将需要解决相同的一组约束，我认为这会将类型检查器放入无限循环中，导致 GHC 要么挂起编译，要么给我一个堆栈溢出错误(后者我之前见过)。
不过，很明显，类型检查器不会循环，因为它愉快地触底并愉快地编译我的代码。为什么？在此特定示例中，实例上下文如何满足？为什么这不会给我一个类型错误或产生类型检查循环？
我全心全意地同意这是一个很好的问题。它说明了如何 我们对类型类的直觉与现实不同。
类型类惊喜
看看这里发生了什么，将提高赌注evil的类型签名：
data X
class Convert a b where
convert :: a -> b
instance (Convert a X, Convert X b) => Convert a b where
convert = convert . (convert :: a -> X)
evil :: a -> b
evil = convert
显然，正在选择Covert a b实例，因为只有 此类的一个实例。打字器在想类似的东西 这：
Convert a X是真的，如果...Convert a X为真[假设为真]Convert X X是真的Convert X X是真的，如果...Convert X X为真[假设为真]Convert X X为真[假设为真]
Convert X b是真的，如果...Convert X X是真的[从上面看是真的]Convert X b为真[假设为真]
打字器让我们感到惊讶。我们不希望Convert X X是真的，因为我们没有定义类似的东西。但(Convert X X, Convert X X) => Convert X X是一种重言式：它是 自动为 true，无论类中定义了什么方法，它都是 true。
这可能与我们的类型类的心智模型不匹配。我们期待 编译器在这一点上呆呆地抱怨如何Convert X X不能为真，因为我们没有为它定义任何实例。我们期待 编译器站在Convert X X，寻找另一个位置 走到Convert X X真实的地方，放弃，因为那里 没有其他地方是真的。但是编译器能够 递归！递归、循环和图灵完备。
我们赋予了打字器这个功能，我们做到了UndecidableInstances.当文档指出它是 可以将编译器发送到循环中，很容易假设 最糟糕的是，我们假设坏循环总是无限循环。但 在这里，我们演示了一个更致命的循环，一个循环终止- 除非以令人惊讶的方式。
(这在丹尼尔的评论中得到了更鲜明的证明：
class Loop a where
loop :: a
instance Loop a => Loop a where
loop = loop
.)
不可判定性的危险
这正是UndecidableInstances的情况 允许。如果我们关闭该扩展程序并打开FlexibleContexts(本质上只是句法的无害扩展)，我们得到一个 警告违反帕特森之一 条件：
...
Constraint is no smaller than the instance head
in the constraint: Convert a X
(Use UndecidableInstances to permit this)
In the instance declaration for ‘Convert a b’
...
Constraint is no smaller than the instance head
in the constraint: Convert X b
(Use UndecidableInstances to permit this)
In the instance declaration for ‘Convert a b’
"不小于实例头"，尽管我们可以在心理上重写它 因为"这个实例可能会被用来证明 本身，让你很痛苦，咬牙切齿和打字。这 帕特森条件一起防止实例解析中的循环。 我们在这里的违规行为说明了为什么它们是必要的，我们可以 大概可以查阅一些论文，看看为什么它们就足够了。
触底反弹
至于为什么程序在运行时无限循环：有无聊 答案，evil :: a -> b不能无限循环或抛出 例外或通常触底，因为我们信任Haskell。 类型检查器a -> b，除了 底。
一个更有趣的答案是，既然Convert X X同义重复为真，它的实例定义是这个无限循环
convertXX :: X -> X
convertXX = convertXX . convertXX
我们同样可以扩展Convert A B实例定义。
convertAB :: A -> B
convertAB =
convertXB . convertAX
where
convertAX = convertXX . convertAX
convertXX = convertXX . convertXX
convertXB = convertXB . convertXX
这种令人惊讶的行为，以及如何约束实例解析(通过 没有扩展名的默认值)旨在避免这些 行为，也许可以作为哈斯克尔的一个很好的理由 TypeClass系统尚未得到广泛采用。尽管它 令人印象深刻的受欢迎程度和力量，它有奇怪的角落(无论是 它在文档或错误消息或语法中，甚至可能在 它的基本逻辑)似乎特别不适合我们人类的方式 考虑类型级抽象。
以下是我在心理上如何处理这些情况：
class ConvertFoo a b where convertFoo :: a -> b
instance (ConvertFoo a Foo, ConvertFoo Foo b) => ConvertFoo a b where
convertFoo = ...
evil :: Int -> String
evil = convertFoo
首先，我们从计算所需实例集开始。
evil直接需要ConvertFoo Int String(1)。- 然后，(1) 需要
ConvertFoo Int Foo(2) 和ConvertFoo Foo String(3)。 - 然后，(2)需要
ConvertFoo Int Foo(我们已经计算过)和ConvertFoo Foo Foo(4)。 - 然后(3)需要
ConvertFoo Foo Foo(计数)和ConvertFoo Foo String(计数)。 - 然后(4)需要
ConvertFoo Foo Foo(计数)和ConvertFoo Foo Foo(计数)。
因此，我们到达一个不动点，这是一组有限的必需实例。编译器在有限时间内设置的计算没有问题：只需应用实例定义，直到不再需要约束。
然后，我们继续为这些实例提供代码。在这里。
convertFoo_1 :: Int -> String
convertFoo_1 = convertFoo_3 . convertFoo_2
convertFoo_2 :: Int -> Foo
convertFoo_2 = convertFoo_4 . convertFoo_2
convertFoo_3 :: Foo -> String
convertFoo_3 = convertFoo_3 . convertFoo_4
convertFoo_4 :: Foo -> Foo
convertFoo_4 = convertFoo_4 . convertFoo_4
我们得到了一堆相互递归的实例定义。在这种情况下，这些将在运行时循环，但没有理由在编译时拒绝它们。