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

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: 208-219

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

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 = {http://www.cs.mu.oz.au/~sulzmann/manuscript/coind-type-class-proofs.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 future.

-Martin