diff --git a/typed-racket-lib/typed-racket/core.rkt b/typed-racket-lib/typed-racket/core.rkt
index 4e3758ad2..bd5ef1496 100644
--- a/typed-racket-lib/typed-racket/core.rkt
+++ b/typed-racket-lib/typed-racket/core.rkt
@@ -48,10 +48,12 @@
                                      (and (attribute opt?) (syntax-e (attribute opt?))))]
                       [with-refinements? (and (or (attribute refinement-reasoning?)
                                                   (with-refinements?))
-                                              (when (not (eq? te-mode deep))
+                                              (unless (eq? te-mode deep)
                                                 (raise-arguments-error
-                                                  (string->symbol (format "typed/racket/~a" (keyword->string (syntax-e te-attr))))
-                                                  "#:with-refinements unsupported")))])
+                                                 (string->symbol (format "typed/racket/~a"
+                                                                         (keyword->string
+                                                                          (syntax-e te-attr))))
+                                                 "#:with-refinements unsupported")))])
          (tc-module/full te-mode stx pmb-form
           (λ (new-mod pre-before-code pre-after-code)
             (define ctc-cache (make-hash))
diff --git a/typed-racket-lib/typed-racket/static-contracts/combinators/unit.rkt b/typed-racket-lib/typed-racket/static-contracts/combinators/unit.rkt
index 8ea8181bf..b55e2e4bd 100644
--- a/typed-racket-lib/typed-racket/static-contracts/combinators/unit.rkt
+++ b/typed-racket-lib/typed-racket/static-contracts/combinators/unit.rkt
@@ -61,10 +61,9 @@
                                             (list invoke/scs ...)))
     v)
   (define (sig-spec->syntax sig-spec)
-    (match sig-spec
-      [(signature-spec name members scs)
-       (define member-stx (map (lambda (id sc) #`(#,id #,(f sc))) members scs))
-       #`(#,name #,@member-stx)]))
+    (match-define (signature-spec name members scs) sig-spec)
+    (define member-stx (map (lambda (id sc) #`(#,id #,(f sc))) members scs))
+    #`(#,name #,@member-stx))
 
   (define (invokes->contract lst)
     (cond
diff --git a/typed-racket-lib/typed-racket/tc-setup.rkt b/typed-racket-lib/typed-racket/tc-setup.rkt
index 197f2ea2d..6f2b123f1 100644
--- a/typed-racket-lib/typed-racket/tc-setup.rkt
+++ b/typed-racket-lib/typed-racket/tc-setup.rkt
@@ -36,15 +36,15 @@
   ;; types are enforced (not no-check etc.),
   ;; PLT_TR_NO_OPTIMIZE is not set, and the
   ;; current code inspector has sufficient privileges
-  (if (and (optimize?)
-           (memq (current-type-enforcement-mode) (list deep shallow))
-           (not (getenv "PLT_TR_NO_OPTIMIZE"))
-           (authorized-code-inspector?))
-      (begin
-        (do-time "Starting optimizer")
-        (begin0 (stx-map optimize-top body)
-          (do-time "Optimized")))
-      body))
+  (cond
+    [(and (optimize?)
+          (memq (current-type-enforcement-mode) (list deep shallow))
+          (not (getenv "PLT_TR_NO_OPTIMIZE"))
+          (authorized-code-inspector?))
+     (do-time "Starting optimizer")
+     (begin0 (stx-map optimize-top body)
+       (do-time "Optimized"))]
+    [else body]))
 
 (define (maybe-shallow-rewrite body-stx ctc-cache)
   (case (current-type-enforcement-mode)
diff --git a/typed-racket-lib/typed-racket/typecheck/check-below.rkt b/typed-racket-lib/typed-racket/typecheck/check-below.rkt
index 0c8bab2e5..c3be99ddf 100644
--- a/typed-racket-lib/typed-racket/typecheck/check-below.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/check-below.rkt
@@ -129,19 +129,16 @@
     [((tc-result1: t1 p1 o1) (tc-result1: t2 p2 o2))
      (define (perform-check!)
        (cond
-         [(not (subtype t1 t2 o1))
-          (expected-but-got t2 t1)]
-         [(and (not (prop-set-better? p1 p2))
-               (object-better? o1 o2))
+         [(not (subtype t1 t2 o1)) (expected-but-got t2 t1)]
+         [(and (not (prop-set-better? p1 p2)) (object-better? o1 o2))
           (type-mismatch p2 p1 "mismatch in proposition")]
-         [(and (prop-set-better? p1 p2)
-               (not (object-better? o1 o2)))
+         [(and (prop-set-better? p1 p2) (not (object-better? o1 o2)))
           (type-mismatch (print-object o2) (print-object o1) "mismatch in object")]
-         [(and (not (prop-set-better? p1 p2))
-               (not (object-better? o1 o2)))
+         [(and (not (prop-set-better? p1 p2)) (not (object-better? o1 o2)))
           (type-mismatch (format "`~a' and `~a'" p2 (print-object o2))
                          (format "`~a' and `~a'" p1 (print-object o1))
-                         "mismatch in proposition and object")])
+                         "mismatch in proposition and object")]
+         [else (void)])
        (ret (upgrade-trusted-rng t1 t2) (fix-props p2 p1) (fix-object o2 o1)))
      (cond
        [(with-refinements?)
diff --git a/typed-racket-lib/typed-racket/typecheck/integer-refinements.rkt b/typed-racket-lib/typed-racket/typecheck/integer-refinements.rkt
index 2a6f18883..6446860f3 100644
--- a/typed-racket-lib/typed-racket/typecheck/integer-refinements.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/integer-refinements.rkt
@@ -71,143 +71,127 @@
            #:attr obj (if (Object? o) o -empty-obj)))
 
 ;; < <= >= =
-(define (numeric-comparison-function prop-constructor)
-  (λ (args-stx result)
-    (syntax-parse args-stx
-      [((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int)))
-       (define p (prop-constructor (attribute e1.obj) (attribute e2.obj)))
-       (add-p/not-p result p)]
-      [((~var e1 (w/type -Int)) (~var e2 (w/type -Int)) (~var e3 (w/type -Int)))
-       #:when (or (and (Object? (attribute e1.obj)) (Object? (attribute e2.obj)))
-                  (and (Object? (attribute e2.obj)) (Object? (attribute e3.obj))))
-       (define p (-and (prop-constructor (attribute e1.obj) (attribute e2.obj))
-                       (prop-constructor (attribute e2.obj) (attribute e3.obj))))
-       (add-p/not-p result p)]
-      [_  result])))
+(define ((numeric-comparison-function prop-constructor) args-stx result)
+  (syntax-parse args-stx
+    [((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int)))
+     (define p (prop-constructor (attribute e1.obj) (attribute e2.obj)))
+     (add-p/not-p result p)]
+    [((~var e1 (w/type -Int)) (~var e2 (w/type -Int)) (~var e3 (w/type -Int)))
+     #:when (or (and (Object? (attribute e1.obj)) (Object? (attribute e2.obj)))
+                (and (Object? (attribute e2.obj)) (Object? (attribute e3.obj))))
+     (define p
+       (-and (prop-constructor (attribute e1.obj) (attribute e2.obj))
+             (prop-constructor (attribute e2.obj) (attribute e3.obj))))
+     (add-p/not-p result p)]
+    [_ result]))
 
 ;; +/-
-(define (plus/minus plus?)
-  (λ (args-stx result)
-    (match result
-      [(tc-result1: ret-t ps orig-obj)
-       (syntax-parse args-stx
-         ;; +/- (2 args)
-         [((~var e1 (w/obj+type -Int))
-           (~var e2 (w/obj+type -Int)))
-          (define (sign o) (if plus? o (scale-obj -1 o)))
-          (define l (-lexp (attribute e1.obj) (sign (attribute e2.obj))))
-          (ret (-refine/fresh x ret-t (-eq (-lexp x) l))
-               ps
-               l)]
-         ;; +/- (3 args)
-         [((~var e1 (w/obj+type -Int))
-           (~var e2 (w/obj+type -Int))
-           (~var e3 (w/obj+type -Int)))
-          (define (sign o) (if plus? o (scale-obj -1 o)))
-          (define l (-lexp (attribute e1.obj) (sign (attribute e2.obj)) (sign (attribute e3.obj))))
-          (ret (-refine/fresh x ret-t (-eq (-lexp x) l))
-               ps
-               l)]
-         [_ result])]
-      [_ result])))
+(define ((plus/minus plus?) args-stx result)
+  (match result
+    [(tc-result1: ret-t ps orig-obj)
+     (syntax-parse args-stx
+       ;; +/- (2 args)
+       [((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int)))
+        (define (sign o)
+          (if plus?
+              o
+              (scale-obj -1 o)))
+        (define l (-lexp (attribute e1.obj) (sign (attribute e2.obj))))
+        (ret (-refine/fresh x ret-t (-eq (-lexp x) l)) ps l)]
+       ;; +/- (3 args)
+       [((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int)) (~var e3 (w/obj+type -Int)))
+        (define (sign o)
+          (if plus?
+              o
+              (scale-obj -1 o)))
+        (define l (-lexp (attribute e1.obj) (sign (attribute e2.obj)) (sign (attribute e3.obj))))
+        (ret (-refine/fresh x ret-t (-eq (-lexp x) l)) ps l)]
+       [_ result])]
+    [_ result]))
 
 ;; equal?/eqv?/eq?
 ;; if only one side is a supported type, we can learn integer equality for
 ;; a result of `#t`, whereas if both sides are of the supported type,
 ;; we learn on both `#t` and `#f` answers
-(define (equality-function supported-type)
-  (λ (args-stx result)
-    (syntax-parse args-stx
-      [((~var e1 (w/obj+type supported-type)) (~var e2 (w/obj+type supported-type)))
-       (define p (-eq (attribute e1.obj) (attribute e2.obj)))
-       (add-p/not-p result p)]
-      [((~var e1 (w/obj+type supported-type)) (~var e2 (w/obj+type Univ)))
-       (define p (-eq (attribute e1.obj) (attribute e2.obj)))
-       (add-to-pos-side result p)]
-      [((~var e1 (w/obj+type Univ)) (~var e2 (w/obj+type supported-type)))
-       (define p (-eq (attribute e1.obj) (attribute e2.obj)))
-       (add-to-pos-side result p)]
-      [_  result])))
+(define ((equality-function supported-type) args-stx result)
+  (syntax-parse args-stx
+    [((~var e1 (w/obj+type supported-type)) (~var e2 (w/obj+type supported-type)))
+     (define p (-eq (attribute e1.obj) (attribute e2.obj)))
+     (add-p/not-p result p)]
+    [((~var e1 (w/obj+type supported-type)) (~var e2 (w/obj+type Univ)))
+     (define p (-eq (attribute e1.obj) (attribute e2.obj)))
+     (add-to-pos-side result p)]
+    [((~var e1 (w/obj+type Univ)) (~var e2 (w/obj+type supported-type)))
+     (define p (-eq (attribute e1.obj) (attribute e2.obj)))
+     (add-to-pos-side result p)]
+    [_ result]))
 
 ;;  *
-(define product-function
-  (λ (args-stx result)
-    (match result
-      [(tc-result1: ret-t ps orig-obj)
-       (syntax-parse args-stx
-         [((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int)))
-          (define product-obj (-obj* (attribute e1.obj) (attribute e2.obj)))
-          (cond
-            [(Object? product-obj)
-             (ret (-refine/fresh x ret-t (-eq (-lexp x) product-obj))
-                  ps
-                  product-obj)]
-            [else result])]
-         [_ result])]
-      [_ result])))
+(define (product-function args-stx result)
+  (match result
+    [(tc-result1: ret-t ps orig-obj)
+     (syntax-parse args-stx
+       [((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int)))
+        (define product-obj (-obj* (attribute e1.obj) (attribute e2.obj)))
+        (cond
+          [(Object? product-obj)
+           (ret (-refine/fresh x ret-t (-eq (-lexp x) product-obj)) ps product-obj)]
+          [else result])]
+       [_ result])]
+    [_ result]))
 
 ;; make-vector
-(define make-vector-function
-  (λ (args-stx result)
-    (match result
-      [(tc-result1: ret-t ps orig-obj)
-       (syntax-parse args-stx
-         [((~var size (w/obj+type -Int)) . _)
-          (ret (-refine/fresh v ret-t (-eq (-lexp (-vec-len-of (-id-path v)))
-                                           (attribute size.obj)))
-               ps
-               orig-obj)]
-         [_ result])]
-      [_ result])))
+(define (make-vector-function args-stx result)
+  (match result
+    [(tc-result1: ret-t ps orig-obj)
+     (syntax-parse args-stx
+       [((~var size (w/obj+type -Int)) . _)
+        (ret (-refine/fresh v ret-t (-eq (-lexp (-vec-len-of (-id-path v))) (attribute size.obj)))
+             ps
+             orig-obj)]
+       [_ result])]
+    [_ result]))
 
 ;; modulo
-(define modulo-function
-  (λ (args-stx result)
-    (match result
-      [(tc-result1: ret-t ps orig-obj)
-       (syntax-parse args-stx
-         [((~var e1 (w/type -Int)) (~var e2 (w/obj+type -Nat)))
-          (ret (-refine/fresh x ret-t (-lt (-lexp x) (attribute e2.obj)))
-               ps
-               orig-obj)]
-         [_ result])]
-      [_ result])))
+(define (modulo-function args-stx result)
+  (match result
+    [(tc-result1: ret-t ps orig-obj)
+     (syntax-parse args-stx
+       [((~var e1 (w/type -Int)) (~var e2 (w/obj+type -Nat)))
+        (ret (-refine/fresh x ret-t (-lt (-lexp x) (attribute e2.obj))) ps orig-obj)]
+       [_ result])]
+    [_ result]))
 
 ;; random
-(define random-function
-  (λ (args-stx result)
-    (match result
-      [(tc-result1: ret-t ps orig-obj)
-       (syntax-parse args-stx
-         ;; random (1 arg)
-         [((~var e1 (w/obj+type -Nat)))
-          (ret (-refine/fresh x ret-t (-lt (-lexp x) (attribute e1.obj)))
-               ps
-               orig-obj)]
-         ;; random (2 arg)
-         [((~var e1 (w/type -Int)) (~var e2 (w/type -Int)))
-          #:when (or (Object? (attribute e1.obj))
-                     (Object? (attribute e2.obj)))
-          (ret (-refine/fresh x ret-t (-and (-leq (attribute e1.obj) (-lexp x))
-                                            (-lt (-lexp x) (attribute e2.obj))))
-               ps
-               orig-obj)]
-         [_ result])]
-      [_ result])))
+(define (random-function args-stx result)
+  (match result
+    [(tc-result1: ret-t ps orig-obj)
+     (syntax-parse args-stx
+       ;; random (1 arg)
+       [((~var e1 (w/obj+type -Nat)))
+        (ret (-refine/fresh x ret-t (-lt (-lexp x) (attribute e1.obj))) ps orig-obj)]
+       ;; random (2 arg)
+       [((~var e1 (w/type -Int)) (~var e2 (w/type -Int)))
+        #:when (or (Object? (attribute e1.obj)) (Object? (attribute e2.obj)))
+        (ret (-refine/fresh x
+                            ret-t
+                            (-and (-leq (attribute e1.obj) (-lexp x))
+                                  (-lt (-lexp x) (attribute e2.obj))))
+             ps
+             orig-obj)]
+       [_ result])]
+    [_ result]))
 
 ;; add1 / sub1
-(define (add/sub-1-function add?)
-  (λ (args-stx result)
-    (match result
-      [(tc-result1: ret-t ps orig-obj)
-       (syntax-parse args-stx
-         [((~var e1 (w/obj+type -Int)))
-          (define l ((if add? -lexp-add1 -lexp-sub1) (attribute e1.obj)))
-          (ret (-refine/fresh x ret-t (-eq (-lexp x) l))
-               ps
-               l)]
-         [_ result])]
-      [_ result])))
+(define ((add/sub-1-function add?) args-stx result)
+  (match result
+    [(tc-result1: ret-t ps orig-obj)
+     (syntax-parse args-stx
+       [((~var e1 (w/obj+type -Int)))
+        (define l ((if add? -lexp-add1 -lexp-sub1) (attribute e1.obj)))
+        (ret (-refine/fresh x ret-t (-eq (-lexp x) l)) ps l)]
+       [_ result])]
+    [_ result]))
 
 (define linear-integer-function-table
   (make-immutable-free-id-table
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
index 77e6ea206..f2f1a4631 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
@@ -42,32 +42,42 @@
 
      (when check?
        (define extra-arg-count (- (length t-a) (length dom)))
-       (cond [(and (not rst) (not (eqv? 0 extra-arg-count)))
-              (tc-error/fields "could not apply function"
-                               #:more "wrong number of arguments provided"
-                               "expected" (length dom)
-                               "given" (length t-a)
-                               #:delayed? #t)]
-             [(and rst (negative? extra-arg-count))
-              (tc-error/fields "could not apply function"
-                               #:more "wrong number of arguments provided"
-                               "expected at least" (length dom)
-                               "given" (length t-a)
-                               #:delayed? #t)]
-             [(and (Rest? rst)
-                   (positive? extra-arg-count)
-                   (not (zero? (remainder extra-arg-count (length (Rest-tys rst))))))
-              (cond
-                [(eqv? 2 (length (Rest-tys rst)))
-                 (tc-error/fields "could not apply function"
-                                  #:more "wrong number of rest arguments provided"
-                                  "expected an even number, given" extra-arg-count
-                                  #:delayed? #t)]
-                [else (tc-error/fields "could not apply function"
-                                       #:more "wrong number of rest arguments provided"
-                                       "expected a multiple of " (length (Rest-tys rst))
-                                       "given" extra-arg-count
-                                       #:delayed? #t)])])
+       (cond
+         [(and (not rst) (not (eqv? 0 extra-arg-count)))
+          (tc-error/fields "could not apply function"
+                           #:more "wrong number of arguments provided"
+                           "expected"
+                           (length dom)
+                           "given"
+                           (length t-a)
+                           #:delayed? #t)]
+         [(and rst (negative? extra-arg-count))
+          (tc-error/fields "could not apply function"
+                           #:more "wrong number of arguments provided"
+                           "expected at least"
+                           (length dom)
+                           "given"
+                           (length t-a)
+                           #:delayed? #t)]
+         [(and (Rest? rst)
+               (positive? extra-arg-count)
+               (not (zero? (remainder extra-arg-count (length (Rest-tys rst))))))
+          (cond
+            [(eqv? 2 (length (Rest-tys rst)))
+             (tc-error/fields "could not apply function"
+                              #:more "wrong number of rest arguments provided"
+                              "expected an even number, given"
+                              extra-arg-count
+                              #:delayed? #t)]
+            [else
+             (tc-error/fields "could not apply function"
+                              #:more "wrong number of rest arguments provided"
+                              "expected a multiple of "
+                              (length (Rest-tys rst))
+                              "given"
+                              extra-arg-count
+                              #:delayed? #t)])]
+         [else (void)])
        (match rst
          [(Rest: rst-ts)
           (for ([a (in-syntax args-stx)]
@@ -307,78 +317,77 @@
               . ->* . tc-results/c)])
 (define (poly-fail f-stx args-stx t argtypes #:name [name #f] #:expected [expected #f])
   (match t
-    [(or (Poly-names:
-          msg-vars
-          (Fun: (list (Arrow: msg-doms
-                              msg-rests
-                              (list (Keyword: _ _ #f) ...)
-                              msg-rngs)
-                      ...)))
+    [(or (Poly-names: msg-vars
+                      (Fun: (list (Arrow: msg-doms msg-rests (list (Keyword: _ _ #f) ...) msg-rngs)
+                                  ...)))
          (PolyDots-names:
           msg-vars
-          (Fun: (list (Arrow: msg-doms
-                              msg-rests
-                              (list (Keyword: _ _ #f) ...)
-                              msg-rngs)
-                      ...)))
-         (PolyRow-names:
-          msg-vars (Fun: (list (Arrow: msg-doms
-                              msg-rests
-                              (list (Keyword: _ _ #f) ...)
-                              msg-rngs)
-                      ...))
-          _))
-     (let ([fcn-string (name->function-str name)])
-       (if (and (andmap null? msg-doms)
-                (null? argtypes))
-           (tc-error/expr (string-append
-                           "Could not infer types for applying polymorphic "
+          (Fun: (list (Arrow: msg-doms msg-rests (list (Keyword: _ _ #f) ...) msg-rngs) ...)))
+         (PolyRow-names: msg-vars
+                         (Fun: (list (Arrow: msg-doms msg-rests (list (Keyword: _ _ #f) ...) msg-rngs)
+                                     ...))
+                         _))
+     (define fcn-string (name->function-str name))
+     (if (and (andmap null? msg-doms) (null? argtypes))
+         (tc-error/expr
+          (string-append "Could not infer types for applying polymorphic " fcn-string "\n"))
+         (domain-mismatches
+          f-stx
+          args-stx
+          t
+          msg-doms
+          msg-rests
+          msg-rngs
+          argtypes
+          #f
+          #f
+          #:expected expected
+          #:msg-thunk
+          (lambda (dom)
+            (string-append "Polymorphic "
                            fcn-string
-                           "\n"))
-           (domain-mismatches f-stx args-stx t msg-doms msg-rests
-                              msg-rngs argtypes #f #f #:expected expected
-                              #:msg-thunk (lambda (dom)
-                                            (string-append
-                                             "Polymorphic " fcn-string " could not be applied to arguments:\n"
-                                             dom
-                                             (if (not (subset? (apply set-union (seteq) (map fv/list msg-doms))
-                                                               (list->seteq msg-vars)))
-                                                 (string-append "Type Variables: " (stringify msg-vars) "\n")
-                                                 ""))))))]
-    [(Poly-names:
-      msg-vars
-      (DepFun: raw-domain _ raw-rng))
-     (with-printable-names (length raw-domain) names
-       (define domain (for/list ([d (in-list raw-domain)])
-                        (instantiate-obj d names)))
-       (define rng (instantiate-obj raw-rng names))
-       (let ([fcn-string (name->function-str name)])
-         (if (and (null? domain)
-                  (null? argtypes))
-             (tc-error/expr (string-append
-                             "Could not infer types for applying polymorphic "
-                             fcn-string
-                             "\n"))
-             (domain-mismatches f-stx args-stx t (list domain) (list #f)
-                                (list rng) argtypes #f #f #:expected expected
-                                #:msg-thunk (lambda (dom)
-                                              (string-append
-                                               "Polymorphic " fcn-string " could not be applied to arguments:\n"
-                                               dom
-                                               (if (not (subset? (fv/list domain) (list->seteq msg-vars)))
-                                                   (string-append "Type Variables: " (stringify msg-vars) "\n")
-                                                   "")))
-                                #:arg-names names))))]
-    [(or (Poly-names:
-          msg-vars
-          (Fun: (list (Arrow: msg-doms msg-rests kws msg-rngs) ...)))
-         (PolyDots-names:
-          msg-vars
-          (Fun: (list (Arrow: msg-doms msg-rests kws msg-rngs) ...)))
-         (PolyRow-names:
-          msg-vars
-          (Fun: (list (Arrow: msg-doms msg-rests kws msg-rngs) ...))
-          _))
+                           " could not be applied to arguments:\n"
+                           dom
+                           (if (not (subset? (apply set-union (seteq) (map fv/list msg-doms))
+                                             (list->seteq msg-vars)))
+                               (string-append "Type Variables: " (stringify msg-vars) "\n")
+                               "")))))]
+    [(Poly-names: msg-vars (DepFun: raw-domain _ raw-rng))
+     (with-printable-names
+      (length raw-domain)
+      names
+      (define domain
+        (for/list ([d (in-list raw-domain)])
+          (instantiate-obj d names)))
+      (define rng (instantiate-obj raw-rng names))
+      (let ([fcn-string (name->function-str name)])
+        (if (and (null? domain) (null? argtypes))
+            (tc-error/expr
+             (string-append "Could not infer types for applying polymorphic " fcn-string "\n"))
+            (domain-mismatches
+             f-stx
+             args-stx
+             t
+             (list domain)
+             (list #f)
+             (list rng)
+             argtypes
+             #f
+             #f
+             #:expected expected
+             #:msg-thunk
+             (lambda (dom)
+               (string-append "Polymorphic "
+                              fcn-string
+                              " could not be applied to arguments:\n"
+                              dom
+                              (if (not (subset? (fv/list domain) (list->seteq msg-vars)))
+                                  (string-append "Type Variables: " (stringify msg-vars) "\n")
+                                  "")))
+             #:arg-names names))))]
+    [(or (Poly-names: msg-vars (Fun: (list (Arrow: msg-doms msg-rests kws msg-rngs) ...)))
+         (PolyDots-names: msg-vars (Fun: (list (Arrow: msg-doms msg-rests kws msg-rngs) ...)))
+         (PolyRow-names: msg-vars (Fun: (list (Arrow: msg-doms msg-rests kws msg-rngs) ...)) _))
      (define fcn-string
        (if name
            (format "function with keywords ~a" (syntax->datum name))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
index cb4c15bcb..ca224528a 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
@@ -310,15 +310,16 @@
        (match argtys
          [(list) (ret out)]
          [(list t)
-          (if (subtype t in)
-              (ret -Void -true-propset)
-              (tc-error/expr
-               #:return (ret -Void -true-propset)
-               "Wrong argument to parameter - expected ~a and got ~a"
-               in t))]
-         [_ (tc-error/expr
-             "Wrong number of arguments to parameter - expected 0 or 1, got ~a"
-             (length argtys))])]
+          #:when (subtype t in)
+          (ret -Void -true-propset)]
+         [(list t)
+          (tc-error/expr #:return (ret -Void -true-propset)
+                         "Wrong argument to parameter - expected ~a and got ~a"
+                         in
+                         t)]
+         [_
+          (tc-error/expr "Wrong number of arguments to parameter - expected 0 or 1, got ~a"
+                         (length argtys))])]
       [(Distinction: _ _ t)
        (tc/funapp f-stx args-stx t args-res expected)]
       ;; resolve names, polymorphic apps, mu, etc
diff --git a/typed-racket-lib/typed-racket/typed-reader.rkt b/typed-racket-lib/typed-racket/typed-reader.rkt
index 7cb6e9340..a9f157bcc 100644
--- a/typed-racket-lib/typed-racket/typed-reader.rkt
+++ b/typed-racket-lib/typed-racket/typed-reader.rkt
@@ -8,73 +8,82 @@
 (define (skip-whitespace port)
   ;; Skips whitespace characters, sensitive to the current
   ;; readtable's definition of whitespace
-  (let ([ch (peek-char port)])
-    (unless (eof-object? ch)
-      ;; Consult current readtable:
-      (let-values ([(like-ch/sym proc dispatch-proc)
-                    (readtable-mapping (current-readtable) ch)])
-        ;; If like-ch/sym is whitespace, then ch is whitespace
-        (when (and (char? like-ch/sym)
-                   (char-whitespace? like-ch/sym))
-          (read-char port)
-          (skip-whitespace port))))))
+  (define ch (peek-char port))
+  (unless (eof-object? ch)
+    ;; Consult current readtable:
+    (define-values (like-ch/sym proc dispatch-proc) (readtable-mapping (current-readtable) ch))
+    ;; If like-ch/sym is whitespace, then ch is whitespace
+    (when (and (char? like-ch/sym) (char-whitespace? like-ch/sym))
+      (read-char port)
+      (skip-whitespace port))))
 
 (define (skip-comments read-one port src)
   ;; Recursive read, but skip comments and detect EOF
   (let loop ()
-    (let ([v (read-one)])
-      (cond
-        [(special-comment? v) (loop)]
-        [(eof-object? v)
-         (let-values ([(l c p) (port-next-location port)])
-           (raise-read-eof-error "unexpected EOF in type annotation" src l c p 1))]
-        [else v]))))
+    (define v (read-one))
+    (cond
+      [(special-comment? v) (loop)]
+      [(eof-object? v)
+       (define-values (l c p) (port-next-location port))
+       (raise-read-eof-error "unexpected EOF in type annotation" src l c p 1)]
+      [else v])))
 
 (define (parse port read-one src)
   (skip-whitespace port)
-  (let ([name (read-one)])
-    (begin0
-      (begin (skip-whitespace port)
-             (let ([next (read-one)])
-               (case (syntax-e next)
-                 ;; type annotation
-                 [(:) (skip-whitespace port)
-                      (type-label-property name (syntax->datum (read-one)))]
-                 [(::) (skip-whitespace port)
-                       (datum->syntax name `(ann ,name : ,(read-one)))]
-                 [(@) (let ([elems (let loop ([es '()])
-                                     (skip-whitespace port)
-                                     (if (equal? #\} (peek-char port))
-                                         (reverse es)
-                                         (loop (cons (read-one) es))))])
-                        (datum->syntax name `(inst ,name : ,@elems)))]
-                 ;; arbitrary property annotation
-                 [(PROP) (skip-whitespace port)
-                         (let* ([prop-name (syntax-e (read-one))])
-                           (skip-whitespace port)
-                           (syntax-property name prop-name (read-one)))]
-                 ;; otherwise error
-                 [else
-                  (let-values ([(l c p) (port-next-location port)])
-                    (raise-read-error (format "typed expression ~a must be followed by :, ::, or @"
-                                              (syntax->datum name)) src l c p 1))])))
-      (skip-whitespace port)
-      (let ([c (read-char port)])
-        (unless (equal? #\} c)
-          (let-values ([(l c p) (port-next-location port)])
-            (raise-read-error (format "typed expression ~a not properly terminated" (syntax->datum name)) src l c p 1)))))))
+  (define name (read-one))
+  (begin0 (begin
+            (skip-whitespace port)
+            (let ([next (read-one)])
+              (case (syntax-e next)
+                ;; type annotation
+                [(:)
+                 (skip-whitespace port)
+                 (type-label-property name (syntax->datum (read-one)))]
+                [(::)
+                 (skip-whitespace port)
+                 (datum->syntax name `(ann ,name : ,(read-one)))]
+                [(@)
+                 (let ([elems (let loop ([es '()])
+                                (skip-whitespace port)
+                                (if (equal? #\} (peek-char port))
+                                    (reverse es)
+                                    (loop (cons (read-one) es))))])
+                   (datum->syntax name `(inst ,name : ,@elems)))]
+                ;; arbitrary property annotation
+                [(PROP)
+                 (skip-whitespace port)
+                 (let* ([prop-name (syntax-e (read-one))])
+                   (skip-whitespace port)
+                   (syntax-property name prop-name (read-one)))]
+                ;; otherwise error
+                [else
+                 (let-values ([(l c p) (port-next-location port)])
+                   (raise-read-error (format "typed expression ~a must be followed by :, ::, or @"
+                                             (syntax->datum name))
+                                     src
+                                     l
+                                     c
+                                     p
+                                     1))])))
+    (skip-whitespace port)
+    (let ([c (read-char port)])
+      (unless (equal? #\} c)
+        (let-values ([(l c p) (port-next-location port)])
+          (raise-read-error (format "typed expression ~a not properly terminated"
+                                    (syntax->datum name))
+                            src
+                            l
+                            c
+                            p
+                            1))))))
 
 (define parse-id-type
-  (case-lambda
-    [(ch port src line col pos)
-     ;; `read-syntax' mode
-     (datum->syntax
-      #f
-      (parse port
-             (lambda () (read-syntax src port ))
-             src)
-      (let-values ([(l c p) (port-next-location port)])
-        (list src line col pos (and pos (- p pos)))))]))
+  (λ (ch port src line col pos)
+    ;; `read-syntax' mode
+    (datum->syntax #f
+                   (parse port (lambda () (read-syntax src port)) src)
+                   (let-values ([(l c p) (port-next-location port)])
+                     (list src line col pos (and pos (- p pos)))))))
 
 (define (readtable)
   ; don't install the reader macro if a dispatch macro on the open brace has already been installed
diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt
index 775938af3..3c39d0037 100644
--- a/typed-racket-lib/typed-racket/types/subtype.rkt
+++ b/typed-racket-lib/typed-racket/types/subtype.rkt
@@ -754,61 +754,62 @@
   [(case: DepFun (DepFun: raw-dom1 raw-pre1 raw-rng1))
    (match t2
      [(DepFun: raw-dom2 raw-pre2 raw-rng2)
-      (cond
-        [(not (= (length raw-dom1)
-                 (length raw-dom2)))
-         #f]
-        [else
-         (with-fresh-ids (length raw-dom1) ids
-           (define dom1 (for/list ([d (in-list raw-dom1)])
+      #:when (not (= (length raw-dom1) (length raw-dom2)))
+      #f]
+     [(DepFun: raw-dom2 raw-pre2 raw-rng2)
+      (with-fresh-ids (length raw-dom1)
+                      ids
+                      (define dom1
+                        (for/list ([d (in-list raw-dom1)])
                           (instantiate-obj d ids)))
-           (define pre1 (instantiate-obj raw-pre1 ids))
-           (define rng1 (instantiate-obj raw-rng1 ids))
-           (define dom2 (for/list ([d (in-list raw-dom2)])
+                      (define pre1 (instantiate-obj raw-pre1 ids))
+                      (define rng1 (instantiate-obj raw-rng1 ids))
+                      (define dom2
+                        (for/list ([d (in-list raw-dom2)])
                           (instantiate-obj d ids)))
-           (define pre2 (instantiate-obj raw-pre2 ids))
-           (define rng2 (instantiate-obj raw-rng2 ids))
-           (with-naively-extended-lexical-env
-               [#:identifiers ids
-                #:types dom2
-                #:props (list pre2)]
-             (define A* (for/fold ([A (subval* A rng1 rng2)])
-                                  ([d1 (in-list dom1)]
-                                   [d2 (in-list dom2)]
-                                   [id (in-list ids)]
-                                   #:break (not A))
-                          (subtype* A d2 d1 (-id-path id))))
-             (and (implies-in-env? (lexical-env) pre2 pre1)
-                  A*)))])]
+                      (define pre2 (instantiate-obj raw-pre2 ids))
+                      (define rng2 (instantiate-obj raw-rng2 ids))
+                      (with-naively-extended-lexical-env
+                       [#:identifiers ids #:types dom2 #:props (list pre2)]
+                       (define A*
+                         (for/fold ([A (subval* A rng1 rng2)])
+                                   ([d1 (in-list dom1)]
+                                    [d2 (in-list dom2)]
+                                    [id (in-list ids)]
+                                    #:break (not A))
+                           (subtype* A d2 d1 (-id-path id))))
+                       (and (implies-in-env? (lexical-env) pre2 pre1) A*)))]
      [(Fun: arrows2)
-      (define arity (for/fold ([arity (length raw-dom1)])
-                              ([a2 (in-list arrows2)])
-                      (max arity (length (Arrow-dom a2)))))
-      (with-fresh-ids arity ids
-        (define dom1 (for/list ([d (in-list raw-dom1)])
-                       (instantiate-obj d ids)))
-        (define pre1 (instantiate-obj raw-pre1 ids))
-        (for/fold ([A A])
-                  ([a2 (in-list arrows2)]
-                   #:break (not A))
-          (match-define (Arrow: dom2 rst2 kws2 raw-rng2) a2)
-          (define A* (subtype-seq A (subtypes* dom2 dom1) (kw-subtypes* '() kws2)))
-          (cond
-            [(not A*) #f]
-            [else
-             (define arity (max (length dom1) (length dom2)))
-             (define-values (mapping t2s)
-               (for/lists (_1 _2)
-                          ([idx (in-range arity)] [id (in-list ids)])
-                          (define t (dom+rst-ref dom2 rst2 idx Univ))
-                          (values (list* idx id t) t)))
-             (with-naively-extended-lexical-env [#:identifiers ids #:types t2s]
-                                                (define A-res
-                                                  (subval* A*
-                                                           (instantiate-obj+simplify raw-rng1 mapping)
-                                                           (instantiate-obj raw-rng2 ids)))
-                                                (and (implies-in-env? (lexical-env) -tt pre1)
-                                                     A-res))])))]
+      (define arity
+        (for/fold ([arity (length raw-dom1)]) ([a2 (in-list arrows2)])
+          (max arity (length (Arrow-dom a2)))))
+      (with-fresh-ids arity
+                      ids
+                      (define dom1
+                        (for/list ([d (in-list raw-dom1)])
+                          (instantiate-obj d ids)))
+                      (define pre1 (instantiate-obj raw-pre1 ids))
+                      (for/fold ([A A])
+                                ([a2 (in-list arrows2)]
+                                 #:break (not A))
+                        (match-define (Arrow: dom2 rst2 kws2 raw-rng2) a2)
+                        (define A* (subtype-seq A (subtypes* dom2 dom1) (kw-subtypes* '() kws2)))
+                        (cond
+                          [(not A*) #f]
+                          [else
+                           (define arity (max (length dom1) (length dom2)))
+                           (define-values (mapping t2s)
+                             (for/lists (_1 _2)
+                                        ([idx (in-range arity)] [id (in-list ids)])
+                                        (define t (dom+rst-ref dom2 rst2 idx Univ))
+                                        (values (list* idx id t) t)))
+                           (with-naively-extended-lexical-env
+                            [#:identifiers ids #:types t2s]
+                            (define A-res
+                              (subval* A*
+                                       (instantiate-obj+simplify raw-rng1 mapping)
+                                       (instantiate-obj raw-rng2 ids)))
+                            (and (implies-in-env? (lexical-env) -tt pre1) A-res))])))]
      [_ (continue<: A t1 t2 obj)])]
   [(case: Distinction (Distinction: nm1 id1 t1*))
    (match t2
@@ -1097,30 +1098,33 @@
   [(case: PolyDots (PolyDots: (list ns ... n-dotted) b1))
    (match t2
      [(PolyDots: (list ms ... m-dotted) b2)
-      (cond
-        [(< (length ns) (length ms))
-         (define-values (short-ms rest-ms) (split-at ms (length ns)))
-         ;; substitute ms for ns in b1 to make it look like b2
-         (define subst
-           (hash-set (make-simple-substitution ns (map make-F short-ms))
-                     n-dotted (i-subst/dotted (map make-F rest-ms) (make-F m-dotted) m-dotted)))
-         (subtype* A (subst-all subst b1) b2)]
-        [else
-         (define-values (short-ns rest-ns) (split-at ns (length ms)))
-         ;; substitute ns for ms in b2 to make it look like b1
-         (define subst
-           (hash-set (make-simple-substitution ms (map make-F short-ns))
-                     m-dotted (i-subst/dotted (map make-F rest-ns) (make-F n-dotted) n-dotted)))
-         (subtype* A b1 (subst-all subst b2))])]
+      #:when (< (length ns) (length ms))
+      (define-values (short-ms rest-ms) (split-at ms (length ns)))
+      ;; substitute ms for ns in b1 to make it look like b2
+      (define subst
+        (hash-set (make-simple-substitution ns (map make-F short-ms))
+                  n-dotted
+                  (i-subst/dotted (map make-F rest-ms) (make-F m-dotted) m-dotted)))
+      (subtype* A (subst-all subst b1) b2)]
+     [(PolyDots: (list ms ... m-dotted) b2)
+      (define-values (short-ns rest-ns) (split-at ns (length ms)))
+      ;; substitute ns for ms in b2 to make it look like b1
+      (define subst
+        (hash-set (make-simple-substitution ms (map make-F short-ns))
+                  m-dotted
+                  (i-subst/dotted (map make-F rest-ns) (make-F n-dotted) n-dotted)))
+      (subtype* A b1 (subst-all subst b2))]
      [(Poly: ms b2)
       #:when (<= (length ns) (length ms))
       ;; substitute ms for ns in b1 to make it look like b2
       (define subst
         (hash-set (make-simple-substitution ns (map make-F (take ms (length ns))))
-                  n-dotted (i-subst (map make-F (drop ms (length ns))))))
+                  n-dotted
+                  (i-subst (map make-F (drop ms (length ns))))))
       (subtype* A (subst-all subst b1) b2)]
-     [_ #:when (infer ns (list n-dotted) (list b1) (list t2) Univ)
-        A]
+     [_
+      #:when (infer ns (list n-dotted) (list b1) (list t2) Univ)
+      A]
      [_ (continue<: A t1 t2 obj)])]
   [(case: PolyRow (PolyRow: vs1 b1 c1))
    (match t2
@@ -1312,18 +1316,16 @@
       (for*/or ([b (in-list bs)]
                 [pred (in-value (Base-predicate b))])
         (and (pred val1) A))]
-     [(SequenceTop:)
-      (and (exact-nonnegative-integer? val1) A)]
+     [(SequenceTop:) (and (exact-nonnegative-integer? val1) A)]
      [(Sequence: (list seq-t))
-      (cond
-        [(exact-nonnegative-integer? val1)
-         (define type
-           (for*/or ([pred/type (in-list value-numeric-seq-possibilities)]
-                     [pred? (in-value (car pred/type))]
-                     #:when (pred? val1))
-             (cdr pred/type)))
-         (subtype* A type seq-t)]
-        [else #f])]
+      #:when (exact-nonnegative-integer? val1)
+      (define type
+        (for*/or ([pred/type (in-list value-numeric-seq-possibilities)]
+                  [pred? (in-value (car pred/type))]
+                  #:when (pred? val1))
+          (cdr pred/type)))
+      (subtype* A type seq-t)]
+     [(Sequence: (list seq-t)) #f]
      [(or (? Struct? s1) (NameStruct: s1))
       #:when (not (struct? val1))
       #f]
@@ -1331,9 +1333,7 @@
       #:when (and (exact-integer? val1)
                   (let ([obj (-lexp val1)])
                     (and (subtype* A t1 t2*)
-                         (implies-in-env? (lexical-env)
-                                          (-is-type obj t1)
-                                          (instantiate-obj p* obj)))))
+                         (implies-in-env? (lexical-env) (-is-type obj t1) (instantiate-obj p* obj)))))
       A]
      [_ (continue<: A t1 t2 obj)])]
   [(case: Weak-Box (Weak-Box: elem1))
diff --git a/typed-racket-lib/typed-racket/types/utils.rkt b/typed-racket-lib/typed-racket/types/utils.rkt
index 69ea0c83d..a46c32e57 100644
--- a/typed-racket-lib/typed-racket/types/utils.rkt
+++ b/typed-racket-lib/typed-racket/types/utils.rkt
@@ -29,12 +29,16 @@
 (define (dom+rst-ref dom rst idx [default dom+rst-ref-failure])
   (match dom
     [(cons t ts)
-     (cond
-       [(zero? idx) t]
-       [else (dom+rst-ref ts rst (sub1 idx) default)])]
-    [_ (match rst
-         [(Rest: rst-ts) (list-ref rst-ts (remainder idx (length rst-ts)))]
-         [_ (if (procedure? default) (default) default)])]))
+     #:when (zero? idx)
+     t]
+    [(cons t ts) (dom+rst-ref ts rst (sub1 idx) default)]
+    [_
+     (match rst
+       [(Rest: rst-ts) (list-ref rst-ts (remainder idx (length rst-ts)))]
+       [_
+        (if (procedure? default)
+            (default)
+            default)])]))
 
 (define (Rest->Type r)
   (match r
diff --git a/typed-racket-test/optimizer/reset-port.rkt b/typed-racket-test/optimizer/reset-port.rkt
index 913fb5678..a0859be36 100644
--- a/typed-racket-test/optimizer/reset-port.rkt
+++ b/typed-racket-test/optimizer/reset-port.rkt
@@ -5,7 +5,7 @@
 (provide read-syntax)
 
 (define (read-syntax name port)
-  (read-line port)
+  (read-line port 'any)
   (when (port-counts-lines? port)
     (set-port-next-location! port 1 0 1))
   (make-special-comment 'typed-racket/optimizer/reset-port))
diff --git a/typed-racket-test/optimizer/run.rkt b/typed-racket-test/optimizer/run.rkt
index 4795a01b9..d49ed2900 100644
--- a/typed-racket-test/optimizer/run.rkt
+++ b/typed-racket-test/optimizer/run.rkt
@@ -11,7 +11,7 @@
 (define (get-expected-results file)
   (with-input-from-file file #:mode 'text
     (lambda () ; from the test file
-      (read-line) ; skip the #;#;
+      (read-line (current-input-port) 'any) ; skip the #;#;
       (values (for/list ((l (in-lines (open-input-string (read))))) l)
               (read)))))
 
diff --git a/typed-racket-test/optimizer/transform.rkt b/typed-racket-test/optimizer/transform.rkt
index dced57d72..935f675d4 100644
--- a/typed-racket-test/optimizer/transform.rkt
+++ b/typed-racket-test/optimizer/transform.rkt
@@ -21,7 +21,7 @@
   (define source-code
     (call-with-input-file* (build-path dir file)
       (lambda (in)
-        (read-line in) ; drop the #;#;
+        (read-line in 'any) ; drop the #;#;
         (read in) ; drop the old expected tr log
         (read in) ; drop the old expected output
         (port->string in))))
@@ -32,13 +32,12 @@
       (for ((entry new-tr-log))
         (write-stringln entry))
       (write-stringln "END")
-      (if (regexp-match "\n" new-output)
-          (begin
-            (write-stringln "#<<END")
-            (write-stringln new-output)
-            (write-stringln "END"))
-          (begin
-            (write new-output)))
+      (cond
+        [(regexp-match "\n" new-output)
+         (write-stringln "#<<END")
+         (write-stringln new-output)
+         (write-stringln "END")]
+        [else (write new-output)])
           (write-string source-code))))
 
 ;; proc returns the list of tests to be run on each file
diff --git a/typed-racket-test/unit-tests/shallow-rewrite-expansion/main.rkt b/typed-racket-test/unit-tests/shallow-rewrite-expansion/main.rkt
index 45462fc61..0bddef7f2 100644
--- a/typed-racket-test/unit-tests/shallow-rewrite-expansion/main.rkt
+++ b/typed-racket-test/unit-tests/shallow-rewrite-expansion/main.rkt
@@ -205,20 +205,19 @@
 
     (list "case-lambda.rkt"
           (lambda (stx)
-            (and
-              (let* ((f0-stx (stx-find
-                               stx
-                               (syntax-predicate
-                                 ((~literal define-values) ((~datum f0)) ((~literal case-lambda) _)))))
-                     (f0-assert (stx-find-shape-check f0-stx))
-                     (f0-match? (shape-check-matches #:expr 'x #:shape 'symbol?  #:type "Symbol")))
-                (f0-match? f0-assert))
-              (let* ((all-assert* (stx-find-shape-check* stx))
-                     (y-pred (shape-check-matches #:expr 'y #:shape 'none/c/proc #:type "Nothing"))
-                     (z-pred (shape-check-matches #:expr 'z #:shape 'none/c/proc #:type "Nothing")))
-                (and
-                  (one-assert-matches y-pred all-assert*)
-                  (one-assert-matches z-pred all-assert*))))))
+            (cond
+              [(let* ([f0-stx (stx-find stx
+                                        (syntax-predicate ((~literal define-values)
+                                                           ((~datum f0))
+                                                           ((~literal case-lambda) _))))]
+                      [f0-assert (stx-find-shape-check f0-stx)]
+                      [f0-match? (shape-check-matches #:expr 'x #:shape 'symbol? #:type "Symbol")])
+                 (f0-match? f0-assert))
+               (define all-assert* (stx-find-shape-check* stx))
+               (define y-pred (shape-check-matches #:expr 'y #:shape 'none/c/proc #:type "Nothing"))
+               (define z-pred (shape-check-matches #:expr 'z #:shape 'none/c/proc #:type "Nothing"))
+               (and (one-assert-matches y-pred all-assert*) (one-assert-matches z-pred all-assert*))]
+              [else #f])))
 
     (list "cdr.rkt"
           no-shape-check?)