How can undecidable instances actually hang the co

问题:

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?

回答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.

回答2:

The simplest way to get a "reduction stack overflow" is using type families:

type family Loop where
  Loop = Loop

foo :: Loop
foo = True

I don't know a direct way to get actually looping compilation on the current GHC. I recall getting loops a couple of times with GHC 7.11, but I only remember one in reproducible detail:

data T where
    T :: forall (t :: T). T

But this has been fixed since.

回答3:

To my surprise, UndecidableInstances can actually hang certain GHC versions. Here are the few lines of code that did it for me:

{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}
module Nested where

class Nested r ix where

type family Lower ix :: *

data LN

instance Nested LN (Lower ix) => Nested LN ix where

data L

instance Nested LN ix => Nested L ix where

When compiled as part of a library (not directly ghc main.hs) this code hangs indefinitely on GHC 8.2.1

As @luqui mentioned, this does seem like a bug, so it has been reported as such: https://ghc.haskell.org/trac/ghc/ticket/14402

Edit: It turned out to be a bug indeed, which has already been fixed in current development version of GHC.