[racket] Typed Racket: limited polymorphism?

On Jun 14, 2011, at 5:41 PM, Sam Tobin-Hochstadt wrote:

>> 
> 
> #lang typed/racket
> (define-type SN (U String Number))
> (define-predicate sn? SN)
> (struct: (α) node ({left : α} {right : α}))
> 
> (: create-node (All (β) (β β -> (node SN))))
> (define (create-node x y)
>  (if (and (sn? x) (sn? y))
>      (node x y)
>      (error 'bad "")))
> 
> Unfortunately, Typed Racket doesn't know that the function Matthias
> wrote never returns if `x' and `y' aren't in `SN', so his version
> won't typecheck, regardless of the bug he's found.

That's the version I had first. Then I thought I'd trick it into believing me with begin0 and unless. 

Why doesn't error return empty and then it all works out? BTW, the SN should be a beta.