Local evidence and type class instances

[Simon Peyton-Jones]

| Now that the Glorious New type checker can handle local evidence
| seamlessly, is it a big implementation burden to extend it to deal
| with local *type class instances* in addition to local *equality
| constraints*?
...
| Are there big theoretical problems with this extension, or is it just
| a lack of engineering effort that has prevented its implementation?

The issues I know about are

a) overlap (of course)
b) coherence (two different instances in two places)
c) if you add associated types, then soundness too
d) completeness

Concerning (c) you can't define (type instance F Int = Bool) in one place and (type instance F Int = Char) somewhere else, or you'll have seg faults.  GHC checks that you don't, but it can only do that because the instances are global.

Perhaps most important

Concerning (d) we only have a theory for local *constraints*, not for local *constraint schemes* (ie with foralls in them).  To get complete inference with assumptions like (F (G x) ~ G x) was tricky enough.  Adding schemes would make it harder.

But yes, it'd be useful.  As well as Oleg and Ken's paper, the "Derivable type classes" paper that Ralf and I wrote some time ago argues for local constraint schemes.

Simon