Type functions and recursive dictionaries

Stefan Holdermans reports: 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 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?

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

Trac metadata

Trac field	Value
Version	6.10.4
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	stefan@cs.uu.nl
Operating system
Architecture