What I'm trying to demonstrate here is that only during inference (ie. applying CHRs) we may come across cycles. Hence, the quest is to come up with *dynamic* termination methods. I think that's what you are interested in?
first, lets clarify: all of this is happening before program runtime, so instead of talking about static-static and static-dynamic, I'd prefer to talk about decisions made (a) on the basis of a single instance declaration for a class C (b) on the basis of all declarations for a class C (c) on the basis of each use of class C your concern then seems to be that while you'd like to encourage exploration of termination proofs based on (c), you suggest restriction to those based on (a) for now. but even if I accepted that, I would still not put the generalised occurs-check into the same category as other (c) conditions. the reason being that having occurs-checks whenever types are unified is a built-in assumption in all of Haskell's static type system. my point is that FDs introduce a new source of type unifications, and that this new source needs to be provided with an adequate version of occurs-checks for the rest of the type system to be safe from non-termination. consequently: - we need to devise such an occurs-check anyway - once we've done so, we might as well assume it in FD handling as well in other words, even though using some form of occurs-check to guarantee termination of examples like Mul looks like it would fall under (c), it actually falls under (a), because that specific "dynamic" check is part of the environment. that said, yes, I agree that we need to tackle termination with more than just (a) - the sooner the better. it seems strange to rule out definitions because of possible invalid uses; even with static typing, we only check under which conditions a definition is internally consistent, then reject any *uses* that would violate those conditions (we don't reject length because someone might try to call it with a non-list as parameter).
FYI, in a technical report version of the FD paper, we already address such issues, briefly.
where would I find that report? cheers, claus