relaxed instance rules spec (was: the MPTC Dilemma (pleasesolve))

[Claus Reinke]

> 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