How can undecidable instances actually hang the compiler?

Question

By the time I first read serious criticism on -XUndecidableInstances, I had already completely accustomed to it, seeing it as merely removal of an annoying restriction Haskell98 has to make compilers easier to implement.

In fact I've encountered plenty of applications where undecidable instances were needed, but none where they actually caused any problems related to undecidability. Luke's example is problematic for quite a different reason

class Group g where
  (%) :: g -> g -> g
  ...
instance Num g => Group g where
  ...

– well, this would clearly be overlapped by any proper Group instance, so undecidability is the least of our worries: this is actually undeterministic!

But fair enough, I since kept “undecidable instances can possibly hang the compiler” in the back of my head.

Whence it was procured when I read this challenge on CodeGolf.SE, asking for code that would infinitely hang the compiler. Well, sounds like a job for undecidable instances, right?

Turns out I can't get them to do it. The following compiles in no time, at least from GHC-7.10:

{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
class C y
instance C y => C y
main = return ()

I can even use class methods, and they'll only cause a loop at runtime:

{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
class C y where y::y
instance C y => C y where y=z
z :: C y=>y; z=y
main = print (y :: Int)

But runtime loops are nothing unusual, you can easily code these in Haskell98.

I also tried different, less direct loops such as

{-# LANGUAGE FlexibleContexts, UndecidableInstances #-}
data A x=A
data B x=B
class C y
instance C (A x) => C (B x)
instance C (B x) => C (A x)

Again, no problem at compile time.

So, what is actually needed to hang the compiler up in resolution of undecidable type class instances?

Answer 1

I don't think I've ever actually hung the compiler. I can get it to stack overflow though by modifying your first example. It seems that there is some caching going on, so we need to demand an infinite sequence of unique constraints, e.g.

data A x = A deriving (Show)
class C y where get :: y
instance (C (A (A a))) => C (A a) where
    get = A

main = print (get :: A ())

which gives us

• Reduction stack overflow; size = 201
  When simplifying the following type:
    C (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A ())))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  Use -freduction-depth=0 to disable this check
  (any upper bound you could choose might fail unpredictably with
   minor updates to GHC, so disabling the check is recommended if
   you're sure that type checking should terminate)

which tells you how you could get it to hang if you really wanted to. My guess is that if you can get it to hang without this you've found a bug.

I'd love to hear from somebody who works on GHC.