Why does Typed Racket think that `cond` can return `Void` here?

Question

Typed Racket seems to think that this conditional can return Void. Why?

#lang typed/racket

(define x : Real 1234)

(+ 4 (cond [(< x 5) 5]
           [(<= 5 x) 10]))

... produces the error

Type Checker: type mismatch
  expected: Number
  given: (U Positive-Byte Void) in: (cond ((< x 5) 5) ((<= 5 x) 10))

Why?

Answer 1

The issue here is that for historical reasons, cond will return the (void) value when all of the test clauses fail. Looking at this code, you'll probably say "But wait! That's impossible! Every real number must either be (< 5) or (>= 5), right?" Well, that's true, but that's not something that Typed Racket can reason about within the bounds of its type system.

So, what do you do? Well, in this case it's pretty easy to share your knowledge with Typed Racket. Just change that last test into an else clause, which TR can see must always succeed:

#lang typed/racket

(define x : Real 1234)

(+ 4 (cond [(< x 5) 5]
           [else 10]))

... which type-checks and runs fine.