diff --git a/collects/tests/typed-racket/fail/pr12706.rkt b/collects/tests/typed-racket/fail/pr12706.rkt new file mode 100644 index 0000000000..40e71b5f79 --- /dev/null +++ b/collects/tests/typed-racket/fail/pr12706.rkt @@ -0,0 +1,10 @@ +#; +(exn-pred 2) +#lang typed/racket + +(: foo (Nonnegative-Float -> Nonnegative-Float)) +(define (foo x) + (cond [(> x 0.0) 1.0] + [else (ann x String)])) + +(foo 0.0) diff --git a/collects/typed-racket/base-env/base-env-numeric.rkt b/collects/typed-racket/base-env/base-env-numeric.rkt index 3a55f923e7..aa03ea9f90 100644 --- a/collects/typed-racket/base-env/base-env-numeric.rkt +++ b/collects/typed-racket/base-env/base-env-numeric.rkt @@ -473,58 +473,58 @@ (define fl<-type (lambda () (from-cases - (-> -FlonumZero -Flonum B : (-FS (-filter -PosFlonum 1) (-filter (Un -NonPosFlonum -FlonumPosZero) 1))) - (-> -Flonum -FlonumZero B : (-FS (-filter -NegFlonum 0) (-filter (Un -NonNegFlonum -FlonumNegZero) 0))) + (-> -FlonumZero -Flonum B : (-FS (-filter -PosFlonum 1) (-filter -NonPosFlonum 1))) + (-> -Flonum -FlonumZero B : (-FS (-filter -NegFlonum 0) (-filter -NonNegFlonum 0))) (-> -PosFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top)) (-> -Flonum -PosFlonum B : (-FS -top (-filter -PosFlonum 0))) (-> -NonNegFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top)) - (-> -Flonum -NonNegFlonum B : (-FS -top (-filter (Un -NonNegFlonum -FlonumNegZero) 0))) + (-> -Flonum -NonNegFlonum B : (-FS -top (-filter -NonNegFlonum 0))) (-> -NegFlonum -Flonum B : (-FS -top (-filter -NegFlonum 1))) (-> -Flonum -NegFlonum B : (-FS (-filter -NegFlonum 0) -top)) - (-> -NonPosFlonum -Flonum B : (-FS -top (-filter (Un -NonPosFlonum -FlonumPosZero) 1))) + (-> -NonPosFlonum -Flonum B : (-FS -top (-filter -NonPosFlonum 1))) (-> -Flonum -NonPosFlonum B : (-FS (-filter -NegFlonum 0) -top)) (comp -Flonum)))) (define fl>-type (lambda () (from-cases - (-> -FlonumZero -Flonum B : (-FS (-filter -NegFlonum 1) (-filter (Un -NonNegFlonum -FlonumNegZero) 1))) - (-> -Flonum -FlonumZero B : (-FS (-filter -PosFlonum 0) (-filter (Un -NonPosFlonum -FlonumPosZero) 0))) + (-> -FlonumZero -Flonum B : (-FS (-filter -NegFlonum 1) (-filter -NonNegFlonum 1))) + (-> -Flonum -FlonumZero B : (-FS (-filter -PosFlonum 0) (-filter -NonPosFlonum 0))) (-> -PosFlonum -Flonum B : (-FS -top (-filter -PosFlonum 1))) (-> -Flonum -PosFlonum B : (-FS (-filter -PosFlonum 0) -top)) - (-> -NonNegFlonum -Flonum B : (-FS -top (-filter (Un -NonNegFlonum -FlonumNegZero) 1))) + (-> -NonNegFlonum -Flonum B : (-FS -top (-filter -NonNegFlonum 1))) (-> -Flonum -NonNegFlonum B : (-FS (-filter -PosFlonum 0) -top)) (-> -NegFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top)) (-> -Flonum -NegFlonum B : (-FS -top (-filter -NegFlonum 0))) (-> -NonPosFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top)) - (-> -Flonum -NonPosFlonum B : (-FS -top (-filter (Un -NonPosFlonum -FlonumPosZero) 0))) + (-> -Flonum -NonPosFlonum B : (-FS -top (-filter -NonPosFlonum 0))) (comp -Flonum)))) (define fl<=-type (lambda () (from-cases - (-> -FlonumZero -Flonum B : (-FS (-filter (Un -NonNegFlonum -FlonumNegZero) 1) (-filter -NegFlonum 1))) - (-> -Flonum -FlonumZero B : (-FS (-filter (Un -NonPosFlonum -FlonumPosZero) 0) (-filter -PosFlonum 0))) + (-> -FlonumZero -Flonum B : (-FS (-filter -NonNegFlonum 1) (-filter -NegFlonum 1))) + (-> -Flonum -FlonumZero B : (-FS (-filter -NonPosFlonum 0) (-filter -PosFlonum 0))) (-> -PosFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top)) (-> -Flonum -PosFlonum B : (-FS -top (-filter -PosFlonum 0))) - (-> -NonNegFlonum -Flonum B : (-FS (-filter (Un -NonNegFlonum -FlonumNegZero) 1) -top)) + (-> -NonNegFlonum -Flonum B : (-FS (-filter -NonNegFlonum 1) -top)) (-> -Flonum -NonNegFlonum B : (-FS -top (-filter -PosFlonum 0))) (-> -NegFlonum -Flonum B : (-FS -top (-filter -NegFlonum 1))) (-> -Flonum -NegFlonum B : (-FS (-filter -NegFlonum 0) -top)) (-> -NonPosFlonum -Flonum B : (-FS -top (-filter -NegFlonum 1))) - (-> -Flonum -NonPosFlonum B : (-FS (-filter (Un -NonPosFlonum -FlonumPosZero) 0) -top)) + (-> -Flonum -NonPosFlonum B : (-FS (-filter -NonPosFlonum 0) -top)) (comp -Flonum)))) (define fl>=-type (lambda () (from-cases - (-> -FlonumZero -Flonum B : (-FS (-filter (Un -NonPosFlonum -FlonumPosZero) 1) (-filter -PosFlonum 1))) - (-> -Flonum -FlonumZero B : (-FS (-filter (Un -NonNegFlonum -FlonumNegZero) 0) (-filter -NegFlonum 0))) + (-> -FlonumZero -Flonum B : (-FS (-filter -NonPosFlonum 1) (-filter -PosFlonum 1))) + (-> -Flonum -FlonumZero B : (-FS (-filter -NonNegFlonum 0) (-filter -NegFlonum 0))) (-> -PosFlonum -Flonum B : (-FS -top (-filter -PosFlonum 1))) (-> -Flonum -PosFlonum B : (-FS (-filter -PosFlonum 0) -top)) (-> -NonNegFlonum -Flonum B : (-FS -top (-filter -PosFlonum 1))) - (-> -Flonum -NonNegFlonum B : (-FS (-filter (Un -NonNegFlonum -FlonumNegZero) 0) -top)) + (-> -Flonum -NonNegFlonum B : (-FS (-filter -NonNegFlonum 0) -top)) (-> -NegFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top)) (-> -Flonum -NegFlonum B : (-FS -top (-filter -NegFlonum 0))) (-> -NonPosFlonum -Flonum B : (-FS -top (-filter -PosFlonum 1))) - (-> -Flonum -NonPosFlonum B : (-FS (-filter (Un -NonPosFlonum -FlonumPosZero) 0) -top)) + (-> -Flonum -NonPosFlonum B : (-FS (-filter -NonPosFlonum 0) -top)) (comp -Flonum)))) (define flmin-type (lambda () @@ -556,7 +556,7 @@ (unop -Flonum)))) (define flexp-type (lambda () - (from-cases ((Un -NonNegFlonum -FlonumNegZero) . -> . -PosFlonum) + (from-cases (-NonNegFlonum . -> . -PosFlonum) (-NegFlonum . -> . -NonNegFlonum) (-Flonum . -> . -Flonum)))) ; nan is the only non nonnegative case (returns nan) (define flsqrt-type @@ -1192,24 +1192,22 @@ ;; we could add cases to encode that (commutative-case -PosFlonum -Flonum) (varop -NonNegFlonum) - ;; the following case is not guaranteed to return a NonNegFlonum - ;; here's an example: (max 0.0 -0.0) -> -0.0 - (commutative-case (Un -NonNegFlonum -FlonumNegZero) -Flonum) + (commutative-case -NonNegFlonum -Flonum) (map varop (list -NegFlonum -NonPosFlonum -Flonum -SingleFlonumPosZero -SingleFlonumNegZero -SingleFlonumZero)) (commutative-case -PosSingleFlonum -SingleFlonum) (varop -NonNegSingleFlonum) - (commutative-case (Un -NonNegSingleFlonum -SingleFlonumNegZero) -SingleFlonum) + (commutative-case -NonNegSingleFlonum -SingleFlonum) (map varop (list -NegSingleFlonum -NonPosSingleFlonum -SingleFlonum -InexactRealPosZero -InexactRealNegZero -InexactRealZero)) (commutative-case -PosInexactReal -InexactReal) (varop -NonNegInexactReal) - (commutative-case (Un -NonNegInexactReal -InexactRealNegZero) -InexactReal) + (commutative-case -NonNegInexactReal -InexactReal) (map varop (list -NegInexactReal -NonPosInexactReal -InexactReal -RealZero)) (commutative-case -PosReal -Real) (varop -NonNegReal) - (commutative-case (Un -NonNegReal -RealZero) -InexactReal) + (commutative-case -NonNegReal -InexactReal) (map varop (list -NegReal -NonPosReal -Real)))] [min (from-cases (map varop (list -Zero -One)) @@ -1225,24 +1223,24 @@ -PosFlonum -NonNegFlonum)) (commutative-case -NegFlonum -Flonum) (varop -NonPosFlonum) - (commutative-case (Un -NonPosFlonum -FlonumPosZero) -Flonum) + (commutative-case -NonPosFlonum -Flonum) (map varop (list -Flonum -SingleFlonumPosZero -SingleFlonumNegZero -SingleFlonumZero -PosSingleFlonum -NonNegSingleFlonum)) (commutative-case -NegSingleFlonum -SingleFlonum) (varop -NonPosSingleFlonum) - (commutative-case (Un -NonPosSingleFlonum -SingleFlonumPosZero) -SingleFlonum) + (commutative-case -NonPosSingleFlonum -SingleFlonum) (map varop (list -SingleFlonum -InexactRealPosZero -InexactRealNegZero -InexactRealZero -PosInexactReal -NonNegInexactReal)) (commutative-case -NegInexactReal -InexactReal) (varop -NonPosInexactReal) - (commutative-case (Un -NonPosInexactReal -InexactRealPosZero) -InexactReal) + (commutative-case -NonPosInexactReal -InexactReal) (map varop (list -InexactReal -RealZero -PosReal -NonNegReal)) (commutative-case -NegReal -Real) (varop -NonPosReal) - (commutative-case (Un -NonPosReal -RealZero) -Real) + (commutative-case -NonPosReal -Real) (varop -Real))] [add1 (from-cases diff --git a/collects/typed-racket/types/numeric-tower.rkt b/collects/typed-racket/types/numeric-tower.rkt index 651aa6ac59..a8e30ccc74 100644 --- a/collects/typed-racket/types/numeric-tower.rkt +++ b/collects/typed-racket/types/numeric-tower.rkt @@ -149,13 +149,13 @@ #'(and/c flonum? positive?) (lambda (x) (and (flonum? x) (positive? x))) #'-PosFlonum)) -(define -NonNegFlonum (*Un -PosFlonum -FlonumPosZero)) +(define -NonNegFlonum (*Un -PosFlonum -FlonumZero)) (define -NegFlonum (make-Base 'Negative-Float #'(and/c flonum? negative?) (lambda (x) (and (flonum? x) (negative? x))) #'-NegFlonum)) -(define -NonPosFlonum (*Un -NegFlonum -FlonumNegZero)) +(define -NonPosFlonum (*Un -NegFlonum -FlonumZero)) (define -Flonum (*Un -NegFlonum -FlonumNegZero -FlonumPosZero -PosFlonum -FlonumNan)) ; 64-bit floats ;; inexact reals can be flonums (64-bit floats) or 32-bit floats (define -SingleFlonumPosZero ; disjoint from Flonum 0s @@ -187,16 +187,16 @@ (lambda (x) #f) #'-PosSingleFlonum)) (define -PosInexactReal (*Un -PosSingleFlonum -PosFlonum)) -(define -NonNegSingleFlonum (*Un -PosSingleFlonum -SingleFlonumPosZero)) -(define -NonNegInexactReal (*Un -PosInexactReal -InexactRealPosZero)) +(define -NonNegSingleFlonum (*Un -PosSingleFlonum -SingleFlonumZero)) +(define -NonNegInexactReal (*Un -PosInexactReal -InexactRealZero)) (define -NegSingleFlonum (make-Base 'Negative-Single-Flonum #'(and/c single-flonum? negative?) (lambda (x) #f) #'-NegSingleFlonum)) (define -NegInexactReal (*Un -NegSingleFlonum -NegFlonum)) -(define -NonPosSingleFlonum (*Un -NegSingleFlonum -SingleFlonumNegZero)) -(define -NonPosInexactReal (*Un -NegInexactReal -InexactRealNegZero)) +(define -NonPosSingleFlonum (*Un -NegSingleFlonum -SingleFlonumZero)) +(define -NonPosInexactReal (*Un -NegInexactReal -InexactRealZero)) (define -SingleFlonum (*Un -NegSingleFlonum -SingleFlonumNegZero -SingleFlonumPosZero -PosSingleFlonum -SingleFlonumNan)) (define -InexactReal (*Un -SingleFlonum -Flonum))