diff --git a/typed-racket-lib/typed-racket/static-contracts/combinators/struct.rkt b/typed-racket-lib/typed-racket/static-contracts/combinators/struct.rkt
index 05da781aa..19dfcef65 100644
--- a/typed-racket-lib/typed-racket/static-contracts/combinators/struct.rkt
+++ b/typed-racket-lib/typed-racket/static-contracts/combinators/struct.rkt
@@ -26,28 +26,23 @@
   #:property prop:combinator-name "struct/sc"
   #:methods gen:sc
     [(define (sc-map v f)
-       (match v
-        [(struct-combinator args name mut?)
-         (struct-combinator (map (λ (a) (f a (if mut? 'invariant 'covariant))) args)
-                            name mut?)]))
+       (match-define (struct-combinator args name mut?) v)
+       (struct-combinator (map (λ (a) (f a (if mut? 'invariant 'covariant))) args) name mut?))
      (define (sc-traverse v f)
-       (match v
-        [(struct-combinator args name mut?)
-         (for-each (λ (a) (f a (if mut? 'invariant 'covariant))) args)
-         (void)]))
+       (match-define (struct-combinator args name mut?) v)
+       (for-each (λ (a) (f a (if mut? 'invariant 'covariant))) args)
+       (void))
      (define (sc->contract v f)
-       (match v
-         [(struct-combinator args name _)
-          #`(struct/c #,name #,@(map f args))]))
+       (match-define (struct-combinator args name _) v)
+       #`(struct/c #,name #,@(map f args)))
      (define (sc->constraints v f)
-       (match v
-        [(struct-combinator args _ mut?)
-         (merge-restricts* (if mut? 'chaperone 'flat)
-                           (map (lambda (a)
-                                  (if (not mut?)
-                                      (add-constraint (f a) 'chaperone)
-                                      (f a)))
-                                args))]))])
+       (match-define (struct-combinator args _ mut?) v)
+       (merge-restricts* (if mut? 'chaperone 'flat)
+                         (map (lambda (a)
+                                (if (not mut?)
+                                    (add-constraint (f a) 'chaperone)
+                                    (f a)))
+                              args)))])
 
 (define (struct/sc name mut? fields)
   (struct-combinator fields name mut?))
@@ -64,18 +59,15 @@
   #:property prop:combinator-name "struct-type/sc"
   #:methods gen:sc
     [(define (sc-map v f)
-       (match v
-         [(struct-type/sc args)
-          (struct-type/sc (map (λ (a) (f a 'covariant)) args))]))
+       (match-define (struct-type/sc args) v)
+       (struct-type/sc (map (λ (a) (f a 'covariant)) args)))
      (define (sc-traverse v f)
-       (match v
-         [(struct-type/sc args)
-          (for-each (λ (a) (f a 'covariant)) args)
-          (void)]))
+       (match-define (struct-type/sc args) v)
+       (for-each (λ (a) (f a 'covariant)) args)
+       (void))
      (define (sc->contract v f)
-       (match v
-         [(struct-type/sc args)
-          #`(struct-type/c #f)]))
+       (match-define (struct-type/sc args) v)
+       #`(struct-type/c #f))
      (define (sc->constraints v f)
        (match v
          [(struct-type/sc args) (simple-contract-restrict 'chaperone)]))])
diff --git a/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt b/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt
index b1d016b23..8b81d8e48 100644
--- a/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt
@@ -213,7 +213,7 @@
                  opt:opt-lambda^)
            ;; it's only an interesting opt-lambda expansion if the number
            ;; of optional arguments is greater than zero
-           #:when (> (cadr (attribute opt.value)) 0)
+           #:when (positive? (cadr (attribute opt.value)))
            #:do [(register/method #'meth-name)]
            #:with props-core
                   (let* ([prop-val (attribute opt.value)]
@@ -290,12 +290,10 @@
       [(tc-result1: type) (resolve type)]
       [_ #f]))
   (match expected-type
-    [(? Class? class-type)
-     (ret (parse-and-check form class-type))]
+    [(? Class? class-type) (ret (parse-and-check form class-type))]
     [(Poly-names: ns body-type)
-     (match (check-class form (ret body-type))
-       [(tc-result1: t f o)
-        (ret (make-Poly ns t) f o)])]
+     (match-define (tc-result1: t f o) (check-class form (ret body-type)))
+     (ret (make-Poly ns t) f o)]
     [_ (ret (parse-and-check form #f))]))
 
 ;; Syntax Option<Type> -> Type
@@ -714,18 +712,12 @@
      (localize local-augment-table 'augment-internals)
      (localize local-inner-table '(pubment-internals augment-internals))
      (localize local-init-table 'only-init-internals)))
-  (define-values (localized-field-get-names
-                  localized-field-set-names
-                  localized-private-field-get-names
-                  localized-private-field-set-names
-                  localized-inherit-field-get-names
-                  localized-inherit-field-set-names)
-    (values (map car localized-field-pairs)
-            (map cadr localized-field-pairs)
-            (map car localized-private-field-pairs)
-            (map cadr localized-private-field-pairs)
-            (map car localized-inherit-field-pairs)
-            (map cadr localized-inherit-field-pairs)))
+  (define localized-field-get-names (map car localized-field-pairs))
+  (define localized-field-set-names (map cadr localized-field-pairs))
+  (define localized-private-field-get-names (map car localized-private-field-pairs))
+  (define localized-private-field-set-names (map cadr localized-private-field-pairs))
+  (define localized-inherit-field-get-names (map car localized-inherit-field-pairs))
+  (define localized-inherit-field-set-names (map cadr localized-inherit-field-pairs))
 
   ;; construct the types for method accessors
   (define (make-method-types method-names type-map
@@ -1317,14 +1309,14 @@
 ;; Check that by-name inits are valid for the superclass
 (define (check-by-name init-stxs super-inits)
   (match-define (super-init-stxs _ by-name) init-stxs)
-  (for ([(name _) (in-dict by-name)])
-    (unless (dict-ref super-inits name #f)
-      (tc-error/fields
-       "invalid `super-new' or `super-instantiate'"
-       #:more "init argument not accepted by superclass"
-       "init name" name
-       #:stx #`#,name
-       #:delayed? #t))))
+  (for ([(name _) (in-dict by-name)]
+        #:unless (dict-ref super-inits name #f))
+    (tc-error/fields "invalid `super-new' or `super-instantiate'"
+                     #:more "init argument not accepted by superclass"
+                     "init name"
+                     name
+                     #:stx #`#,name
+                     #:delayed? #t)))
 
 ;; check-super-new : super-init-stxs Dict Type -> Void
 ;; Check if the super-new call is well-typed
@@ -1332,10 +1324,10 @@
   (match-define (super-init-stxs provided-pos-args provided-inits)
                 super-new)
   (define pos-init-diff (- (length provided-pos-args) (length super-inits)))
-  (cond [(and (> pos-init-diff 0) (not init-rest))
+  (cond [(and (positive? pos-init-diff) (not init-rest))
          ;; errror case that's caught above, do nothing
          (void)]
-        [(> pos-init-diff 0)
+        [(positive? pos-init-diff)
          (define-values (pos-args for-init-rest)
            (split-at provided-pos-args (length super-inits)))
          (for ([pos-arg pos-args]
@@ -1361,12 +1353,9 @@
 ;; the pubment types as default augment types if an augment type
 ;; was not already provided
 (define (setup-pubment-defaults pubment-names annotations augment-annotations)
-  (for ([name pubment-names])
-    (when (and (not (hash-has-key? augment-annotations name))
-               (hash-has-key? annotations name))
-      (hash-set! augment-annotations
-                 name
-                 (dict-ref annotations name)))))
+  (for ([name pubment-names]
+        #:when (and (not (hash-has-key? augment-annotations name)) (hash-has-key? annotations name)))
+    (hash-set! augment-annotations name (dict-ref annotations name))))
 
 ;; infer-self-type : Dict RowVar Class Dict<Symbol, Type> Dict<Symbol, Type>
 ;;                   Set<Symbol> Dict<Symbol, Symbol>
@@ -1430,13 +1419,12 @@
       [(Class: _ inits fields publics augments init-rest)
        (values inits fields publics augments init-rest)]
       [_ (values #f #f #f #f #f)]))
-  (define-values (inits fields publics pubments overrides init-rest-name)
-    (values (hash-ref parse-info 'init-internals)
-            (hash-ref parse-info 'field-internals)
-            (hash-ref parse-info 'public-internals)
-            (hash-ref parse-info 'pubment-internals)
-            (hash-ref parse-info 'override-internals)
-            (hash-ref parse-info 'init-rest-name)))
+  (define inits (hash-ref parse-info 'init-internals))
+  (define fields (hash-ref parse-info 'field-internals))
+  (define publics (hash-ref parse-info 'public-internals))
+  (define pubments (hash-ref parse-info 'pubment-internals))
+  (define overrides (hash-ref parse-info 'override-internals))
+  (define init-rest-name (hash-ref parse-info 'init-rest-name))
   (define init-types (make-inits inits super-inits expected-inits))
   (define field-types (make-type-dict fields super-fields expected-fields Univ))
 
diff --git a/typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt b/typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt
index 947eab7c7..5e18b7e81 100644
--- a/typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt
@@ -175,7 +175,8 @@
   ;; this map is used to determine the actual signatures corresponding to the
   ;; given signature tags of the init-depends
   (define tag-map (make-immutable-free-id-table (map cons import-tags import-sigs)))
-  (define lookup-temp (λ (temp) (free-id-table-ref export-temp-internal-map temp #f)))
+  (define (lookup-temp temp)
+    (free-id-table-ref export-temp-internal-map temp #f))
   
   (values (for/list ([sig-id  (in-list import-sigs)]
                      [sig-internal-ids (in-list import-internal-ids)])
diff --git a/typed-racket-lib/typed-racket/typecheck/error-message.rkt b/typed-racket-lib/typed-racket/typecheck/error-message.rkt
index 6a04a7bce..fd909f39f 100644
--- a/typed-racket-lib/typed-racket/typecheck/error-message.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/error-message.rkt
@@ -77,7 +77,7 @@
   (define class/object (if object? "object" "class"))
   (match-define (Class: row inits fields methods augments init-rest) c1)
   (match-define (Class: row* inits* fields* methods* augments* init-rest*) c2)
-  (when (not object?)
+  (unless object?
     (when (and (F? row) (not (F? row*)))
       (type-mismatch (format "Class with row variable `~a'" row)
                      (format "Class with no row variable")))
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/possible-domains.rkt b/typed-racket-lib/typed-racket/typecheck/possible-domains.rkt
index 6e0c8b46a..9be78c7ae 100644
--- a/typed-racket-lib/typed-racket/typecheck/possible-domains.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/possible-domains.rkt
@@ -55,11 +55,11 @@
 
   ;; currently does not take advantage of multi-valued or arbitrary-valued expected types,
   (define expected-ty
-    (and expected
-         (match expected
-           [(tc-result1: t) t]
-           [(tc-any-results: (or #f (TrueProp:))) #t] ; anything is a subtype of expected
-           [_ #f]))) ; don't know what it is, don't do any pruning
+    (match expected
+      [#f #f]
+      [(tc-result1: t) t]
+      [(tc-any-results: (or #f (TrueProp:))) #t] ; anything is a subtype of expected
+      [_ #f])) ; don't know what it is, don't do any pruning
   (define (returns-subtype-of-expected? fun-ty)
     (or (not expected) ; no expected type, anything is fine
         (eq? expected-ty #t) ; expected is tc-anyresults, anything is fine
diff --git a/typed-racket-lib/typed-racket/typecheck/renamer.rkt b/typed-racket-lib/typed-racket/typecheck/renamer.rkt
index e38625ffe..90837be87 100644
--- a/typed-racket-lib/typed-racket/typecheck/renamer.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/renamer.rkt
@@ -43,9 +43,8 @@
 ;;
 ;; The syntax-transforming check is for unit tests
 (define (un-rename id)
-  (if (syntax-transforming?)
-      (let-values (((binding new-id) (syntax-local-value/immediate id (lambda () (values #f #f)))))
-        (if (typed-renaming? binding)
-            new-id
-            id))
-      id))
+  (cond
+    [(syntax-transforming?)
+     (define-values (binding new-id) (syntax-local-value/immediate id (lambda () (values #f #f))))
+     (if (typed-renaming? binding) new-id id)]
+    [else id]))
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 4dd83fe35..77e6ea206 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
@@ -379,25 +379,34 @@
           msg-vars
           (Fun: (list (Arrow: msg-doms msg-rests kws msg-rngs) ...))
           _))
-     (let ([fcn-string (if name
-                           (format "function with keywords ~a" (syntax->datum name))
-                           "function with keywords")])
-       (if (and (andmap null? msg-doms)
-                (null? argtypes))
-           (tc-error/expr (string-append
-                           "Could not infer types for applying polymorphic "
+     (define fcn-string
+       (if name
+           (format "function with keywords ~a" (syntax->datum name))
+           "function with keywords"))
+     (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")
-                                                 ""))))))]))
+                           " 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")
+                               "")))))]))
 
 ;; name->function-str : (Option Identifier) -> String
 ;; Produce a function name string for error messages
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt b/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt
index 26d84d985..101173790 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt
@@ -50,15 +50,24 @@
 
   ;; Raises an error message for the case that the arguments do not match any of the domains
   (define (failure)
-    (match f-ty
-      [(tc-result1:
-         (and t (AnyPoly-names: _ _
-                                (Fun: (list (Arrow: doms rests (list (Keyword: _ _ #f) ...) rngs) ..1)))))
-       (domain-mismatches f args t doms rests rngs arg-tres full-tail-ty #f
-                          #:msg-thunk (lambda (dom)
-                                        (string-append
-                                         "Bad arguments to function in `apply':\n"
-                                         dom)))]))
+    (match-define (tc-result1: (and t
+                                    (AnyPoly-names:
+                                     _
+                                     _
+                                     (Fun: (list (Arrow: doms rests (list (Keyword: _ _ #f) ...) rngs)
+                                                 ..1)))))
+      f-ty)
+    (domain-mismatches f
+                       args
+                       t
+                       doms
+                       rests
+                       rngs
+                       arg-tres
+                       full-tail-ty
+                       #f
+                       #:msg-thunk
+                       (lambda (dom) (string-append "Bad arguments to function in `apply':\n" dom))))
 
   (match f-ty
     ;; apply of a simple function or polymorphic function
@@ -74,9 +83,8 @@
            ;; Takes a possible substitution and computes
            ;; the substituted range type if it is not #f
            (define (finish substitution)
-             (begin0
-               (and substitution (do-ret (subst-all substitution rng)))
-               (add-typeof-expr f (ret (make-Fun (list arrow))))))
+             (and substitution (do-ret (subst-all substitution rng))))
+           (add-typeof-expr f (ret (make-Fun (list arrow))))
            (finish
             (infer vars dotted-vars
                    (list (-Tuple* arg-tys full-tail-ty))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
index e440fab57..ff780b7ca 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
@@ -42,17 +42,17 @@
     [else
      (define-values (props atoms^) (combine-props ps (env-props env)))
 
-     (define atoms (if atoms^
+     (define atoms (and atoms^
                         ;; fix the order of paths to the same object.
                         ;; move objects with fewer path elements forward.
-                        (sort atoms^ (lambda (x y)
-                                       (match* (x y)
-                                         [((TypeProp: (Path: pes1 (? identifier? var1)) _)
-                                           (TypeProp: (Path: pes2 (? identifier? var2)) _))
-                                          #:when (equal? var1 var2)
-                                          (and (< (length pes1) (length pes2)))]
-                                         [(_ _) #f])))
-                        atoms^))
+                        (sort atoms^
+                              (lambda (x y)
+                                (match* (x y)
+                                  [((TypeProp: (Path: pes1 (? identifier? var1)) _)
+                                    (TypeProp: (Path: pes2 (? identifier? var2)) _))
+                                   #:when (equal? var1 var2)
+                                   (and (< (length pes1) (length pes2)))]
+                                  [(_ _) #f])))))
      (cond
        [props
         (let loop ([todo atoms]
@@ -82,35 +82,36 @@
                           (env-set-obj-type Γ obj new-t*))])))
              (match p
                [(TypeProp: (and obj (Path: pes (? identifier? x))) pt)
-                (let ([t (lookup-id-type/lexical x Γ #:fail (λ (_) Univ))])
-                  (define new-t (update t pt #t pes))
-                  (cond
-                    [(Bottom? new-t) #f]
-                    [(equal? t new-t)
-                     (cond
-                       [(ormap uninterpreted-PE? pes)
-                        (update-obj-pos-type new Γ obj pt)]
-                       [else (loop ps (cons p atoms) negs new Γ)])]
-                    [else
-                     ;; it's a new type! check if there are any logical propositions that can
-                     ;; be extracted from new-t
-                     (define-values (new-t* new-props) (extract-props (-id-path x) new-t))
-                     (cond
-                       ;; if the path contains an uninterpreted path element,
-                       ;; we need to update the object's type in addition to
-                       ;; the identifier's type
-                       [(ormap uninterpreted-PE? pes)
-                        (update-obj-pos-type (append new-props new)
-                                             (env-set-id-type Γ x new-t*)
-                                             obj
-                                             pt)]
-                       [(path-type pes new-t*) => (lambda (pt)
-                                                    (loop ps
-                                                          (cons (-is-type obj pt) atoms)
-                                                          negs
-                                                          (append new-props new)
-                                                          (env-set-id-type Γ x new-t*)))]
-                       [else #f])]))]
+                (define t (lookup-id-type/lexical x Γ #:fail (λ (_) Univ)))
+                (define new-t (update t pt #t pes))
+                (cond
+                  [(Bottom? new-t) #f]
+                  [(equal? t new-t)
+                   (cond
+                     [(ormap uninterpreted-PE? pes) (update-obj-pos-type new Γ obj pt)]
+                     [else (loop ps (cons p atoms) negs new Γ)])]
+                  [else
+                   ;; it's a new type! check if there are any logical propositions that can
+                   ;; be extracted from new-t
+                   (define-values (new-t* new-props) (extract-props (-id-path x) new-t))
+                   (cond
+                     ;; if the path contains an uninterpreted path element,
+                     ;; we need to update the object's type in addition to
+                     ;; the identifier's type
+                     [(ormap uninterpreted-PE? pes)
+                      (update-obj-pos-type (append new-props new)
+                                           (env-set-id-type Γ x new-t*)
+                                           obj
+                                           pt)]
+                     [(path-type pes new-t*)
+                      =>
+                      (lambda (pt)
+                        (loop ps
+                              (cons (-is-type obj pt) atoms)
+                              negs
+                              (append new-props new)
+                              (env-set-id-type Γ x new-t*)))]
+                     [else #f])])]
                [(TypeProp: obj pt)
                 (update-obj-pos-type new Γ obj pt)]
                ;; process negative info _after_ positive info so we don't miss anything!
@@ -145,33 +146,32 @@
                                  (env-set-obj-type Γ obj new-t*))])))
                     (match p
                       [(NotTypeProp: (and obj (Path: pes (? identifier? x))) pt)
-                       (let ([t (lookup-id-type/lexical x Γ #:fail (λ (_) Univ))])
-                         (define new-t (update t pt #f pes))
-                         (cond
-                           [(Bottom? new-t) #f]
-                           [(equal? t new-t)
-                            (cond
-                              [(ormap uninterpreted-PE? pes)
-                               (update-obj-neg-type new Γ obj pt)]
-                              [else (loop negs (cons p atoms) new Γ)])]
-                           [else
-                            ;; it's a new type! check if there are any logical propositions that can
-                            ;; be extracted from new-t
-                            (define-values (new-t* new-props) (extract-props (-id-path x) new-t))
-                            (cond
-                              ;; if the path contains an uninterpreted path element,
-                              ;; we need to update the object's type in addition to
-                              ;; the identifier's type
-                              [(ormap uninterpreted-PE? pes)
-                               (update-obj-neg-type (append new-props new)
-                                                    (env-set-id-type Γ x new-t*)
-                                                    obj
-                                                    pt)]
-                              [else
-                               (loop negs
-                                     (cons p atoms)
-                                     (append new-props new)
-                                     (env-set-id-type Γ x new-t*))])]))]
+                       (define t (lookup-id-type/lexical x Γ #:fail (λ (_) Univ)))
+                       (define new-t (update t pt #f pes))
+                       (cond
+                         [(Bottom? new-t) #f]
+                         [(equal? t new-t)
+                          (cond
+                            [(ormap uninterpreted-PE? pes) (update-obj-neg-type new Γ obj pt)]
+                            [else (loop negs (cons p atoms) new Γ)])]
+                         [else
+                          ;; it's a new type! check if there are any logical propositions that can
+                          ;; be extracted from new-t
+                          (define-values (new-t* new-props) (extract-props (-id-path x) new-t))
+                          (cond
+                            ;; if the path contains an uninterpreted path element,
+                            ;; we need to update the object's type in addition to
+                            ;; the identifier's type
+                            [(ormap uninterpreted-PE? pes)
+                             (update-obj-neg-type (append new-props new)
+                                                  (env-set-id-type Γ x new-t*)
+                                                  obj
+                                                  pt)]
+                            [else
+                             (loop negs
+                                   (cons p atoms)
+                                   (append new-props new)
+                                   (env-set-id-type Γ x new-t*))])])]
                       [(NotTypeProp: obj pt)
                        (update-obj-neg-type new Γ obj pt)])]
                    [_
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
index 336eaeb09..e26f1ccda 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
@@ -94,8 +94,8 @@
     (values (tc-expr/t expr) (current-type-error?))))
 
 (define (tc-expr/check/t e t)
-  (match (tc-expr/check e t)
-    [(tc-result1: t) t]))
+  (match-define (tc-result1: t) (tc-expr/check e t))
+  t)
 
 ;; typecheck an expression by passing tr-expr/check a tc-results
 (define/cond-contract (tc-expr/check/type form expected)
@@ -143,8 +143,8 @@
       (dynamic-wind
         (λ () (save-errors!))
         (λ ()
-          (let ([result (tc-expr/check form expected)])
-            (and (not (current-type-error?)) result)))
+          (define result (tc-expr/check form expected))
+          (and (not (current-type-error?)) result))
         (λ () (restore-errors!))))))
 
 (define (tc-expr/check/t? form expected)
@@ -194,7 +194,7 @@
       [t:assert-typecheck-failure
        (cond
          [(tc-expr/check? #'t.body expected)
-          (tc-error/expr #:stx #'t.body (format "Expected a type check error!"))]
+          (tc-error/expr #:stx #'t.body "Expected a type check error!")]
          [else
           (fix-results expected)])]
       ;; data
@@ -317,9 +317,11 @@
               (attribute opt.value))
             (opt-convert fun-type required-pos optional-pos optional-supplied?)]
            [_ #f]))
-       (if conv-type
-           (begin (tc-expr/check/type #'fun conv-type) (fix-results expected))
-           (tc-expr/check form #f))]
+       (cond
+         [conv-type
+          (tc-expr/check/type #'fun conv-type)
+          (fix-results expected)]
+         [else (tc-expr/check form #f)])]
       [(~and _:kw-lambda^
              (let-values ([(f) fun])
                (let-values _
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
index 7f237be3b..cb4c15bcb 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
@@ -134,24 +134,30 @@
        (cond
          ;; find the first function where the argument types match
          [(ormap (match-lambda
-                   [(and a (Arrow: dom rst _ _))
-                    (and (subtypes/varargs argtys dom rst) a)])
+                   [(and a (Arrow: dom rst _ _)) (and (subtypes/varargs argtys dom rst) a)])
                  arrows)
-          => (λ (a)
-               ;; then typecheck here -- we call the separate function so that we get
-               ;; the appropriate props/objects
-               (tc/funapp1 f-stx args-stx a args-res expected #:check #f))]
+          =>
+          (λ (a)
+            ;; then typecheck here -- we call the separate function so that we get
+            ;; the appropriate props/objects
+            (tc/funapp1 f-stx args-stx a args-res expected #:check #f))]
          [else
           ;; if nothing matched, error
-          (match arrows
-            [(list (Arrow: doms rsts _ rngs) ...)
-             (domain-mismatches
-              f-stx args-stx f-type doms rsts rngs args-res #f #f
-              #:expected expected
-              #:msg-thunk (lambda (dom)
-                            (string-append
-                             "No function domains matched in function application:\n"
-                             dom)))])])]
+          (match-define (list (Arrow: doms rsts _ rngs) ...) arrows)
+          (domain-mismatches f-stx
+                             args-stx
+                             f-type
+                             doms
+                             rsts
+                             rngs
+                             args-res
+                             #f
+                             #f
+                             #:expected expected
+                             #:msg-thunk
+                             (lambda (dom)
+                               (string-append "No function domains matched in function application:\n"
+                                              dom)))])]
       ;; any kind of dotted polymorphic function without mandatory keyword args
       [(PolyDots: (list fixed-vars ... dotted-var)
                   (Fun: arrows))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-if.rkt b/typed-racket-lib/typed-racket/typecheck/tc-if.rkt
index 4cea80d0c..7e1e97a8a 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-if.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-if.rkt
@@ -15,27 +15,25 @@
 (export tc-if^)
 
 (define (tc/if-twoarm tst thn els [expected #f])
-  (match (single-value tst)
-    [(tc-result1: _ (PropSet: p+ p-) _)
-     (define thn-res
-       (with-lexical-env+props (list p+)
-         #:expected expected
-         #:unreachable (warn-unreachable thn)
-         (test-position-add-true tst)
-         (tc-expr/check thn expected)))
-     (define els-res
-       (with-lexical-env+props (list p-)
-         #:expected expected
-         #:unreachable (warn-unreachable els)
-         (test-position-add-false tst)
-         (tc-expr/check els expected)))
+  (match-define (tc-result1: _ (PropSet: p+ p-) _) (single-value tst))
+  (define thn-res
+    (with-lexical-env+props (list p+)
+                            #:expected expected
+                            #:unreachable (warn-unreachable thn)
+                            (test-position-add-true tst)
+                            (tc-expr/check thn expected)))
+  (define els-res
+    (with-lexical-env+props (list p-)
+                            #:expected expected
+                            #:unreachable (warn-unreachable els)
+                            (test-position-add-false tst)
+                            (tc-expr/check els expected)))
 
-     (match expected
-       ;; if there was not any expected results, then merge the 'then'
-       ;; and 'else' results so we propogate the correct info upwards
-       [(or #f (tc-any-results: #f))
-        (merge-tc-results (list thn-res els-res))]
-       ;; otherwise, the subcomponents have already been checked and
-       ;; we just return the expected result 'fixed' to replace any
-       ;; missing fields (i.e. #f props or objects)
-       [_ (fix-results expected)])]))
+  (match expected
+    ;; if there was not any expected results, then merge the 'then'
+    ;; and 'else' results so we propogate the correct info upwards
+    [(or #f (tc-any-results: #f)) (merge-tc-results (list thn-res els-res))]
+    ;; otherwise, the subcomponents have already been checked and
+    ;; we just return the expected result 'fixed' to replace any
+    ;; missing fields (i.e. #f props or objects)
+    [_ (fix-results expected)]))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
index 36f666762..6af500811 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
@@ -336,7 +336,7 @@
       [_ #f]))
 
   (cond
-    [(and (> (free-id-table-count aux-table) 0) (not rest-id))
+    [(and (positive? (free-id-table-count aux-table)) (not rest-id))
      (tc/opt-lambda-clause arg-list body aux-table)]
     [else
      (define arg-types (get-types arg-list #:default (lambda () #f)))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
index 89ef796d4..6720c4d93 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
@@ -256,12 +256,12 @@
            non-bindings
            expected
            #:before-check-body
-           (λ () (begin (for ([expr (in-list remaining-exprs)]
-                              [results (in-list given-rhs-types)])
-                          (match results
-                            [(list (tc-result: ts fs os) ...)
-                             (tc-expr/check expr (ret ts fs os))]))
-                        (check-thunk))))])))))
+           (λ ()
+             (for ([expr (in-list remaining-exprs)]
+                   [results (in-list given-rhs-types)])
+               (match results
+                 [(list (tc-result: ts fs os) ...) (tc-expr/check expr (ret ts fs os))]))
+             (check-thunk)))])))))
 
 ;; An lr-clause is a
 ;;   (lr-clause (Listof Identifier) Syntax)
@@ -284,8 +284,8 @@
       (if (null? names)
           (values (cons clause non-binding) other-clauses)
           (values non-binding (cons clause other-clauses)))))
-  (define-values (non-binding other-clauses)
-    (values (reverse *non-binding) (reverse *other-clauses)))
+  (define non-binding (reverse *non-binding))
+  (define other-clauses (reverse *other-clauses))
 
   ;; Set up vertices for Tarjan's algorithm, where each letrec-values
   ;; clause is a vertex but mapped in the table for each of the clause names
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt b/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt
index 182f32e8f..728a718dc 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt
@@ -190,9 +190,9 @@
            [vt (apply Un vts)])
       (tycon (check-below kt expected-kt) (check-below vt expected-vt)))]
    [(check-element h tycon)
-    (let ([kt (generalize (apply Un (map check-element (hash-keys h))))]
-          [vt (generalize (apply Un (map check-element (hash-values h))))])
-      (tycon kt vt))]))
+    (define kt (generalize (apply Un (map check-element (hash-keys h)))))
+    (define vt (generalize (apply Un (map check-element (hash-values h)))))
+    (tycon kt vt)]))
 
 ;; Typecheck a prefab struct literal (or result of syntax-e)
 ;; `check-field` allows prefabs in syntax to be checked by passing
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index 66496b11b..7f391d921 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
@@ -193,10 +193,10 @@
       (if (null? l)
           (values (reverse getters) (reverse setters))
           (loop (cddr l) (cons (car l) getters) (cons (cadr l) setters)))))
-  (match (build-struct-names nm flds #f #f nm #:constructor-name maker*)
-    [(list sty maker pred getters/setters ...)
-     (let-values ([(getters setters) (split getters/setters)])
-       (struct-names nm type-name sty maker extra-maker pred getters setters))]))
+  (match-define (list sty maker pred getters/setters ...)
+    (build-struct-names nm flds #f #f nm #:constructor-name maker*))
+  (let-values ([(getters setters) (split getters/setters)])
+    (struct-names nm type-name sty maker extra-maker pred getters setters)))
 
 ;; gets the fields of the parent type, if they exist
 ;; Option[Struct-Ty] -> Listof[Type]
@@ -413,9 +413,9 @@
     (for/list ([opname (in-list operators)]
                [self-fld (in-list self-fields)]
                [idx-parent-cnt (in-naturals parent-count)])
-      (let-values ([(fn-args poly-ty) (mk-vals opname self-fld idx-parent-cnt st-type-alias)])
-        (apply add-struct-operator-fn! opname fn-args)
-        (make-def-binding opname poly-ty))))
+      (define-values (fn-args poly-ty) (mk-vals opname self-fld idx-parent-cnt st-type-alias))
+      (apply add-struct-operator-fn! opname fn-args)
+      (make-def-binding opname poly-ty)))
 
   (define bindings
     (list* (make-def-binding struct-type (make-StructType sty))
@@ -458,14 +458,12 @@
                            def-bindings))))
 
 (define (register-parsed-struct-sty! ps)
-  (match ps
-    ((parsed-struct sty names desc si)
-     (register-sty! sty names desc))))
+  (match-define (parsed-struct sty names desc si) ps)
+  (register-sty! sty names desc))
 
 (define (register-parsed-struct-bindings! ps)
-  (match ps
-    ((parsed-struct sty names desc si)
-     (register-struct-bindings! sty names desc si))))
+  (match-define (parsed-struct sty names desc si) ps)
+  (register-struct-bindings! sty names desc si))
 
 ;; extract the type annotation of prop:procedure value
 (define/cond-contract (extract-proc-ty proc-ty-stx desc fld-names st-name)
@@ -513,28 +511,29 @@
        (match ty
          [(Fun: (list arrs ...))
           (make-Fun
-           (map (lambda (arr)
-                  (Arrow-update
-                   arr
-                   dom
-                   (lambda (doms)
-                     (match (car doms)
-                       [(Name/simple: n)
-                        #:when (free-identifier=? n st-name)
-                        (void)]
-                       [(App: (Name/simple: rator) vars)
-                        #:when (free-identifier=? rator st-name)
-                        (void)]
-                       [(Univ:)
-                        (void)]
-                       [(or (Name/simple: (app syntax-e n)) n)
-                        (tc-error/fields "type mismatch in the first parameter of the function for prop:procedure"
-                                         "expected" (syntax-e st-name)
-                                         "got" n
-                                         #:stx (st-proc-ty-property #'ty-stx))])
-
-                     (cdr doms))))
-                arrs))]
+           (for/list ([arr (in-list arrs)])
+             (Arrow-update
+              arr
+              dom
+              (lambda (doms)
+                (match (car doms)
+                  [(Name/simple: n)
+                   #:when (free-identifier=? n st-name)
+                   (void)]
+                  [(App: (Name/simple: rator) vars)
+                   #:when (free-identifier=? rator st-name)
+                   (void)]
+                  [(Univ:) (void)]
+                  [(or (Name/simple: (app syntax-e n)) n)
+                   (tc-error/fields
+                    "type mismatch in the first parameter of the function for prop:procedure"
+                    "expected"
+                    (syntax-e st-name)
+                    "got"
+                    n
+                    #:stx (st-proc-ty-property #'ty-stx))])
+           
+                (cdr doms)))))]
          [_
           (tc-error/fields "type mismatch"
                            "expected"
diff --git a/typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt b/typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt
index 29aacdf6c..23c258b33 100644
--- a/typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt
@@ -61,14 +61,14 @@
 
   (define-for-syntax (maybe-optimize body)
     ;; do we optimize?
-    (if (and (optimize?)
-             (memq (current-type-enforcement-mode) (list deep shallow))
-             (not (getenv "PLT_TR_NO_OPTIMIZE")))
-        (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")))
+       (do-time "Starting optimizer")
+       (begin0 (stx-map optimize-top body)
+         (do-time "Optimized"))]
+      [else body]))
 
   (define-for-syntax (maybe-shallow-rewrite body-stx ctc-cache)
     (case (current-type-enforcement-mode)
diff --git a/typed-racket-lib/typed/private/rewriter.rkt b/typed-racket-lib/typed/private/rewriter.rkt
index 7bd43150d..8c40bfe27 100644
--- a/typed-racket-lib/typed/private/rewriter.rkt
+++ b/typed-racket-lib/typed/private/rewriter.rkt
@@ -7,7 +7,7 @@
 
 (define-for-syntax (rewrite stx tbl from)
   (define (rw stx)
-     (syntax-parse (syntax-disarm stx code-insp) #:literal-sets (kernel-literals)
+     (syntax-parse stx #:literal-sets (kernel-literals)
        [i:identifier
         (dict-ref tbl #'i #'i)]
        ;; no expressions here