Resolving overloading loops for circular constraint graph

Martin Sulzmann martin.sulzmann.haskell at
Thu Sep 10 14:54:50 EDT 2009

2009/9/9 Stefan Holdermans <stefan at>

> Dear Martin,
>  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.
> A propos: are there fundamental objections to coinductive resolving, i.e.,
> constructing recursive dictionaries. I suppose termination is hard to
> guarantee then: is it enough to require constraints to be productive w.r.t.
> instance heads?
Yes, you need instances to be productive, otherwise, you get
bogus cyclic proofs like
instance Foo a => Foo a

dictFooa = dictFooa

You could call this a bug, or simply blame the programmer
for writing down a 'bogus' instance.

Under co-inductive type class solving more (type class) programs will
terminate (my guess). Here are some references:

Satish R. Thatte: Semantics of Type Classes Revisited. LISP and Functional
Programming 1994<>:

As far as I know, the first paper which talks about co-induction and type

I myself and some co-workers explored this idea further in some
unpublished draft:

 AUTHOR = {M. Sulzmann and J. Wazny and P. J. Stuckey},
  TITLE = {Co-induction and Type Improvement in Type Class Proofs},

  NOTE = {Manuscript},
  YEAR = {2005},
  MONTH = {July},
  PS = {

I'm quite fond of co-induction because it's such an elegant and powerful
proof technique. However, GHC's co-induction mechanism is fairly limited,
see Simon's reply, so I'm also curious to see what's happening in the

-------------- next part --------------
An HTML attachment was scrubbed...

More information about the Glasgow-haskell-users mailing list