I've had some interesting off-list discussion with Tom Schrijvers (one of the guys responsible for the K.U.Leuven CHR System, which is provided, eg., in SWI Prolog). particularly interesting was the difference in perspective (logic vs functional programming). I'd like to share two items from that discussion (haven't thought either of them through yet, but hope they both provide useful food for thought to those of you interested in the type class problem). 1. I didn't have to explain to him that FDs may lead to variable instantiation, but I did have to explain why without FDs, there is no variable instantiation, and why we even think about FD consistency without automatically implying unification (improvement). the main difference here seems to be that he was thinking of all variables as existentially quantified, whereas type variables are mostly universally quantified, so far. I hadn't given that much thought before, because FDs are meant to determine their range types, and there isn't much difference between universal and existential quantification if there is only one possible variable value, eg: (forall a in {Char}. T a) vs (exists a in {Char}. T a) but perhaps some of the interpretation disagreements we have with FDs could be mitigated if we interpreted FDs differently, depending on whether the range type variables are universally or existentially quantified. given some 'class C a b | a -> b', we could try something like: - forall a b. C a b => T a b: no improvement for b, the FD is used only for checking consistency - forall a. exists b. C a b => T a b improvement & consistency check for b 2. he suggested that the whole problem may be an instance of generalised propagation: Generalised Constraint Propagation Over the CLP Scheme, by Thierry Le Provost and Mark Wallace. Journal of Logic Programming 16, July 1993. Also [ECRC-92-1] http://eclipse.crosscoreop.com:8080/eclipse/reports/ecrc_genprop.ps.gz I agree that this might be a useful framework in which to discuss further developments (variable instantiation is a lot more limited in our context, but we think about why and how to change that; we need to reason in an open world, but at least theoretically, we can collect all instances; we don't have multiple solutions, but we do sometimes need to look at instances before knowing all variable instantiations, leaving us with multiple possible matches, so approximation may be a useful alternative to full search for us, rather than just the optimisation it is in the logic case). any thoughts?-) cheers, claus