Resolving overloading loops for circular constraint graph

[Simon Peyton-Jones]

Stefan

You are trying to do something quite delicate here.  

The whole idea of solving constraints in a co-inductive way (building a recursive group of dictionary definitions) relies on spotting something we've seen before to "tie the knot".  To date, the main application I knew for this fairly exotic idea was described in the SYB3 paper [1].  So I'm curious about your application (and that of anyone else) that relies on this recursive-dictionary-solving mechanism.

Returning to your problem, this "loop spotting" mechanism is rather syntactic at the moment, whereas your application needs something more refined, involving equality modulo type function reductions.  Alas, the constraint solving machinery for type classes and for type functions is not properly integrated.  I'm amazed it works as well as it does, actually.

We [Manuel, Dimitrios, and I] are (slowly, slowly) working on a complete rewrite of GHC's constraint-solving mechanism.  I'm pretty sure that it'll solve this problem among many others.  But don't hold your breath.  It'll be months not weeks.  But not years!

sorry not to be able to solve your problem sooner.  I'll open a ticket.

Simon

[1] http://research.microsoft.com/~simonpj/papers/hmap

| -----Original Message-----
| From: Stefan Holdermans [mailto:stefan at cs.uu.nl]
| Sent: 09 September 2009 14:38
| To: Manuel M T Chakravarty; Simon Peyton-Jones
| Cc: glasgow-haskell-users; haskell-cafe; José Pedro Magalhães; Thomas van Noort;
| Johan Jeuring
| Subject: Resolving overloading loops for circular constraint graph
| 
| 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