Ben Greenman

Yes, very rudimentary. https://github.com/bennn/require-typed-scv/blob/master/private/parse-type.rkt#L17 Just parses surface syntax. It would be better to parse expanded TR syntax ... and I think that is the best we could do without changing...

Also, trying to verify a module that depends on another module that uses classes will raise an exception about `protect-out` (because Racket's `class-internal.rkt` happens to use a `protect-out`) ### Example...

Just tried this program. It's rejected. Then I tried changing `(>=/c 4)` to `(>=/c 5)` and it's still rejected (new issue?)

More examples, from #86 ### Keyword args ``` #lang racket/base (define (f #:x x) x) ``` Error message: ``` /..../racket/collects/racket/private/kw.rkt:251:10: parser: don't know what this identifier means. It is possibly...

Question: why is "write contracts" a task? I mean, why not use the types from the benchmarks? I've looked at your [sieve](https://github.com/philnguyen/soft-contract/blob/afee86a290f999e43b5f19a38a9911264200577e/soft-contract/test/gradual-typing-benchmarks/sieve/streams.rkt) and [morsecode](https://github.com/philnguyen/soft-contract/blob/afee86a290f999e43b5f19a38a9911264200577e/soft-contract/test/gradual-typing-benchmarks/morsecode/morse-code-table.rkt#L7) but I'm not sure if you're...

Also, FYI, I'm hoping to run these benchmarks "as-is" through soft contracts and I started a mapping from contracts to Typed Racket syntax [here](https://github.com/bennn/require-typed-scv).

Pushed with `~e` for the predicate in https://github.com/racket/typed-racket/commit/4165b6baa0c79e7391d990d76d74c483592145c1

One response to the 2020 TR survey (out of 106 total) asked for this feature too.

Those are my comments & tests. If `box/sc` is no longer invariant, they need to be updated. The idea with the tests is: - if there's an `(or/sc sc_0 sc_1)`...

yes