2

以下代码段使 GHC（使用 8.6.2 和 8.4.4 检查）在编译期间卡住：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

import GHC.Exts (Constraint)

data T = T

type family F t (c :: * -> Constraint) :: Constraint
type instance F T c = c T

class F t C => C t where

t :: C T => t
t = undefined

我认为它被卡住了，因为tGHC 试图找到C T，这导致F T C通过类型族扩展F回C T，这就是它正在寻找的（无限循环）。

我想理论上 GHC 可以说它C T从自身达到了它的要求，并且任何依赖于自身的东西都可以递归地工作，还是我误解了什么？

旁注：在我偶然发现这种行为的真实示例中，我能够实现我想要的，而编译器不会被替换为UndecidableSuperClasses卡住Data.Constraint.Dict。

4

1 回答 1

5

UndecidableSuperClasses不会使实例解析变得懒惰。编译器仍然会尽可能地扩展超类约束。我相信实例字典中指向超类字典的字段是严格的，GHC 实际上在编译时将它们固定下来。这与 相比UndecidableInstances，它允许（有点）懒惰地处理实例约束。

deriving instance Show (f (Fix f)) => Show (Fix f)

会工作得很好。当解析例如Show (Fix Maybe)) 的实例时，GHC 将看到它需要Show (Maybe (Fix Maybe)). 然后它看到它需要Show (Fix Maybe)（它目前正在解决）并接受它，这要归功于UndecidableInstances.

UndecidableSuperClases所做的只是禁用保证扩展不会循环的检查。请参阅Ed Kmett 演讲开头附近的一段，他描述了“到达固定点”的过程。

考虑一个工作示例（摘自Data.Constraint.Forall）：

type family Skolem (p :: k -> Constraint) :: k
class p (Skolem p) => Forall (p :: k -> Constraint)

GHC 只接受这个UndecidableSuperclasses。为什么？因为它不知道该约束可能意味着什么。据它所知，情况可能p (Skolem p)会减少到Forall p. 这实际上可能发生！

class Forall P => P x

-- This definition loops the type checker
foo :: P x => x
foo = undefined
于 2018-11-29T20:54:53.493 回答