uncidable实例如何实际挂起编译器？

Question

当我第一次阅读严肃的批评时-XUndecidableInstances,我已经完全习惯了它,将其视为仅仅删除了令人讨厌的限制Haskell98必须使编译器更容易实现.

事实上,我遇到了大量需要不可判定实例的应用程序,但没有一处它们实际上导致任何与不可判定性相关的问题.卢克的例子存在问题,原因完全不同

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

- 好吧,这显然会被任何适当的实例重叠Group,所以不可判断性是我们最不担心的事情:这实际上是不确定的!

但公平地说,我自己保留了"不可判断的实例可能会让编译器挂起".

当我在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)

它告诉你如果你真的想要如何让它挂起来.我的猜测是,如果你能在没有这个的情况下让它挂起,你就会发现一个bug.

我很想听听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

但此后这已得到修复.