不可确定的实例如何实际上挂起编译器

Question

到我第一次阅读对-XUndecidableInstances的严重批评时，我已经完全习惯了它，因为它仅仅是删除了令人讨厌的限制haskell98必须使编译器更易于实现。

实际上，我遇到了很多需要不可确定的实例的应用程序，但是它们实际上没有造成与不可证明性有关的任何问题。卢克的例子是有问题的，原因是完全不同的原因

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

- 嗯，这显然是由任何适当的Group实例重叠的，因此不确定性是我们最不担忧的：这实际上是毫无确定的 stroneisticalisticisticalisticisticaliastic ！

但很公平，我将"不可决定的实例可能会挂在编译器的后面"。

在我在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的人的来信。

Answer 2

获得"减少堆栈溢出"的最简单方法是使用类型自己的家族：

type family Loop where
  Loop = Loop
foo :: Loop
foo = True

我不知道在当前GHC上实际循环汇编的直接方法。我记得GHC 7.11几次获得循环，但我只记得一个可复制的细节：

data T where
    T :: forall (t :: T). T

，但这已经解决了。

Answer 3

令我惊讶的是，UndecidableInstances实际上可以挂起某些GHC版本。这是为我做的几行代码：

{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}
module Nested where
class Nested r ix where
type family Lower ix :: *
data LN
instance Nested LN (Lower ix) => Nested LN ix where
data L
instance Nested LN ix => Nested L ix where

作为库的一部分进行编译时（不是直接ghc main.hs），此代码无限期地悬挂在GHC 8.2.1

上

正如@luqui提到的那样，这确实是一个错误，因此已被报道：https：//ghc.haskell.org/trac/ghc/ghc/ticket/14402

编辑：事实证明它确实是一个错误，它已经在GHC的当前开发版本中固定。