[Haskell-cafe] Fwd: Increasing Haskell modularity

[Gesh]

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