Dear Martin,
Your example must loop because as you show below the instance declaration leads to a cycle.
By "black-holing" you probably mean co-induction. That is, if the statement to proven appears again, we assume it must hold. However, type classes are by default inductive, so there's no easy fix to offer to your problem.
Yes, I meant coinductive resolving of overloading. By that line of reasoning, the following should loop as well, but doesn't: {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE UndecidableInstances #-} class C a instance C () instance (C (a, ()), C b) => C (a, b) f :: C (a, ()) => a -> Int f _ = 2 main :: IO () main = print (f (3 :: Int)) Note: here I would accept looping behaviour as this program requires undecidable instances.
In any case, this is not a bug, you simply play with fire once type functions show up in the instance context. There are sufficient conditions to guarantee termination, but they are fairly restrictive.
I disagree: it is a bug. I think the original program should require undecidable instances as well: indeed, the presence of the type family makes that the constraint is possibly no smaller than the instance head. However, without the undecidable-instance requirement (i.e., as it is now), I expect type checking to terminate. Cheers, Stefan