[racket-dev] Machinery for eliding contracts

One of the slowest parts when using TR is the contract boundary
between untyped and typed code. Even with recent changes it still
causes a large overhead.

Example:
#lang racket/load

(module lib typed/racket
  (provide f g)
  (: f (Symbol -> (Boxof Symbol)))
  (define (f x) (box x))
  (: g ((Boxof Symbol) -> Symbol))
  (define (g x) (unbox x)))

(module user-1 racket
  (provide go1)
  (require 'lib)
  (define (go1)
    (for ((i (in-range 200000)))
      (g (f 'x)))))

(module user-2 typed/racket
  (provide go2)
  (require 'lib)
  (define (go2)
    (for ((i (in-range 100000000)))
      (g (f 'x)))))

(require 'user-1 'user-2)

(for ((j 5))
  (time (go1))
  (time (go2)))


It would be nice if the contract on the input to g could be elided. It
seems like this could be done by using something like prop:contracted
but that allowed accessing the parties that agreed to the contract.

I'm imagining something like
(lambda (v) (and (has-contract? v) (contracted-value-providing-side=?
v 'the-typed-world) (contract-stronger? (value-contract v)
new-contract)))

One issue I see is that we need an unforgeable property that the value
actually came from the typed world so we know that eliding the new
contract is safe.

Does this seem like a reasonable thing to support/do people see issues with it?

Other related ideas I had were:

A similar thing could be done if the same contract were being applied
multiple times with the same blame parties. In that case the later
contracts could be elided because they would error out in exactly the
same cases with exactly the same messages.

That in addition to not applying the new contract if it is weaker than
the old contract, we remove the old contract (and access the
unprotected value) if the new contract is stronger. In the case that
they were the same contract this would mean that there would be no
higher order contract checks while the typed code was executing.