That said, I'm going to take the opportunity to ask a question: does Pyret's gradual typing cover parametric polymorphism and mutable data structures? Those usually are specially though to do in these fully gradual systems so I'm curious what you guys have done about that.
Re. your other question, yes, this is a wide-open problem, and we're trying to not get bogged down in research issues like this. We actually have one answer about what to do, presented in a paper we wrote some time ago (http://cs.brown.edu/~sk/Publications/Papers/Published/gmfk-r...), but we don't really want to do that. But because we're working on a (curious) type inference story, we may be able to carve up this problem in a very different way.
Sorry for the non-answer. You're right, and we're working on it.
In fact, we'd really love it if gradual typing folks would tell us what set of primitives they miss in a language. They aren't constrained to what Racket or Python or whatever; there may be a primitive that makes sense that Pyret can add to enable space-efficient, semantically-meaningful contracting or gradual typing in the presence of such operations.
Though I'm not enamored of the Typed Racket style of wrapping everything at the boundary (even as I appreciate why it's there). Not even hypothetical: we actually began developing Pyret in TR but, with great sadness, ended up having to move it out because of the enormous performance hits.
And yes, soundness + interoperation + structural types = heavy performance cost. You can give up on one of those easily, but the combination can't be free.
But the best way to make TR programs not pay that cost is to not cross the boundary all the time, which it sounds like is what you were doing. Why was that necessary?