haskelltypeclassundecidable-instances

Why does this code using UndecidableInstances compile, then generate a runtime infinite loop?

When writing some code using UndecidableInstances earlier, I ran into something that I found very odd. I managed to unintentionally create some code that typechecks when I believed it should not:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}

data Foo = Foo

class ConvertFoo a b where
  convertFoo :: a -> b

instance (ConvertFoo a Foo, ConvertFoo Foo b) => ConvertFoo a b where
  convertFoo = convertFoo . (convertFoo :: a -> Foo)

evil :: Int -> String
evil = convertFoo

Specifically, the convertFoo function typechecks when given any input to produce any output, as demonstrated by the evil function. At first, I thought that perhaps I managed to accidentally implement unsafeCoerce, but that is not quite true: actually attempting to call my convertFoo function (by doing something like evil 3, for example) simply goes into an infinite loop.

I sort of understand what’s going on in a vague sense. My understanding of the problem is something like this:

Now, even if the above understanding is correct, I am still confused about why the whole program typechecks. Specifically, I would expect the ConvertFoo a Foo and ConvertFoo Foo b constraints to fail, given that no such instances exist.

I do understand (at least fuzzily) that constraints don’t matter when picking an instance—the instance is picked based solely on the instance head, then constraints are checked—so I could see that those constraints might resolve just fine because of my ConvertFoo a b instance, which is about as permissive as it can possibly be. However, that would then require the same set of constraints to be resolved, which I think would put the typechecker into an infinite loop, causing GHC to either hang on compilation or give me a stack overflow error (the latter of which I’ve seen before).

Clearly, though, the typechecker does not loop, because it happily bottoms out and compiles my code happily. Why? How is the instance context satisfied in this particular example? Why doesn’t this give me a type error or produce a typechecking loop?

Solution

  • I wholeheartedly agree that this is a great question. It speaks to how our intuitions about typeclasses differ from the reality.

    Typeclass surprise

    To see what is going on here, going to raise the stakes on the type signature for evil:

    data X

class Convert a b where
  convert :: a -> b

instance (Convert a X, Convert X b) => Convert a b where
  convert = convert . (convert :: a -> X)

evil :: a -> b
evil = convert

    Clearly the Covert a b instance is being chosen as there is only one instance of this class. The typechecker is thinking something like this:

    The typechecker has surprised us. We do not expect Convert X X to be true as we have not defined anything like it. But (Convert X X, Convert X X) => Convert X X is a kind of tautology: it is automatically true and it is true no matter what methods are defined in the class.

    This might not match our mental model of typeclasses. We expect the compiler to gawk at this point and complain about how Convert X X cannot be true because we have defined no instance for it. We expect the compiler to stand at the Convert X X, to look for another spot to walk to where Convert X X is true, and to give up because there is no other spot where that is true. But the compiler is able to recurse! Recurse, loop, and be Turing-complete.

    We blessed the typechecker with this capability, and we did it with UndecidableInstances. When the documentation states that it is possible to send the compiler into a loop it is easy to assume the worst and we assumed that the bad loops are always infinite loops. But here we have demonstrated a loop even deadlier, a loop that terminates – except in a surprising way.

    (This is demonstrated even more starkly in Daniel's comment:

    class Loop a where
  loop :: a

instance Loop a => Loop a where
  loop = loop

    .)

    The perils of undecidability

    This is the exact sort of situation that UndecidableInstances allows. If we turn that extension off and turn FlexibleContexts on (a harmless extension that is just syntactic in nature), we get a warning about a violation of one of the Paterson conditions:

    ...
Constraint is no smaller than the instance head
  in the constraint: Convert a X
(Use UndecidableInstances to permit this)
In the instance declaration for ‘Convert a b’

...
Constraint is no smaller than the instance head
  in the constraint: Convert X b
(Use UndecidableInstances to permit this)
In the instance declaration for ‘Convert a b’

    "No smaller than instance head," although we can mentally rewrite it as "it is possible this instance will be used to prove an assertion of itself and cause you much anguish and gnashing and typing." The Paterson conditions together prevent looping in instance resolution. Our violation here demonstrates why they are necessary, and we can presumably consult some paper to see why they are sufficient.

    Bottoming out

    As for why the program at runtime infinite loops: There is the boring answer, where evil :: a -> b cannot but infinite loop or throw an exception or generally bottom out because we trust the Haskell typechecker and there is no value that can inhabit a -> b except bottom.

    A more interesting answer is that, since Convert X X is tautologically true, its instance definition is this infinite loop

    convertXX :: X -> X
convertXX = convertXX . convertXX

    We can similarly expand out the Convert A B instance definition.

    convertAB :: A -> B
convertAB =
  convertXB . convertAX
  where
    convertAX = convertXX . convertAX
    convertXX = convertXX . convertXX
    convertXB = convertXB . convertXX

    This surprising behavior, and how constrained instance resolution (by default without extensions) is meant to be as to avoid these behaviors, perhaps can be taken as a good reason for why Haskell's typeclass system has yet to pick up wide adoption. Despite its impressive popularity and power, there are odd corners to it (whether it is in documentation or error messages or syntax or maybe even in its underlying logic) that seem particularly ill fit to how we humans think about type-level abstractions.