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.

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.

-Martin

2009/9/9 Stefan Holdermans <stefan@cs.uu.nl>
Manuel, Simon,

I've spotted a hopefully small but for us quite annoying bug in GHC's type checker: it loops when overloading resolving involves a circular constraint graph containing type-family applications.

The following program (also attached) demonstrates the problem:

 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeFamilies     #-}

 type family F a :: *
 type instance F Int = (Int, ())

 class C a
 instance C ()
 instance (C (F a), C b) => C (a, b)

 f :: C (F a) => a -> Int
 f _ = 2

 main :: IO ()
 main = print (f (3 :: Int))

My guess is that the loop is caused by the constraint C (F Int) that arises from the use of f in main:

 C (F Int) = C (Int, ()) <= C (F Int)

Indeed, overloading can be resolved successfully by "black-holing" the initial constraint, but it seems like the type checker refuses to do so.

Can you confirm my findings?

I'm not sure whether this is a known defect. If it isn't, I'd be more than happy to issue a report.

Since this problem arises in a piece of very mission-critical code, I would be pleased to learn about any workarounds.

Thanks in advance,

 Stefan
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe