
9 Sep
2009
9 Sep
'09
3:48 p.m.
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? Cheers, Stefan