[plt-scheme] Type scheme annotations and macros

A couple quick questions on Typed Scheme:

1) Why does the first type-check while the latter does not?

#lang typed-scheme
(if #f
     (add1 "dog")
     'ok)

#;
(if (ann #f #f)
     (add1 "dog")
     'ok)

2) How can I write a `bif' macro that works like Typed Scheme's if (ie. 
types its branches with occurrence typing), but forces the conditional 
value to be a Boolean and nothing but a Boolean?

(define-syntax bif
   (syntax-rules ()
     [(bif e0 e1 e2)
      (if (ann e0 Boolean)
          e1
          e2)]))

This enforces a Boolean type on e0, but seems to destroy the occurrence 
typing of e1 and e2.

Thanks,
David