[racket] filters in typed racket

Is there a way of specifying filters in typed racket so that if it returns true, it knows it’s a certain type, but if it returns false, it doesn’t mean that it’s not that type (or the other way around).  

For example:
(: string-with-length-1? (Any -> Boolean : #:if-true String #:if-false (U String Any)))
(define (string-with-length-1? x)
  (if (string? x)
      (one? (string-length x))
      #f))

I know there’s something like this somewhere.

When I tried it, it gave me an error message (I expected that), but that error message said something about #:+ and #:-

After trying some stuff and guessing stuff from error messages, and just to try it and see what happened, I tried this:  
(: string-with-length-1? (Any -> Boolean : #:+ (String @ x) #:- ((U String Any) @ x)))
(define (string-with-length-1? x)
  (if (string? x)
      (one? (string-length x))
      #f))
And it gave me this weird error message:
. Type Checker: type mismatch;
 mismatch in filter
  expected: ((String @ x) | Top)
  given: ((String @ x) | Top) in: (if (string? x) (one? (string-length x)) #f)

What?  If it’s expecting ((String @ x) | Top), and I’m giving it ((String @ x) | Top),  then what’s the problem?

And is there any documentation anywhere about this?


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20140510/7cd8c3ba/attachment.html>