[racket] `assert', `and' and `or' in Typed Racket

Hi everyone,

I've been starting out learning Typed Racket, which I've enjoyed quite a
lot -- thanks!

I've run into a snag several times now that I wanted to ask the experts
about: does TR know about short-circuiting `and' and `or'?  (If not, why
not?)  If so, how do they interact with `assert'?

Here's the example I'm working with:

#lang typed/racket
(: try-read ((U String Regexp PRegexp) Input-Port -> (U String False)))
(define (try-read re ip)
  (let* ([m (regexp-try-match re ip)]
         [v (and m (car m))]
         [s (and v (bytes->string/utf-8 v))])
    (and (assert s string?) 
         (not (string=? s "")) 
         s)))          ;^ type check fails here


This example fails to type check, with the message "Expected String, but
got (U String False) in: s".  I would have thought that TR would be able
to infer that, if the `(not ...)' form is reached, `s' must be a string,
due to the short-circuiting nature of `and'.

[pause for some tinkering...]

Curiously, if I change `(assert s string?)' to `(string? s)', the
example passes the type check.  So I guess maybe the short-circuiting
nature of `and' and `or' is a red herring here, and what I don't
understand is something about `assert'.  What makes for the difference
between `(assert s string?)' and `(string? s)'?

I thought that the difference was that `(assert s string?)' performs a
type check at macro expansion time on the type of the expression `s', in
addition to performing the dynamic check that `(string? s)' does at
runtime.  But if that's right, then why doesn't the type check fail on
the `assert' form in the `and' expression, rather than on the second
form?  That is, if the type of `s' is known to be (U String False) by
the time the second form is type checked, why doesn't the assertion in
the first form fail the type check?

Thanks!

Richard