[racket-dev] typed racket non-monotonic in scary way?

I was trying to write a function on natural numbers today, and came up with an example that scares me all to bits. This program:

#lang typed/racket

(: int->nat (Natural -> Natural))
(define (int->nat n)
  (cond [(<= n 0) 13]
        [else (- n 1)]))

Does not type-check, because (- n 1) has type Integer rather than Natural. Well, too bad, but sort of okay. But then:

#lang typed/racket

(: int->nat (Integer -> Natural))
(define (int->nat n)
  (cond [(<= n 0) 13]
        [else (- n 1)]))

*does* typecheck. AIIEE! As far as I can tell, Integer is a supertype of Natural, so I would expect that things that typecheck with Integer inputs should also typecheck with Natural inputs.

Please please tell me this is a bug? I can imagine a world where it's not a bug, but the difficulty of using the type system would skyrocket if you have to consider *widening* types as well as narrowing them to get things to work.

No?

John
 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4800 bytes
Desc: not available
URL: <http://lists.racket-lang.org/dev/archive/attachments/20120907/47fe6a7e/attachment.p7s>