Haskell/GHC UnndecidableInstances - 非終了型チェックの例？

Question

コンパイルするために-XUndecidableInstancesが必要なHaskellコードを書いています。私はそれがなぜ起こるか、違反された特定の条件があり、それゆえGHCが叫ぶことを理解しています。

しかし、タイプチェッカーが実際にハングアップしたり、無限ループに巻き込まれたりすることはありません。

終了しないインスタンス定義はどのようなものですか？例を挙げてください。例えば

Answer 1

：何が起こっている

{-# LANGUAGE UndecidableInstances #-} 

class C a where 
    f :: a -> a 

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

g x = x + f [x] 

：f [x]を入力するとき、コンパイラは、いくつかのaのためにそのx :: C [a]を確保する必要があります。インスタンスの宣言では、はタイプC [[a]]の場合にのみタイプC [a]であることができます。したがって、コンパイラはx :: C [[a]]などを無限ループで捕らえる必要があります。

も参照してくださいCan using UndecidableInstances pragma locally have global consequences on compilation termination?

Answer 2

（関数従属性との相互作用を含む）、古典的な、やや驚くべき例がthis paper from 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 

我々はyと同じ型を持っているmul x [y]が必要なので、x :: xを取りますおよびy :: y、必要です

instance Mul x [y] y 

whi ch、与えられた例によると、私たちは持つことができます。もちろん、我々はいくつかのzな

instance Mul x y z 

すなわち

instance Mul x [z] z 

、我々はループにしているそのためy ~ [z]を取る必要があります。

Mulインスタンスは、その再帰が構造的にであるため、が減少しているため、Petrの回答の明確な病理学的インスタンスとは異なり、邪魔になります。しかし、それはGHCループを引き起こします（退屈を避けるために退屈な閾値が蹴られます）。

問題は、おそらくどこかで言及したように、がyに機能的に依存しているにもかかわらず、識別番号y ~ [z]が作られているということです。関数の依存関係に関数表記法を使用した場合、制約にy ~ Mul x [y]と表示され、オカレンスチェックに違反して置換が拒否されることがあります。

興味をそそらが、私は、これを有効にUndecidableInstancesで

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を無効にすると、インスタンスは引き続き受け入れられ、型チェッカーは引き続きループしますが、カットオフはずっと速く行われます。

だから...面白い古い世界。