plt/racket — pull request #516 by takikawa (2013-12-13 21:56:09+00:00)
Title: Add support for base type environment bindings in Typed Racket that have contracts already attached

This PR is for code review.

Right now, contracted identifiers like `~a` cannot be imported into TR's base type environment. They only work with `require/typed`.

This is because contracted identifiers are really bound to transformers which lift into an expression that actually produces the value. TR may have a type assigned for the transformer identifier, but the resulting expression contains identifiers with no type information.

These commits allow the contract system to inform TR what transformer identifier resulted in the lifting, so that TR can assume the resulting expression has the same type that the base type environment records.

This should be sound if the following assumptions are met: (1) TR only allows untyped identifiers to have a type if they are in the base type environment or brought in with `require/typed` (I think this is true), and (2) the contracted identifiers have chaperone contracts, so that their "type" cannot change (or just assign a type where that's ok).

With these changes, something like this type-checks:
````
(module a typed/racket (~a 3 "foo" 5))
````

Doesn't work at the top-level yet because TR's top-level and lifting don't fit together well yet.

Relevant people for this PR: @rfindler @samth