Can you add a test of the new functionality?

I tried adding this test to typecheck-tests.rkt

        [tc-e (let ([pos-not-5? : [-> Real (U Positive-Real #f) : #:+ Positive-Real]
                                (λ (x) (and (positive? x) (not (= x 5)) x))])
                (partition pos-not-5? '(1 2 -3 4 5 -6)))
              (-values (list -PosReal -Real))]

But I got a failure including this error:

. . ../../../../../../../../../../Applications/Racket/2015-05-17/Racket v6.2.0.3/collects/racket/private/for.rkt:585:2: in-list: contract violation
  expected: list?
  given: (values (U 1 Byte-Larger-Than-One Positive-Index-Not-Byte Positive-Fixnum-Not-Index Positive-Integer-Not-Fixnum Positive-Rational-Not-Integer Float-Nan Positive-Float-No-NaN Single-Flonum-Nan Positive-Single-Flonum-No-Nan) (U 0 1 Byte-Larger-Than-...

What am I doing wrong?

Ok, I figured out that I'm not supposed to use -values for this. I also realized that I put -PosReal and -Real where I should have put (-lst -PosReal) and (-lst -Real).

I also had to switch the order of the cases in the type of partition to get it to infer the right type without an explicit annotation.

Looks good to me.

When committing this, try to avoid creating a merge commit (usually done by rebasing before pushing).

I don't think rebasing first helps, does it? That's what I've done before for pull requests (and that's also what I did for this one) and it still creates the merge commit. I can try pushing directly to the racket/typed-racket repo though.