haskellundecidable-instances

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


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 :

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

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

What is happening ?


Solution

  • 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.