diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt index 69240d78..b9ba8707 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt @@ -104,6 +104,19 @@ (pattern cdr #:attr pe (make-CdrPE))) +(define-splicing-syntax-class idx-obj + #:description "index object" + #:attributes (arg depth pair) + (pattern (~seq idx:nat) + #:attr arg (syntax-e #'idx) + #:attr depth 0 + #:attr pair (list 0 (syntax-e #'idx))) + (pattern (~seq depth-idx:nat idx:nat) + #:attr arg (syntax-e #'idx) + #:attr depth (syntax-e #'depth-idx) + #:attr pair (list (syntax-e #'depth-idx) + (syntax-e #'idx)))) + (define-splicing-syntax-class simple-latent-filter #:description "latent filter" (pattern (~seq t:expr (~describe "@" (~datum @)) pe:path-elem ...) @@ -118,18 +131,18 @@ #:attributes (prop) (pattern (~literal Top) #:attr prop -top) (pattern (~literal Bot) #:attr prop -bot) - (pattern (t:expr (~describe "@" (~datum @)) pe:path-elem ... i:nat) - #:fail-unless (< (syntax-e #'i) (length doms)) + (pattern (t:expr (~describe "@" (~datum @)) pe:path-elem ... i:idx-obj) + #:fail-unless (< (attribute i.arg) (length doms)) (format "Filter proposition's object index ~a is larger than argument length ~a" - (syntax-e #'i) (length doms)) - #:attr prop (-filter (parse-type #'t) (syntax-e #'i) (attribute pe.pe))) + (attribute i.arg) (length doms)) + #:attr prop (-filter (parse-type #'t) (attribute i.pair) (attribute pe.pe))) (pattern (t:expr (~describe "@" (~datum @)) pe:path-elem ... i:id) #:attr prop (-filter (parse-type #'t) #'i (attribute pe.pe))) - (pattern ((~datum !) t:expr (~describe "@" (~datum @)) pe:path-elem ... i:nat) - #:fail-unless (< (syntax-e #'i) (length doms)) + (pattern ((~datum !) t:expr (~describe "@" (~datum @)) pe:path-elem ... i:idx-obj) + #:fail-unless (< (attribute i.arg) (length doms)) (format "Filter proposition's object index ~a is larger than argument length ~a" - (syntax-e #'i) (length doms)) - #:attr prop (-not-filter (parse-type #'t) (syntax-e #'i) (attribute pe.pe))) + (attribute i.arg) (length doms)) + #:attr prop (-not-filter (parse-type #'t) (attribute i.pair) (attribute pe.pe))) (pattern ((~datum !) t:expr (~describe "@" (~datum @)) pe:path-elem ... i:id) #:attr prop (-not-filter (parse-type #'t) #'i (attribute pe.pe))) (pattern ((~literal and) (~var p (prop doms)) ...) diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt index 61acfdef..590b500f 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt @@ -1780,6 +1780,22 @@ (void)) ;; type doesn't really matter, just make sure it typechecks -Void] + + ;; The following ensures that the correct filter can be + ;; written by the user + [tc-e + (let () + (: f (Any -> (Any -> Boolean : #:+ (Number @ 1 0) + #:- (! Number @ 1 0)) + : #:+ Top #:- Bot)) + (define f (λ (x) (λ (y) (number? x)))) + (: b (U Number String)) + (define b 5) + (define g (f b)) + (if (g "foo") (add1 b) 3) + (void)) + ;; type doesn't really matter, just make sure it typechecks + -Void] ) (test-suite "tc-literal tests"