haskell - 不可判定的实例如何真正挂起编译器？

Question

当我第一次读到严肃的criticism on -XUndecidableInstances时，我已经完全习惯了它，将其视为消除 Haskell98 必须使编译器更容易实现的烦人限制。

事实上，我遇到过很多需要不可判定实例的应用程序，但没有一个应用程序实际上导致了与不可判定性相关的任何问题。卢克的例子是有问题的，原因完全不同

class Group g where
  (%) :: g -> g -> g
  ...
instance Num g => Group g where
  ...

——嗯，这显然会被任何适当的Group实例重叠，因此不确定性是我们最不担心的:这实际上是不确定的我>!

但公平地说，我一直在我的脑海中保留着“不确定的实例可能会挂起编译器”。

当我读到 this challenge on CodeGolf.SE 时，它是从哪里获得的？ ，要求提供会无限挂起编译器的代码。嗯，听起来像是一项针对不可判定实例的工作，对吧？

事实证明我无法让他们这么做。以下内容可以立即编译，至少从 GHC-7.10 开始是这样:

{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
class C y
instance C y => C y
main = return ()

我什至可以使用类方法，它们只会在运行时引起循环:

{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
class C y where y::y
instance C y => C y where y=z
z :: C y=>y; z=y
main = print (y :: Int)

但是运行时循环并不罕见，您可以轻松地在 Haskell98 中编写这些代码。

我还尝试了不同的、不太直接的循环，例如

{-# LANGUAGE FlexibleContexts, UndecidableInstances #-}
data A x=A
data B x=B
class C y
instance C (A x) => C (B x)
instance C (B x) => C (A x)

再次强调，编译时没有问题。

那么，在解析不可判定的类型类实例时实际需要什么来挂起编译器？

Answer 1

我认为我从未真正挂起编译器。我可以通过修改您的第一个示例来使其堆栈溢出。似乎正在进行一些缓存，因此我们需要要求无限序列的唯一约束，例如

data A x = A deriving (Show)
class C y where get :: y
instance (C (A (A a))) => C (A a) where
    get = A

main = print (get :: A ())

这给了我们

• Reduction stack overflow; size = 201
  When simplifying the following type:
    C (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A ())))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  Use -freduction-depth=0 to disable this check
  (any upper bound you could choose might fail unpredictably with
   minor updates to GHC, so disabling the check is recommended if
   you're sure that type checking should terminate)

它告诉你如果你真的想的话如何让它挂起来。我的猜测是，如果你可以让它在没有这个的情况下挂起，那么你就发现了一个错误。

我很想听听 GHC 工作人员的意见。