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?
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.