由于UndecidableSuperClasses,GHC陷入困境 - 预期的行为或错误？

Question

以下片段使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代替.

Answer 1

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