Why does GHC's type-checker accept this UndecidableInstance trick?

Question

GHC accepts the following code.

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances  #-}

class Blib b where
  blib :: b

class Blob b where
  blob :: b

instance Blib b => Blob b where
  blob = blib

instance Blob b => Blib b where
  blib = blob

bad :: ()
bad = blib () 4 'a' -- I can add any number of arguments of any type, it still compiles

main ::IO ()
main = return bad

More curiosities :

• when I run the executable, it works "fine", somehow
• when I load it in GHCi and I just type bad it hangs GHCi.
• if I I remove the declaration for blib and blob as follows, the code no longer hangs GHCi :

instance Blib b => Blob b where
  -- blob = blib

instance Blob b => Blib b where
  -- blib = blob

What is happening ?

Answer 1

This has nothing to do with UndecidableInstances, really. The only thing that extension is doing is allowing your instance declarations to compile:

instance Blib b => Blob b where

When you put a constraint on an instance, the constrained type is required to be "smaller" than the instance head. For instance:

instance Foo a => Foo [a]

That constraint only covers a, which is a sub-part of the instance head [a]. This is always allowed. But your definitions have the constraint on the same type as the instance head. This is forbidden without UndecidableInstances.

But all the other behavior you're observing isn't concerned about that. You get the exact same results with something like:

blib :: b
blib = blob

blob :: b
blob = blib

bad :: ()
bad = blib () 4 'a'

main ::IO ()
main = return bad

blib accepts any number of arguments because it's literally whatever type (of kind Type). In this case inference (and defaulting the numeric literal to Integer because nothing specifies it) determines its type to be () -> Integer -> Char -> (). The declared type b unifies with that, so there's no type error.

The compiled program works fine because it never evaluates bad. A compiled program runs the IO action main, and ignores the value the IO produces. Since running the IO never evaluates bad, the whole thing reduces to a no-op.

In contrast, ghci loops forever because evaluating bad to print it results in infinite mutual recursion.

For reference, ghci does several things with bare expressions entered into it. It's worth keeping in mind that it tries these things in this order:

1. If the inferred type of the expression unifies with IO (), it runs the IO action and prints nothing.
2. If the inferred type of the expression unifies with Show a => IO a, it runs the IO action and prints the result.
3. If the inferred type of the expression unifies with IO a, it runs the IO action and prints nothing.
4. It treats the input as if it was print <expr> for whatever expression you entered, and proceeds as in case 1 above.