[Haskell-cafe] Resolving overloading loops for circular constraint graph

[Stefan Holdermans]

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