2009/9/9 Stefan Holdermans
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 1994http://www.informatik.uni-trier.de/%7Eley/db/conf/lfp/lfp1994.html#Thatte94: 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 http://www.cs.mu.oz.au/%7Esulzmann/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