Check with-handlers better in TR

Now checks that a predicate and handler in the same clause
are consistent (using the filter on the predicate).

Closes PR 13950
Closes PR 14641

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt

@@ -562,12 +562,14 @@ This file defines two sorts of primitives. All of them are provided into any mod
   (syntax-parse stx
     [(_ ([pred? action] ...) . body)
      (with-syntax ([(pred?* ...)
-                    (for/list ([s (in-syntax #'(pred? ...))])
-                      (with-type* s #'(Any -> Any)))]
+                    (for/list ([(pred? idx) (in-indexed (in-syntax #'(pred? ...)))])
+                      (exn-predicate-property pred? idx))]
                    [(action* ...)
-                    (stx-map exn-handler #'(action ...))]
+                    (for/list ([(action idx) (in-indexed (in-syntax #'(action ...)))])
+                      (exn-handler-property action idx))]
                    [body* (exn-body #'(let-values () . body))])
-       (exn-handlers #'(with-handlers ([pred?* action*] ...) body*)))]))
+       (exn-handlers (quasisyntax/loc stx
+                       (with-handlers ([pred?* action*] ...) body*))))]))
 
 (begin-for-syntax
   (define-syntax-class dtsi-struct-name

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/syntax-properties.rkt

@@ -59,7 +59,8 @@
   (type-inst type-inst)
   (type-label type-label)
   (type-dotted type-dotted)
-  (exn-handler typechecker:exn-handler #:mark)
+  (exn-predicate typechecker:exn-predicate)
+  (exn-handler typechecker:exn-handler)
   (exn-body typechecker:exn-body #:mark)
   (exn-handlers typechecker:exn-handlers #:mark)
   (struct-info struct-info)

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-subforms-unit.rkt

@@ -5,22 +5,17 @@
          racket/match
          "signatures.rkt" "tc-metafunctions.rkt"
          "tc-funapp.rkt"
-         (types utils abbrev union resolve)
+         (types utils abbrev union resolve subtype match-expanders)
+         (typecheck check-below)
          (private syntax-properties)
          (utils tc-utils)
          (for-syntax racket/base syntax/parse)
          (for-template racket/base)
-         (rep type-rep))
+         (rep type-rep filter-rep object-rep))
 
 (import tc-if^ tc-lambda^ tc-app^ tc-let^ tc-expr^)
 (export check-subforms^)
 
-;; FIXME -- samth 7/15/11
-;; This code is doing the wrong thing wrt the arguments of exception handlers.
-;; In particular, it allows them to be anything at all, but they might
-;; get called with the wrong kind of arguments by the exception
-;; mechanism.  The right thing is to use the exception predicate.
-
 ;; Does a depth first search of the syntax object. For each sub object it attempts to match it
 ;; against the provide syntax-parse patterns.
 (define-syntax find-syntax
@@ -41,36 +36,95 @@
 ;; find the subexpressions that need to be typechecked in an ignored form
 ;; syntax (or/c #f tc-results/c) -> full-tc-results/c
 (define (check-subforms/with-handlers form expected)
-  (define handler-results '())
+  (define predicate-map (make-hash))
+  (define handler-map (make-hash))
   (define body-results #f)
-  ;; tc-result1 -> tc-results
+
+  ;; syntax tc-result1 type -> tc-results
   ;; The result of applying the function to a single argument of the type of its first argument
-  ;; FIXME: This is the wrong type, see above fixme
-  (define (get-range-result t)
+  (define (get-range-result stx t filter-type)
     (let loop ((t t))
       (match t
         [(Function: (list _ ... (arr: (list arg1) _ _ #f (list (Keyword: _ _ #f) ...)) _ ...))
+         #:when (subtype filter-type arg1)
          (tc/funapp #'here #'(here) t (list (ret arg1)) #f)]
         [(Function: (list _ ... (arr: '() _ (? values rest) #f (list (Keyword: _ _ #f) ...)) _ ...))
+         #:when (subtype filter-type rest)
          (tc/funapp #'here #'(here) t (list (ret rest)) #f)]
         [(? needs-resolving? t)
          (loop (resolve t))]
         [(or (Poly: ns _) (PolyDots: (list ns ... _) _))
          (loop (instantiate-poly t (map (λ (n) Univ) ns)))]
-        [_ (int-err "Unsupported function type in get-result-ty: \n~a" t)])))
+        ;; This clause should raise an error via the check-below test
+        [_
+         (cond [;; a redundant test, but it ensures an error message below
+                (not (subtype t (-> filter-type Univ)))
+                (parameterize ([current-orig-stx stx])
+                  (check-below t (-> filter-type Univ)))]
+               [else (int-err "get-range-result: should not happen. type ~a filter ~a"
+                              t filter-type)])
+         (ret (Un))])))
+
+  ;; Syntax Type -> (Option Type)
+  ;; Extract the type for the filter in a predicate type, or #f if
+  ;; the type is an invalid predicate type.
+  (define (get-filter-type stx pred-type)
+    (cond [;; make sure the predicate has an appropriate type
+           (subtype pred-type (-> Univ Univ))
+           (define fun-type
+             (if (needs-resolving? pred-type)
+                 (resolve pred-type)
+                 pred-type))
+           (match fun-type
+             ;; FIXME: Almost all predicates fall into this case, but it may
+             ;;        be worth being more precise here for some rare code.
+             [(PredicateFilter: fs)
+              (match fs
+                [(FilterSet: (TypeFilter: ft (Path: '() '(0 0))) _) ft]
+                [(Bot:) (Un)]
+                [_ Univ])]
+             [_ Univ])]
+          [else
+           ;; if the type is wrong, produce a nice error message
+           (parameterize ([current-orig-stx stx])
+             (check-below pred-type (-> Univ Univ)))
+           #f]))
+
+  ;; -> (Listof Type)
+  ;; Produce a list of result types from the predicate/handler maps
+  (define (get-handler-results)
+    (for/list ([key (in-hash-keys predicate-map)])
+      (match-define (list predicate-stx predicate-type)
+        (hash-ref predicate-map key))
+      (match-define (list handler-stx handler-type)
+        (hash-ref handler-map key))
+      (define filter-type
+        (get-filter-type predicate-stx predicate-type))
+      ;; if the predicate doesn't check, then don't bother
+      ;; with the RHS and return no result
+      (if filter-type
+          (get-range-result handler-stx handler-type filter-type)
+          (ret (Un)))))
+
   (find-syntax form
     ;; if this needs to be checked
     [stx:with-type^
      ;; the form should be already ascribed the relevant type
      (tc-expr #'stx)]
+    ;; exception predicate
+    [stx:exn-predicate^
+     (match (single-value #'stx)
+       [(tc-result1: t)
+        (hash-set! predicate-map (attribute stx.value) (list #'stx t))])]
     ;; this is a handler function
     [stx:exn-handler^
      (match (single-value #'stx)
        [(tc-result1: t)
-        (set! handler-results (cons (get-range-result t) handler-results))])]
+        (hash-set! handler-map (attribute stx.value) (list #'stx t))])]
     ;; this is the body of the with-handlers
     [stx:exn-body^
      (set! body-results (tc-expr/check #'stx expected))])
+  (define handler-results (get-handler-results))
   (merge-tc-results (cons body-results handler-results)))
 
 ;; typecheck the expansion of a with-handlers form

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/match-expanders.rkt

@@ -10,7 +10,8 @@
          racket/set
          (for-syntax racket/base syntax/parse))
 
-(provide Listof: List: MListof: AnyPoly: AnyPoly-names: Function/arrs:)
+(provide Listof: List: MListof: AnyPoly: AnyPoly-names: Function/arrs:
+         PredicateFilter:)
 
 
 (define-match-expander Listof:
@@ -93,3 +94,11 @@
     (syntax-parse stx
       [(_ doms rngs rests drests kws (~optional (~seq #:arrs arrs) #:defaults ([arrs #'_])))
        #'(Function: (and arrs (list (arr: doms rngs rests drests kws) (... ...))))])))
+
+;; A match expander for matching the filter on a predicate. This assumes a standard
+;; predicate type of the shape (-> Any Any : SomeType)
+(define-match-expander PredicateFilter:
+  (λ (stx)
+    (syntax-parse stx
+      [(_ fs)
+       #'(Function: (list (arr: (list _) (Values: (list (Result: _ fs _))) _ _ _)))])))

pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/metrics.rkt

@@ -75,7 +75,7 @@
 ;; be explained by chance. higher numbers means higher confidence
 ;; that they cannot.
 (define: (chi-square [seqA : (Listof number)] [seqB : (Listof number)]) :  number
-  (with-handlers ([exn:fail? (lambda: ([e : str]) +nan.0)])
+  (with-handlers ([exn:fail? (lambda: ([e : exn]) +nan.0)])
     (let* ([ct-a (length seqA)]
            [ct-b (length seqB)]
            [total-subjects (+ ct-a ct-b)]
@@ -100,7 +100,7 @@
 ;; per-module : path ((listof expr) -> (number | #f)) -> (path -> (listof (number | #f)))  === Unit P
 (pdefine: (X) (per-module [f : ((Listof Sexpr) ->  X )]) : (Path -> (cons (U #f X) '()))
           (lambda: ([path : Path])
-                   (with-handlers ([exn:fail:read? (lambda: ([e : Void]) (list #f))])  ;; with handler
+                   (with-handlers ([exn:fail:read? (lambda: ([e : exn]) (list #f))])  ;; with handler
                      (let ([initial-sexp (with-input-from-file path read)])
                        (match initial-sexp
                          [`(module ,_ ,_  . , (? list? bodies)) ;; FIXME - use ... instead of .

pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/pr12644.rkt

@@ -10,12 +10,12 @@
 (: v (Listof (U inf Number)))
 (define v
   (list
-    (with-handlers ((void add1)) 3)
+    (with-handlers ((number? add1)) 3)
     (with-handlers ((void f)) 4)))
 
 
 (list
   (with-handlers ((void values)) 6)
-  (with-handlers ((void add1)) 7)
+  (with-handlers ((number? add1)) 7)
   (with-handlers ((void f)) 8)
   (with-handlers ((void g)) 9))

pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt

@@ -2953,18 +2953,6 @@
          (ann (for/list ([z #"foobar"]) (add1 z)) (Listof Integer))
          (-lst -Int)]
 
-       [tc-e
-         (with-handlers ([exn:fail? (λ (exn) 4)])
-            5)
-         #:ret (ret -Nat -true-filter)
-         #:expected (ret -Nat -no-filter)]
-
-       [tc-e
-         (with-handlers ([exn:fail? (λ (exn) #f)])
-            5)
-         #:ret (ret Univ -top-filter)
-         #:expected (ret Univ -no-filter)]
-
        [tc-e
          (lambda (a . b) (apply values a b))
 
@@ -3153,6 +3141,40 @@
          (define g (λ (x) (λ () (number? x))))
          (void))
         -Void]
+
+       ;; with-handlers
+       [tc-e
+         (with-handlers ([exn:fail? (λ (exn) 4)])
+            5)
+         #:ret (ret -Nat -true-filter)
+         #:expected (ret -Nat -no-filter)]
+       [tc-e
+         (with-handlers ([exn:fail? (λ (exn) #f)])
+            5)
+         #:ret (ret Univ -top-filter)
+         #:expected (ret Univ -no-filter)]
+       [tc-e
+        (with-handlers ([void (λ: ([x : Any]) #t)]) #f)
+        -Boolean]
+       [tc-err
+        (with-handlers ([values (lambda: ([e : String]) (string-append e "bar"))])
+          (raise "foo"))
+        #:msg #rx"expected: \\(-> Any Any\\).*given: \\(-> String String\\)"]
+       [tc-err
+        (with-handlers (["foo" (lambda: ([e : String]) (string-append e "bar"))])
+          (raise "foo"))
+        #:msg #rx"expected: \\(-> Any Any\\).*given: String"]
+       [tc-err
+        (with-handlers ([string? (lambda (e) (string-append e "bar"))])
+          (raise "foo"))
+        #:ret (ret -String)
+        #:msg #rx"expected: String.*given: Any"]
+       [tc-err
+        (with-handlers ([string? (lambda: ([e : String]) (string-append e "bar"))]
+                        [symbol? (lambda (x) (symbol->string x))])
+          (raise 'foo))
+        #:ret (ret -String)
+        #:msg #rx"expected: Symbol.*given: Any"]
         )
 
   (test-suite