On 10/2/2014 2:50 AM, Richard Eisenberg wrote:
Unfortunately, this all breaks apart horribly when thinking about type instances. Global uniqueness, not just coherence, is needed for type instances:
type family F a b type instance F a b = b
oops :: F a b -> b oops = id
unsafeCoerce :: a -> b unsafeCoerce = let type instance F a b = a in oops
The problem is that a type instance introduces a type equality. Haskell is capable of passing type equality evidence around, so equalities can escape their scope, if the programmer wants to do so. Thus, there can never be a situation where some type (in this case `F a b`) is equal to one thing in one context and an incompatible thing in a different context, anywhere in the same program. I've written my example above with non-associated types, but the same thing can be written with associated types (and more syntactic overhead). I can't currently imagine a type-safe system that did not require global uniqueness for type instances. Thank you, Richard, for giving a concrete example.
Several things can be said about the above code. First and foremost, it seems unsafe to allow oops to even typecheck today. Suppose `F` did not have a catchall instance. Then the type `F a b` is morally equivalent to `forall a. a`, because we could create any instance we wished for `F`. Therefore, I would suggest that regardless of my original proposal being accepted, we only allow open type families in type signatures where they are either morally equivalent to closed type families (by having catchall instances) or where they appear as restrictions on more polymorphic values (such as `id :: F a b -> F a b`). Associated types would also be permitted if an instance of their typeclass were in scope. Second, as hinted above, open type families with catchall instances are morally equivalent to a closed type families, since no other instances can be added to them without overlapping with the catchall instance. Therefore, I also suggest that open type families with catchall clauses be considered closed. Finally, this case serves as an excellent example to show that if and when we add support for local closed type families, we must consider the local type family distinct from the global one. In particular, one won't be able to pass instances of the local families to functions expecting the global family without compromising type safety. With the proposal from my first point, we outlaw `oops`, even with associated types, and thereby regain type safety. Any other problems? Gesh