Haskell/GHC UndecidableInstances - 非终止类型检查的示例？

Question

我编写了一些需要-XUndecidableInstances来编译的Haskell代码.我确实理解为什么会发生这种情况,因为存在某种违反的条件,因此GHC会大喊大叫.

但是,我从来没有遇到类型检查器实际上挂起或在无限循环中结束的情况.

非终止实例定义是什么样的 - 你能给出一个例子吗？

Answer 1

在本文的HQ中有一个经典的,有点令人担忧的例子(涉及与功能依赖的交互):

class Mul a b c | a b -> c where
  mul :: a -> b -> c
instance Mul a b c => Mul a [b] [c] where
  mul a = map (mul a)

f b x y = if b then mul x [y] else y

我们需要mul x [y]有相同的类型y,所以,服用x :: x和y :: y,我们需要

instance Mul x [y] y

根据给定的例子,我们可以拥有.当然,我们必须采取y ~ [z]一些z这样的方式

instance Mul x y z

即

instance Mul x [z] z

我们在一个循环中.

令人不安的是,因为该Mul实例看起来像它的递归在结构上正在减少,这与Petr的答案中明显的病态实例不同.然而它使GHC循环(无聊阈值开始以避免悬挂).

我确信我已经提到某些地方的问题是,y ~ [z]尽管在z功能上取决于事实,但仍然存在问题y.如果我们对函数依赖使用函数表示法,我们可能会看到约束表示y ~ Mul x [y]并拒绝替换,因为它违反了发生检查.

好奇,我以为我会给它一个旋转,

class Mul' a b where
  type MulT a b
  mul' :: a -> b -> MulT a b

instance Mul' a b => Mul' a [b] where
  type MulT a [b] = [MulT a b]
  mul' a = map (mul' a)

g b x y = if b then mul' x [y] else y

与UndecidableInstances启用,它需要相当长一段时间的循环超时.在UndecidableInstances禁用的情况下,实例仍然被接受并且类型检查器仍然循环,但截止发生的速度要快得多.

所以...有趣的旧世界.

Answer 2

例如:

{-# LANGUAGE UndecidableInstances #-}

class C a where
    f :: a -> a

instance C [[a]] => C [a] where
    f = id

g x = x + f [x]

发生了什么:输入f [x]编译时需要确保x :: C [a]一些a.实例声明说,x能型的C [a],只有当它是类型也C [[a]].因此编译器需要确保x :: C [[a]]等等,并陷入无限循环.

另请参见可以在本地使用UndecidableInstances pragma对编译终止产生全局影响吗？