overlapping instances and constraints

[Claus Reinke]

there were a couple of issues Simon raised that I hadn't responded to in 
my earlier reply. since no-one else has taken them on so far, either, ..

>- Haskell would need to be a lot more specific about exactly where
>context reduction takes place.  Consider
>f xs x = xs == [x]
>Do we infer the type (Eq a) => [a] -> a -> Bool?  Thereby committing to
>a particular choice of instance?  Or do we (as GHC does) infer the type
>(Eq [a]) => [a] -> a -> Bool, so that if f is applied at (say) type
>Char, then an instance Eq [Char] instance would apply.  GHC is careful
>to do the latter.

my general idea about that would be never to commit unless we know it
is the only choice. which seems to be in line with what GHC is doing in
this case. of course, it follows that we'd like to be able to specify choices
unambiguously, to avoid delayed committs.

>Concerning using the instance context, yes, it's attractive, but it
>involves *search* which the current mechanism does not.  Presumably you
>have in mind that the type system should "commit" only when there is
>only one remaining instance declaration that can fit.  You need to be
>very careful not to prune off search branches prematurely, because in a
>traditional HM type checker you don't know what all the type are
>completely.  And you need to take functional dependencies into account
>during the search (but not irrevocably).   I have not implemented this
>in GHC.  I don't know anyone who has.   I don't even know anyone who has
>specified it.

search, yes, but with deterministic result (similar to HM inference). so 
the main issue is that we need to be able to perform inferences without 
committing to their conclusions, or setting up encapsulated inference 
processes with their own assumptions. which isn't surprising given that 
we're dealing with implications, or type class functions, where the usual 
proof rule is "if we can prove the conclusions assuming the prerequisites, 
then we have proven the implication". 

that may be substantially more complicated to implement, but is just what 
Prolog, or even simple HM type inference for functions, have been doing 
for a long time. and it is a pain to see the current situation, where Haskell 
implementations treat the conclusions as if there were no pre-requisites
(Haskell: these instances are overlapping; Programmer: no, they are not,
just look at the code!).

can we agree, at least in principle, that in the long term this needs to change?

since the general implementation techniques aren't exactly new, are there 
any specific reasons why they couldn't be applied to type classes? we'd
have a state for the constraint store, and a backtracking monad with 
deterministic result for the inference, just as we have for implementing 
HM inference. 

if we want a more efficient, more low-level implementation, we could 
use the WAM's idea of variable trails (proceed as if there was no 
search, but record all variable substitutions, so that we can undo them 
if it turns out that this branch fails). or is there a pragmatic issue with 
current implementations of those type classes, having grown out of 
simpler type class beginnings, and having grown so complex that they 
couldn't go in that direction without a major rewrite?

in the short term, I'd be quite willing to aim for a compromise, where
we'd not look at all constraints in the context, but just at a few specific 
ones, for which we know that the search involved will be very shallow.
whether to do that via strictness annotations in contexts, as Bulat has
suggested, or by reserving a separate syntactic position for constraints
known to have shallow proofs, is another question.

the outstanding example of this would be type inequalities, which I'd
really like to see in Haskell', because they remove a whole class of
instance overlaps. and with FDs, one can build on that foundation.

I'm not sure I have a good handle on understanding when or how searches
could be hampered by incomplete types. naively, I'd expect residuation, ie,
delaying partially instantiated constraints until their variables are specific
enough to proceed with inference. I think CHR already does this. 

if that means that instance context constraints cannot be completely 
resolved without looking at concrete uses of those instances, then 
we'd have a problem, but no more than at the moment. and I suspect
that problem will not be a showstopper. on the contrary, it may help
to keep those searches shallow.

from my experience, it seems quite possible to arrange instance 
contexts in such a way that even such incomplete resolution will be 
sufficient to show that they ensure mutual exclusion of their instances 
(type inequality, type-level conditional, FDs, closed classes, ..). 
which would be all that was needed at that point.

once we start looking, we could probably find more ways to help
such incomplete inferences along. eg, if there was a built-in class
Fail a (built-in only so that the system could know there can be
no instances), then we could declare mutual exclusion like this:

    instance (Num a, Function a) => Fail a

[an exclusion which, incidentally, some folks might disagree with;-]

and, independent of the specific a, just by looking at the classes
mentioned in the instance context, and the instances visible in the
current module, the system could infer that the following instance 
constraints are mutually exclusive, hence the instances cannot be
overlapping:

    instance (Num a,..other constraints..) => MyClass a where ..
    instance (Function a, .. other constraints..) => MyClass a where..

Oleg, eg, has shown how such is-a-function constraint could
be used to solve several problems, but his code depends on
ghc-specific tricks from HList, iirc.

cheers,
claus