plt/racket — pull request #790 by takikawa (2014-10-08 05:20:38+00:00)
Title: Add contract generation for Evtof types

This PR finally adds contract generation for Evtof types, which was delayed for a while (even though `evt/c` has been ready for a while).

The reason for the delay is that TR needs to be careful with the interaction of synchronizable events and types of values that are writable (e.g., channels). The problem is that the latter have invariant subtyping while the former has covariant subtyping.

This mismatch lets you break the type system if you upcast a value of type `(Channelof String)` to an `(Evtof (U String #f))` and export it to untyped code. TR's read end for original channel is unprotected (and should return `String`) but the untyped code can write a `#f` to the channel.

The solution is to make TR's version of event contracts seal off the writing end of channels (those are the only problematic kind of event that I know of) when they are exported with an event type.

Another solution would be to have TR use invariant subtyping on event types. This seemed worse to me because it'd be unintuitive that a read-only type has invariant subtyping.

If we add support for `prop:evt`, we will need to be careful about that too. Though I suspect it may be fine because if TR imports a `prop:evt` struct with an `Evtof` type, TR always has a protected read end of the event even if it re-exports it elsewhere. If TR itself is defining the struct with `prop:evt`, then it should still be safe because TR will protect the struct mutators.