Allow user to write new pair filter objects

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)
+  (pattern (t:expr (~describe "@" (~datum @)) pe:path-elem ... i:idx-obj)
-           #:fail-unless (< (syntax-e #'i) (length doms))
+           #: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))
+                   (attribute i.arg) (length doms))
-           #:attr prop (-filter (parse-type #'t) (syntax-e #'i) (attribute pe.pe)))
+           #: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)
+  (pattern ((~datum !) t:expr (~describe "@" (~datum @)) pe:path-elem ... i:idx-obj)
-           #:fail-unless (< (syntax-e #'i) (length doms))
+           #: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))
+                   (attribute i.arg) (length doms))
-           #:attr prop (-not-filter (parse-type #'t) (syntax-e #'i) (attribute pe.pe)))
+           #: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)) ...)

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"