Haskell/GHC UndecidableInstances - example for non-terminating type check?

Question

I've written some Haskell code which needs -XUndecidableInstances to compile. I do understand why that happens, that there is a certain condition which is violated and therefore GHC yells.

However, I've never come across a situation where the type checker would actually hang or wind up in an endless loop.

What does a non-terminating instance definition look like - can you give an example?

Answer 1

For example:

{-# LANGUAGE UndecidableInstances #-}

class C a where
    f :: a -> a

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

g x = x + f [x]

What is happening: When typing f [x] the compiler needs to ensure that x :: C [a] for some a. The instance declaration says that x can be of type C [a] only if it is also of type C [[a]]. So the compiler needs to ensure that x :: C [[a]], etc. and gets caught in an infinite loop.

See also Can using UndecidableInstances pragma locally have global consequences on compilation termination?

Answer 2

There's a classic, somewhat alarming example (involving interaction with functional dependencies) in 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

We need mul x [y] to have the same type as y, so, taking x :: x and y :: y, we need

instance Mul x [y] y

which, according to the given instance, we can have. Of course, we must take y ~ [z] for some z such that

instance Mul x y z

i.e.

instance Mul x [z] z

and we're in a loop.

It's disturbing, because that Mul instance looks like its recursion is structurally reducing, unlike the clearly pathological instance in Petr's answer. Yet it makes GHC loop (with the boredom threshold kicking in to avoid hanging).

The trouble, as I'm sure I've mentioned somewhere somewhen, is that the identification y ~ [z] is made in spite of the fact that z depends functionally on y. If we used a functional notation for the functional dependency, we might see that the constraint says y ~ Mul x [y] and reject the substitution as in violation of the occurrence check.

Intrigued, I thought I'd give this a whirl,

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

With UndecidableInstances enabled, it takes quite a while for the loop to time out. With UndecidableInstances disabled, the instance is still accepted and the typechecker still loops, but the cutoff happens much more quickly.

So... funny old world.