Lambda the Ultimate

In the course of a BitC discussion today, somebody pointed me at this recent note by Simon Peyton-Jones. In it, Simon cites Oleg and Martin as pointing out that (1) type families do not play nicely with overlapping instances, (2) functional dependencies appear to, but (3) the two are equivalent, so something smells wrong.

Simon gives two illustrating examples, both of which are constructed by exploiting lexical hiding across modules. I found this quite disturbing, since we rely on functional dependencies in BitC and we've been struggling with the instance resolution question. But looking at Simon's examples, it seems to me that both of them result from obvious type checking failures in the assumed implementation. I would greatly appreciate a sanity check on this.

A functional dependency constitutes a statement by the programmer that a deterministic function exists between the type parameters of the type function and its type result. We are told that such a function exists, but not how it is defined. That is: the functional dependency is an assertion that such a deterministic function exists, and we should interpret it as meaning that the typing of the program is sound provided the assertion is true. The assertion itself remains to be checked.

Both of Simon's examples construct circumstances in which two modules construct conflicting instantiations of a functional dependency by exploiting the limitations of scope visibility. Both break a type class:

class C a b | a -> b

The first does so directly by introducing instances C Int Bool and C Int Char. The second does so by simultaneously introducing C Int Bool and C 'a [a] forall a. This is a problem because the second instance might instantiate polymorphically to C Int [Int].

In both cases, it seems to me that we have a global determinism requirement on the type function that isn't being checked correctly, and that this is the root of the problem. In the first case, the overlap is direct. In the second case, it is sufficient to note that the two instances are not unifiable. The root problem appears to be that a global assertion is not being globally checked. That such a failure to check would lead to unsoundness does not seem either complex or surprising to me. Indeed, I would be surprised by any other outcome!

So here is my question: assuming we do check that the functional dependency requirements are not violated, does an unsoundness problem remain? It's not too late to drop fundeps from BitC v1 if we need to be conservative about this.

The search engine can't handle the # character. Maybe there is an escape character, but in that case I don't know about it.