From 0f8219bed3bc6301f7a02fa009427a7655be2833 Mon Sep 17 00:00:00 2001
From: "resyntax-ci[bot]" <181813515+resyntax-ci[bot]@users.noreply.github.com>
Date: Fri, 18 Oct 2024 00:37:36 +0000
Subject: [PATCH] Automated Resyntax fixes

This is an automated change generated by Resyntax.

#### Pass 1

Applied 1 fix to [`typed-racket-lib/typed-racket/typecheck/possible-domains.rkt`](../blob/HEAD/typed-racket-lib/typed-racket/typecheck/possible-domains.rkt)

  * Line 58, `and-match-to-match`: This `and` expression can be turned into a clause of the inner `match` expression, reducing nesting.

Applied 2 fixes to [`typed-racket-lib/typed-racket/typecheck/integer-refinements.rkt`](../blob/HEAD/typed-racket-lib/typed-racket/typecheck/integer-refinements.rkt)

  * Line 3, `tidy-require`: Keep imports in `require` sorted and grouped by phase, with collections before files.
  * Line 74, `define-lambda-to-define`: The `define` form supports a shorthand for defining functions.

Applied 3 fixes to [`typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt`](../blob/HEAD/typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt)

  * Line 11, `tidy-require`: Keep imports in `require` sorted and grouped by phase, with collections before files.
  * Line 34, `tidy-require`: Keep imports in `require` sorted and grouped by phase, with collections before files.
  * Line 64, `if-begin-to-cond`: Using `cond` instead of `if` here makes `begin` unnecessary

Applied 1 fix to [`typed-racket-lib/typed-racket/private/type-annotation.rkt`](../blob/HEAD/typed-racket-lib/typed-racket/private/type-annotation.rkt)

  * Line 92, `let-to-define`: Internal definitions are recommended instead of `let` expressions, to reduce nesting.

Applied 2 fixes to [`typed-racket-lib/typed-racket/private/user-defined-type-constr.rkt`](../blob/HEAD/typed-racket-lib/typed-racket/private/user-defined-type-constr.rkt)

  * Line 2, `tidy-require`: Keep imports in `require` sorted and grouped by phase, with collections before files.
  * Line 32, `single-clause-match-to-match-define`: This `match` expression can be simplified using `match-define`.

Applied 1 fix to [`typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt`](../blob/HEAD/typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt)

  * Line 178, `define-lambda-to-define`: The `define` form supports a shorthand for defining functions.

Applied 15 fixes to [`typed-racket-lib/typed-racket/private/type-contract.rkt`](../blob/HEAD/typed-racket-lib/typed-racket/private/type-contract.rkt)

  * Line 242, `if-begin-to-cond`: Using `cond` instead of `if` here makes `begin` unnecessary
  * Line 389, `unused-definition`: This definition is not used.
  * Line 557, `let-to-define`: Internal definitions are recommended instead of `let` expressions, to reduce nesting.
  * Line 838, `always-throwing-cond-to-when`: Using `when` and `unless` is simpler than a conditional with an always-throwing branch.
  * Line 1139, `unused-definition`: This definition is not used.
  * Line 1167, `single-clause-match-to-match-define`: This `match` expression can be simplified using `match-define`.
  * Line 1270, `zero-comparison-lambda-to-positive?`: This lambda function is equivalent to the built-in `positive?` predicate.
  * Line 1290, `map-to-for`: This `map` operation can be replaced with a `for/list` loop.
  * Line 1295, `single-clause-match-to-match-define`: This `match` expression can be simplified using `match-define`.
  * Line 1324, `unused-definition`: This definition is not used.
  * Line 1549, `define-lambda-to-define`: The `define` form supports a shorthand for defining functions.
  * Line 1550, `define-lambda-to-define`: The `define` form supports a shorthand for defining functions.
  * Line 1551, `define-lambda-to-define`: The `define` form supports a shorthand for defining functions.
  * Line 1552, `define-lambda-to-define`: The `define` form supports a shorthand for defining functions.
  * Line 1553, `define-lambda-to-define`: The `define` form supports a shorthand for defining functions.

Applied 8 fixes to [`typed-racket-lib/typed-racket/private/shallow-rewrite.rkt`](../blob/HEAD/typed-racket-lib/typed-racket/private/shallow-rewrite.rkt)

  * Line 225, `if-let-to-cond`: `cond` with internal definitions is preferred over `if` with `let`, to reduce nesting
  * Line 275, `define-let-to-double-define`: This `let` expression can be pulled up into a `define` expression.
  * Line 287, `if-let-to-cond`: `cond` with internal definitions is preferred over `if` with `let`, to reduce nesting
  * Line 418, `let-to-define`: Internal definitions are recommended instead of `let` expressions, to reduce nesting.
  * Line 428, `let-to-define`: Internal definitions are recommended instead of `let` expressions, to reduce nesting.
  * Line 452, `if-let-to-cond`: `cond` with internal definitions is preferred over `if` with `let`, to reduce nesting
  * Line 632, `let-to-define`: Internal definitions are recommended instead of `let` expressions, to reduce nesting.
  * Line 717, `unused-definition`: This definition is not used.

Applied 2 fixes to [`typed-racket-lib/typed-racket/private/with-types.rkt`](../blob/HEAD/typed-racket-lib/typed-racket/private/with-types.rkt)

  * Line 3, `tidy-require`: Keep imports in `require` sorted and grouped by phase, with collections before files.
  * Line 53, `inverted-unless`: This negated `unless` expression can be replaced by a `when` expression.

Applied 2 fixes to [`typed-racket-lib/typed-racket/typecheck/check-below.rkt`](../blob/HEAD/typed-racket-lib/typed-racket/typecheck/check-below.rkt)

  * Line 3, `tidy-require`: Keep imports in `require` sorted and grouped by phase, with collections before files.
  * Line 86, `unused-definition`: This definition is not used.

Applied 3 fixes to [`typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt`](../blob/HEAD/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt)

  * Line 96, `single-clause-match-to-match-define`: This `match` expression can be simplified using `match-define`.
  * Line 146, `let-to-define`: Internal definitions are recommended instead of `let` expressions, to reduce nesting.
  * Line 197, `format-identity`: This use of `format` does nothing.

Applied 1 fix to [`typed-racket-lib/typed-racket/private/syntax-properties.rkt`](../blob/HEAD/typed-racket-lib/typed-racket/private/syntax-properties.rkt)

  * Line 2, `tidy-require`: Keep imports in `require` sorted and grouped by phase, with collections before files.

Applied 1 fix to [`typed-racket-lib/typed-racket/private/parse-classes.rkt`](../blob/HEAD/typed-racket-lib/typed-racket/private/parse-classes.rkt)

  * Line 3, `tidy-require`: Keep imports in `require` sorted and grouped by phase, with collections before files.

Applied 3 fixes to [`typed-racket-lib/typed-racket/private/parse-type.rkt`](../blob/HEAD/typed-racket-lib/typed-racket/private/parse-type.rkt)

  * Line 186, `let-to-define`: Internal definitions are recommended instead of `let` expressions, to reduce nesting.
  * Line 1509, `for/fold-with-conditional-body-to-unless-keyword`: This `for/fold` loop can be simplified by using the `#:unless` keyword.
  * Line 1658, `inline-unnecessary-define`: This variable is returned immediately and can be inlined.

## Summary

Fixed 45 issues in 14 files.

  * Fixed 8 occurrences of `tidy-require`
  * Fixed 7 occurrences of `let-to-define`
  * Fixed 7 occurrences of `define-lambda-to-define`
  * Fixed 5 occurrences of `unused-definition`
  * Fixed 4 occurrences of `single-clause-match-to-match-define`
  * Fixed 3 occurrences of `if-let-to-cond`
  * Fixed 2 occurrences of `if-begin-to-cond`
  * Fixed 1 occurrence of `and-match-to-match`
  * Fixed 1 occurrence of `format-identity`
  * Fixed 1 occurrence of `for/fold-with-conditional-body-to-unless-keyword`
  * Fixed 1 occurrence of `inline-unnecessary-define`
  * Fixed 1 occurrence of `always-throwing-cond-to-when`
  * Fixed 1 occurrence of `zero-comparison-lambda-to-positive?`
  * Fixed 1 occurrence of `map-to-for`
  * Fixed 1 occurrence of `define-let-to-double-define`
  * Fixed 1 occurrence of `inverted-unless`
---
 .../typed-racket/private/parse-classes.rkt    |   6 +-
 .../typed-racket/private/parse-type.rkt       |  23 +-
 .../typed-racket/private/shallow-rewrite.rkt  | 206 ++++++++++--------
 .../private/syntax-properties.rkt             |   7 +-
 .../typed-racket/private/type-annotation.rkt  |  83 +++----
 .../typed-racket/private/type-contract.rkt    | 136 +++++-------
 .../private/user-defined-type-constr.rkt      |  13 +-
 .../typed-racket/private/with-types.rkt       | 108 ++++++---
 .../typed-racket/typecheck/check-below.rkt    | 117 ++++------
 .../typecheck/check-unit-unit.rkt             |   3 +-
 .../typecheck/integer-refinements.rkt         |  38 ++--
 .../typecheck/possible-domains.rkt            |  10 +-
 .../typed-racket/typecheck/tc-expr-unit.rkt   |  10 +-
 .../typecheck/toplevel-trampoline.rkt         |  44 ++--
 14 files changed, 411 insertions(+), 393 deletions(-)

diff --git a/typed-racket-lib/typed-racket/private/parse-classes.rkt b/typed-racket-lib/typed-racket/private/parse-classes.rkt
index f4dbe796a..70bb1032d 100644
--- a/typed-racket-lib/typed-racket/private/parse-classes.rkt
+++ b/typed-racket-lib/typed-racket/private/parse-classes.rkt
@@ -1,8 +1,8 @@
 #lang racket/base
 
-(require syntax/parse/pre
-         "../utils/literal-syntax-class.rkt"
-         (for-label "../base-env/base-types-extra.rkt"))
+(require (for-label "../base-env/base-types-extra.rkt")
+         syntax/parse/pre
+         "../utils/literal-syntax-class.rkt")
 (provide star ddd ddd/bound omit-parens)
 
 (define-literal-syntax-class #:for-label ->)
diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt
index 81497c8d1..9a91c0db5 100644
--- a/typed-racket-lib/typed-racket/private/parse-type.rkt
+++ b/typed-racket-lib/typed-racket/private/parse-type.rkt
@@ -183,8 +183,8 @@
 ;; (Syntax -> Type) -> Syntax Any -> Syntax
 ;; See `parse-type/id`. This is a curried generalization.
 (define ((parse/id p) loc datum)
-  (let* ([stx* (datum->syntax loc datum loc loc)])
-    (p stx*)))
+  (define stx* (datum->syntax loc datum loc loc))
+  (p stx*))
 
 (define (parse-literal-alls stx)
   (syntax-parse stx
@@ -1507,10 +1507,9 @@
   ;; Merge all the non-duplicate entries from the parent types
   (define (merge-clause parent-clause clause)
     (for/fold ([clause clause])
-              ([(k v) (in-dict parent-clause)])
-      (if (dict-has-key? clause k)
-          clause
-          (dict-set clause k v))))
+              ([(k v) (in-dict parent-clause)]
+               #:unless (dict-has-key? clause k))
+      (dict-set clause k v)))
 
   (define (match-parent-type parent-type)
     (define resolved (resolve parent-type))
@@ -1655,12 +1654,12 @@
             ;; of init arguments.
             (define parent-inits (get-parent-inits parent/init-type))
 
-            (define class-type
-              (make-Class row-var
-                          (append given-inits parent-inits)
-                          fields methods augments given-init-rest))
-
-            class-type]
+            (make-Class row-var
+                        (append given-inits parent-inits)
+                        fields
+                        methods
+                        augments
+                        given-init-rest)]
            [else
             ;; Conservatively assume that if there *are* #:implements
             ;; clauses, then the current type alias will be recursive
diff --git a/typed-racket-lib/typed-racket/private/shallow-rewrite.rkt b/typed-racket-lib/typed-racket/private/shallow-rewrite.rkt
index 91dad491f..a0d2280c0 100644
--- a/typed-racket-lib/typed-racket/private/shallow-rewrite.rkt
+++ b/typed-racket-lib/typed-racket/private/shallow-rewrite.rkt
@@ -222,36 +222,48 @@
                           [check-formal*
                             (let protect-loop ([args #'formals]
                                                [dom* dom*])
-                              (if (or (identifier? args)
-                                      (null? args)
-                                      (and (syntax? args) (null? (syntax-e args))))
-                                '()
-                                (let*-values ([(fst rst)
-                                               (cond
-                                                 [(pair? args)
-                                                  (values (car args) (cdr args))]
-                                                 [(syntax? args)
-                                                  (let ((e (syntax-e args)))
-                                                    (values (car e) (cdr e)))]
-                                                 [else
-                                                   (raise-syntax-error 'shallow-rewrite-top "#%plain-lambda formals" #'formals args)])]
-                                              [(check*)
-                                               (let ((dom+
-                                                     (for/fold ((acc '()))
-                                                               ((dom (in-list dom*)))
-                                                       (if (pair? dom) (cons (cdr dom) acc) acc))))
-                                                 (protect-loop rst dom+))]
-                                              [(fst-ty)
-                                               (let ((ann-ty (and (type-annotation fst #:infer #f) (get-type fst #:infer #t #:default Univ))))
-                                                 (if (and ann-ty (not (Error? ann-ty)))
-                                                   ann-ty
-                                                   (apply Un (for/list ((dom (in-list dom*)) #:when (pair? dom)) (car dom)))))]
-                                              [(ex* fst+)
-                                               (if skip-dom?
-                                                 (values '() #f)
-                                                 (protect-domain fst-ty fst (build-source-location-list fst) ctc-cache))])
-                                  (void (register-extra-defs! ex*))
-                                  (if fst+ (cons fst+ check*) check*))))])
+                              (cond
+                                [(or (identifier? args)
+                                     (null? args)
+                                     (and (syntax? args) (null? (syntax-e args))))
+                                 '()]
+                                [else
+                                 (define-values (fst rst)
+                                   (cond
+                                     [(pair? args) (values (car args) (cdr args))]
+                                     [(syntax? args)
+                                      (let ([e (syntax-e args)]) (values (car e) (cdr e)))]
+                                     [else
+                                      (raise-syntax-error 'shallow-rewrite-top
+                                                          "#%plain-lambda formals"
+                                                          #'formals
+                                                          args)]))
+                                 (define check*
+                                   (let ([dom+ (for/fold ([acc '()]) ([dom (in-list dom*)])
+                                                 (if (pair? dom)
+                                                     (cons (cdr dom) acc)
+                                                     acc))])
+                                     (protect-loop rst dom+)))
+                                 (define fst-ty
+                                   (let ([ann-ty (and (type-annotation fst #:infer #f)
+                                                      (get-type fst #:infer #t #:default Univ))])
+                                     (if (and ann-ty (not (Error? ann-ty)))
+                                         ann-ty
+                                         (apply Un
+                                                (for/list ([dom (in-list dom*)]
+                                                           #:when (pair? dom))
+                                                  (car dom))))))
+                                 (define-values (ex* fst+)
+                                   (if skip-dom?
+                                       (values '() #f)
+                                       (protect-domain fst-ty
+                                                       fst
+                                                       (build-source-location-list fst)
+                                                       ctc-cache)))
+                                 (void (register-extra-defs! ex*))
+                                 (if fst+
+                                     (cons fst+ check*)
+                                     check*)]))])
                      (if (null? check-formal*)
                        body+
                        (cons
@@ -272,11 +284,11 @@
                             ;; no type
                             (quasisyntax/loc formals [#,formals . #,body])]
                            [else
+                             (define len (formals-length formals))
                              (define matching-dom*
-                               (let ([len (formals-length formals)])
-                                 (for/list ((dom (in-list all-dom*))
-                                            #:when (= len (length dom)))
-                                   dom)))
+                               (for/list ([dom (in-list all-dom*)]
+                                          #:when (= len (length dom)))
+                                 dom))
                              (quasisyntax/loc stx
                                [#,formals .
                                 #,(let* ([body+
@@ -284,38 +296,50 @@
                                          [check-formal*
                                            (let protect-loop ([args formals]
                                                               [dom* matching-dom*])
-                                             (if (or (identifier? args)
-                                                     (null? args)
-                                                     (and (syntax? args) (null? (syntax-e args))))
-                                               '()
-                                               (let*-values ([(fst rst)
-                                                              (cond
-                                                                [(pair? args)
-                                                                 (values (car args) (cdr args))]
-                                                                [(syntax? args)
-                                                                 (let ((e (syntax-e args)))
-                                                                   (values (car e) (cdr e)))]
-                                                                [else
-                                                                  (raise-syntax-error 'shallow-rewrite-top "#%plain-lambda formals" formals args)])]
-                                                             [(check*)
-                                                              (let ((dom+
-                                                                    (for/fold ((acc '()))
-                                                                              ((dom (in-list dom*)))
-                                                                      (if (pair? dom) (cons (cdr dom) acc) acc))))
-                                                                (protect-loop rst dom+))]
-                                                             [(fst-ty)
-                                                              (if (type-annotation fst #:infer #f)
-                                                                (get-type fst #:infer #t #:default Univ)
-                                                                (apply Un
-                                                                       (for/fold ((acc '()))
-                                                                                 ((dom (in-list dom*)))
-                                                                         (if (pair? dom) (cons (car dom) acc) acc))))]
-                                                             [(ex* fst+)
-                                                              (if skip-dom?
-                                                                (values '() #f)
-                                                                (protect-domain fst-ty fst (build-source-location-list fst) ctc-cache))])
-                                                 (void (register-extra-defs! ex*))
-                                                 (if fst+ (cons fst+ check*) check*))))])
+                                             (cond
+                                               [(or (identifier? args)
+                                                    (null? args)
+                                                    (and (syntax? args) (null? (syntax-e args))))
+                                                '()]
+                                               [else
+                                                (define-values (fst rst)
+                                                  (cond
+                                                    [(pair? args) (values (car args) (cdr args))]
+                                                    [(syntax? args)
+                                                     (let ([e (syntax-e args)])
+                                                       (values (car e) (cdr e)))]
+                                                    [else
+                                                     (raise-syntax-error 'shallow-rewrite-top
+                                                                         "#%plain-lambda formals"
+                                                                         formals
+                                                                         args)]))
+                                                (define check*
+                                                  (let ([dom+ (for/fold ([acc '()])
+                                                                        ([dom (in-list dom*)])
+                                                                (if (pair? dom)
+                                                                    (cons (cdr dom) acc)
+                                                                    acc))])
+                                                    (protect-loop rst dom+)))
+                                                (define fst-ty
+                                                  (if (type-annotation fst #:infer #f)
+                                                      (get-type fst #:infer #t #:default Univ)
+                                                      (apply Un
+                                                             (for/fold ([acc '()])
+                                                                       ([dom (in-list dom*)])
+                                                               (if (pair? dom)
+                                                                   (cons (car dom) acc)
+                                                                   acc)))))
+                                                (define-values (ex* fst+)
+                                                  (if skip-dom?
+                                                      (values '() #f)
+                                                      (protect-domain fst-ty
+                                                                      fst
+                                                                      (build-source-location-list fst)
+                                                                      ctc-cache)))
+                                                (void (register-extra-defs! ex*))
+                                                (if fst+
+                                                    (cons fst+ check*)
+                                                    check*)]))])
                                    (if (null? check-formal*)
                                      body+
                                      (cons
@@ -415,9 +439,9 @@
   stx)
 
 (define (maybe-add-typeof-expr new-stx old-stx)
-  (let ((old-type (maybe-type-of old-stx)))
-    (when old-type
-      (add-typeof-expr new-stx old-type))))
+  (define old-type (maybe-type-of old-stx))
+  (when old-type
+    (add-typeof-expr new-stx old-type)))
 
 (define (maybe-add-test-position new-stx old-stx)
   (maybe-add-test-true new-stx old-stx)
@@ -425,9 +449,9 @@
   (void))
 
 (define (maybe-add-scoped-tvar new-stx old-stx)
-  (let ([old-layer (lookup-scoped-tvar-layer old-stx)])
-    (when old-layer
-      (add-scoped-tvars new-stx old-layer))))
+  (define old-layer (lookup-scoped-tvar-layer old-stx))
+  (when old-layer
+    (add-scoped-tvars new-stx old-layer)))
 
 (define (maybe-add-test-true new-stx old-stx)
   (when (test-position-takes-true-branch old-stx)
@@ -449,20 +473,15 @@
 
 (define (formals-fold init f stx)
   (let loop ((v stx))
-    (if (or (identifier? v)
-            (null? v)
-            (and (syntax? v) (null? (syntax-e v))))
-      init
-      (let*-values (((fst rst)
-                     (cond
-                       [(pair? v)
-                        (values (car v) (cdr v))]
-                       [(syntax? v)
-                        (let ((e (syntax-e v)))
-                          (values (car e) (cdr e)))]
-                       [else
-                         (raise-syntax-error 'formals-fold "lambda formals" stx)])))
-        (f (loop rst) fst)))))
+    (cond
+      [(or (identifier? v) (null? v) (and (syntax? v) (null? (syntax-e v)))) init]
+      [else
+       (define-values (fst rst)
+         (cond
+           [(pair? v) (values (car v) (cdr v))]
+           [(syntax? v) (let ([e (syntax-e v)]) (values (car e) (cdr e)))]
+           [else (raise-syntax-error 'formals-fold "lambda formals" stx)]))
+       (f (loop rst) fst)])))
 
 ;; is-application? : Syntax -> Boolean
 ;; Returns #true if `stx` is a function application (an app that may need dynamic checking)
@@ -629,12 +648,10 @@
     (λ (mpi)
       (hash-ref! cache mpi
         (λ () ;; Typed Racket always installs a `#%type-decl` submodule
-          (let* ([mpi+ (module-path-index-join '(submod "." #%type-decl) mpi)])
-            (parameterize ([current-namespace (make-base-namespace)])
-              (with-handlers ([exn:fail:contract? (lambda (exn) #f)])
-                (and mpi+
-                     (dynamic-require mpi+ #f)
-                     #t)))))))))
+          (define mpi+ (module-path-index-join '(submod "." #%type-decl) mpi))
+          (parameterize ([current-namespace (make-base-namespace)])
+            (with-handlers ([exn:fail:contract? (lambda (exn) #f)])
+              (and mpi+ (dynamic-require mpi+ #f) #t))))))))
 
 (define (protect-domain dom-type dom-stx ctx ctc-cache)
   (define-values [extra-def* ctc-stx]
@@ -714,10 +731,7 @@
     [(eq? t Univ)
      (values '() #f)]
     [else
-     (define (fail #:reason r)
-       (raise-user-error 'type->flat-contract "failed to convert type ~a to flat contract because ~a" t r))
-     (match-define (list defs ctc)
-       (type->contract t fail #:typed-side 'both #:cache ctc-cache))
+     (match-define (list defs ctc) (type->contract t fail #:typed-side 'both #:cache ctc-cache))
      (match t
       [(Refine: _ _)
        ;; do not lift defs; they may use a local var
diff --git a/typed-racket-lib/typed-racket/private/syntax-properties.rkt b/typed-racket-lib/typed-racket/private/syntax-properties.rkt
index ff753e9a6..7ffd48f85 100644
--- a/typed-racket-lib/typed-racket/private/syntax-properties.rkt
+++ b/typed-racket-lib/typed-racket/private/syntax-properties.rkt
@@ -1,7 +1,8 @@
 #lang racket/base
-(require
-  syntax/parse/pre
-  (for-syntax racket/base syntax/parse/pre racket/syntax))
+(require (for-syntax racket/base
+                     racket/syntax
+                     syntax/parse/pre)
+         syntax/parse/pre)
 
 (define-syntax define-matcher
   (syntax-parser
diff --git a/typed-racket-lib/typed-racket/private/type-annotation.rkt b/typed-racket-lib/typed-racket/private/type-annotation.rkt
index c714b5805..a826de157 100644
--- a/typed-racket-lib/typed-racket/private/type-annotation.rkt
+++ b/typed-racket-lib/typed-racket/private/type-annotation.rkt
@@ -89,46 +89,49 @@
    (listof tc-result?))
   (match stxs
     [(list stx ...)
-     (let ([anns (for/list ([s (in-list stxs)])
-                   (cond
-                     ;; if the lhs identifier is the rest parameter, its type is
-                     ;; (Listof ty), where ty is the annotated type
-                     [(rst-arg-property s)
-                      (make-Listof (type-annotation s #:infer #t))]
-                     [else (type-annotation s #:infer #t)]))])
-       (if (for/and ([a (in-list anns)]) a)
-           (match (tc-expr/check expr (ret anns))
-             [(tc-results: tcrs _) tcrs])
-           (match (tc-expr expr)
-             [(tc-any-results: _)
-              (tc-error/expr
-               #:return (map (λ _ (-tc-result -Bottom)) stxs)
-               "Expression should produce ~a values, but produces an unknown number of values"
-               (length stxs))]
-             [(tc-result1: (== -Bottom))
-              (for/list ([_ (in-range (length stxs))])
-                (-tc-result -Bottom))]
-             [(tc-results: tcrs _)
-              (cond
-                [(not (= (length stxs) (length tcrs)))
-                 (tc-error/expr #:return (map (λ _ (-tc-result -Bottom)) stxs)
-                                "Expression should produce ~a values, but produces ~a values of types ~a"
-                                (length stxs)
-                                (length tcrs)
-                                (stringify (map tc-result-t tcrs)))]
-                [else
-                 (for/list ([stx (in-list stxs)]
-                            [tcr (in-list tcrs)]
-                            [a   (in-list anns)])
-                   (match tcr
-                     [(tc-result: ty ps o)
-                      (cond [a (check-type stx ty a)
-                               (-tc-result a ps o)]
-                            ;; mutated variables get generalized, so that we don't
-                            ;; infer too small a type
-                            [(is-var-mutated? stx)
-                             (-tc-result (generalize ty) ps o)]
-                            [else (-tc-result ty ps o)])]))])])))]))
+     (define anns
+       (for/list ([s (in-list stxs)])
+         (cond
+           ;; if the lhs identifier is the rest parameter, its type is
+           ;; (Listof ty), where ty is the annotated type
+           [(rst-arg-property s) (make-Listof (type-annotation s #:infer #t))]
+           [else (type-annotation s #:infer #t)])))
+     (if (for/and ([a (in-list anns)])
+           a)
+         (match (tc-expr/check expr (ret anns))
+           [(tc-results: tcrs _) tcrs])
+         (match (tc-expr expr)
+           [(tc-any-results: _)
+            (tc-error/expr
+             #:return (map (λ _ (-tc-result -Bottom)) stxs)
+             "Expression should produce ~a values, but produces an unknown number of values"
+             (length stxs))]
+           [(tc-result1: (== -Bottom))
+            (for/list ([_ (in-range (length stxs))])
+              (-tc-result -Bottom))]
+           [(tc-results: tcrs _)
+            (cond
+              [(not (= (length stxs) (length tcrs)))
+               (tc-error/expr
+                #:return (map (λ _ (-tc-result -Bottom)) stxs)
+                "Expression should produce ~a values, but produces ~a values of types ~a"
+                (length stxs)
+                (length tcrs)
+                (stringify (map tc-result-t tcrs)))]
+              [else
+               (for/list ([stx (in-list stxs)]
+                          [tcr (in-list tcrs)]
+                          [a (in-list anns)])
+                 (match tcr
+                   [(tc-result: ty ps o)
+                    (cond
+                      [a
+                       (check-type stx ty a)
+                       (-tc-result a ps o)]
+                      ;; mutated variables get generalized, so that we don't
+                      ;; infer too small a type
+                      [(is-var-mutated? stx) (-tc-result (generalize ty) ps o)]
+                      [else (-tc-result ty ps o)])]))])]))]))
 
 ;; check that e-type is compatible with ty in context of stx
 ;; otherwise, error
diff --git a/typed-racket-lib/typed-racket/private/type-contract.rkt b/typed-racket-lib/typed-racket/private/type-contract.rkt
index 988018b7b..5cfcf2e09 100644
--- a/typed-racket-lib/typed-racket/private/type-contract.rkt
+++ b/typed-racket-lib/typed-racket/private/type-contract.rkt
@@ -239,10 +239,11 @@
 (define (change-contract-fixups forms [ctc-cache (make-hash)])
   (with-new-name-tables
    (for/list ((e (in-list forms)))
-     (if (not (has-contract-def-property? e))
-         e
-         (begin (set-box! include-extra-requires? #t)
-                (generate-contract-def e ctc-cache))))))
+     (cond
+       [(not (has-contract-def-property? e)) e]
+       [else
+        (set-box! include-extra-requires? #t)
+        (generate-contract-def e ctc-cache)]))))
 
 ;; TODO: These are probably all in a specific place, which could avoid
 ;;       the big traversal
@@ -386,8 +387,8 @@
         (loop t (flip-side typed-side) recursive-values))
       (define (t->sc/both t #:recursive-values (recursive-values recursive-values))
         (loop t 'both recursive-values))
-      (define (t->sc/fun t #:maybe-existential [opt-exi #f]) (t->sc/function t fail typed-side recursive-values loop #f #:maybe-existential opt-exi))
-      (define (t->sc/meth t) (t->sc/method t fail typed-side recursive-values loop))
+      (define (t->sc/meth t)
+        (t->sc/method t fail typed-side recursive-values loop))
 
       (define (struct->recursive-sc name-base key flds sc-ctor)
         (define key* (generate-temporary name-base))
@@ -554,13 +555,11 @@
         ;; Avoid putting (-> any T) contracts on struct predicates (where Boolean <: T)
         ;; Optimization: if the value is typed, we can assume it's not wrapped
         ;;  in a type-unsafe chaperone/impersonator and use the unsafe contract
-        (let* ([unsafe-spp/sc (flat/sc #'struct-predicate-procedure?)]
-               [safe-spp/sc (flat/sc #'struct-predicate-procedure?/c)]
-               [optimized/sc (if (from-typed? typed-side)
-                                 unsafe-spp/sc
-                                 safe-spp/sc)]
-               [spt-pred-procedure?/sc (flat/sc #'struct-type-property-predicate-procedure?)])
-          (or/sc optimized/sc spt-pred-procedure?/sc (t->sc/fun t)))]
+        (define unsafe-spp/sc (flat/sc #'struct-predicate-procedure?))
+        (define safe-spp/sc (flat/sc #'struct-predicate-procedure?/c))
+        (define optimized/sc (if (from-typed? typed-side) unsafe-spp/sc safe-spp/sc))
+        (define spt-pred-procedure?/sc (flat/sc #'struct-type-property-predicate-procedure?))
+        (or/sc optimized/sc spt-pred-procedure?/sc (t->sc/fun t))]
        [(? Fun? t) (t->sc/fun t)]
        [(? DepFun? t) (t->sc/fun t)]
        [(Set: t) (set/sc (t->sc t))]
@@ -835,10 +834,10 @@
            [else (is-flat-type/sc (obj->sc o) sc)])]
         [(NotTypeProp: o t)
          (define sc (t->sc t bound-all-vars))
-         (cond
-           [(not (equal? flat-sym (get-max-contract-kind sc)))
-            (raise-user-error 'type->static-contract/shallow "proposition contract generation not supported for non-flat types")]
-           [else (not-flat-type/sc (obj->sc o) sc)])]
+         (unless (equal? flat-sym (get-max-contract-kind sc))
+           (raise-user-error 'type->static-contract/shallow
+                             "proposition contract generation not supported for non-flat types"))
+         (not-flat-type/sc (obj->sc o) sc)]
         [(LeqProp: (app obj->sc lhs) (app obj->sc rhs))
          (leq/sc lhs rhs)]
         [(AndProp: ps)
@@ -1136,28 +1135,25 @@
 (define (t->sc/function f fail typed-side recursive-values loop method? #:maybe-existential [opt-exi #f])
   (define (t->sc t #:recursive-values (recursive-values recursive-values))
     (loop t typed-side recursive-values))
-  (define (t->sc/neg t #:recursive-values (recursive-values recursive-values))
-    (loop t (flip-side typed-side) recursive-values))
-
   (define (arr-params->exist/sc exi dom rst kw rng prop+type)
     (define (occur? t)
-      (if (or (not t) (empty? t)) #f
+      (if (or (not t) (empty? t))
+          #f
           (set-member? (free-vars-names (free-vars* t)) exi)))
-
+  
     (match* (rng prop+type)
       [((Fun: (list (Arrow: (list-rest (F: n1) a ... _) rst_i kw_i _))) (F: n1))
-       #:when (and (not (ormap occur? (list rst kw rst_i kw_i)))
-                   (eq? n1 exi))
+       #:when (and (not (ormap occur? (list rst kw rst_i kw_i))) (eq? n1 exi))
        (void)]
-      [(_ _) (fail #:reason
-                   "contract generation only supports Some Type in this form: (Some (X) (-> ty1 ... (-> X ty ... ty2) : X)) or (-> ty1 ... (Some (X) (-> X ty ... ty2) : X))")])
-
+      [(_ _)
+       (fail
+        #:reason
+        "contract generation only supports Some Type in this form: (Some (X) (-> ty1 ... (-> X ty ... ty2) : X)) or (-> ty1 ... (Some (X) (-> X ty ... ty2) : X))")])
+  
     (define/with-syntax name exi)
     (define lhs (t->sc/neg dom))
     (define eq-name (flat/sc #'(eq/c name)))
-    (define rhs (t->sc rng
-                       #:recursive-values (hash-set recursive-values exi
-                                                    (same eq-name))))
+    (define rhs (t->sc rng #:recursive-values (hash-set recursive-values exi (same eq-name))))
     (exist/sc (list #'name) lhs rhs))
 
 
@@ -1165,10 +1161,8 @@
   ;; Match the range of an arr and determine if a contract can be generated
   ;; and call the given thunk or raise an error
   (define (handle-arrow-range arrow proceed)
-    (match arrow
-      [(or (Arrow: _ _ _ rng)
-           (DepFun: _ _ rng))
-       (handle-range rng proceed)]))
+    (match-define (or (Arrow: _ _ _ rng) (DepFun: _ _ rng)) arrow)
+    (handle-range rng proceed))
   (define (handle-range rng proceed)
     (match rng
       [(Values: (list (Result: _
@@ -1267,8 +1261,7 @@
              (when (and (not (empty? kws)))
                (fail #:reason (~a "cannot generate contract for case function type"
                                   " with optional keyword arguments")))
-             (when (ormap (lambda (n-exi)
-                            (> n-exi 0))
+             (when (ormap positive?
                           n-exis)
                (fail #:reason (~a "cannot generate contract for case function type with existentials")))
 
@@ -1287,51 +1280,35 @@
             (handle-arrow-range (first arrows)
                                 (lambda ()
                                   (convert-single-arrow (first arrows))))
-            (case->/sc (map (lambda (arr)
-                              (handle-arrow-range arr (lambda ()
-                                                        (convert-one-arrow-in-many arr))))
-                            arrows)))])]
+            (case->/sc (for/list ([arr (in-list arrows)])
+                         (handle-arrow-range arr (lambda () (convert-one-arrow-in-many arr))))))])]
     [(DepFun/ids: ids dom pre rng)
      (define (continue)
-       (match rng
-         [(Values: (list (Result: rngs _ _) ...))
-          (define (dom-id? id) (member id ids free-identifier=?))
-          (define-values (dom* dom-deps)
-            (for/lists (_1 _2) ([d (in-list dom)])
-              (values (t->sc/neg d)
-                      (filter dom-id? (free-ids d)))))
-          (define pre* (if (TrueProp? pre) #f (t->sc/neg pre)))
-          (define pre-deps (filter dom-id? (free-ids pre)))
-          (define rng* (map t->sc rngs))
-          (define rng-deps (filter dom-id?
-                                   (remove-duplicates
-                                    (apply append (map free-ids rngs))
-                                    free-identifier=?)))
-          (->i/sc (from-typed? typed-side)
-                  ids
-                  dom*
-                  dom-deps
-                  pre*
-                  pre-deps
-                  rng*
-                  rng-deps)]))
+       (match-define (Values: (list (Result: rngs _ _) ...)) rng)
+       (define (dom-id? id)
+         (member id ids free-identifier=?))
+       (define-values (dom* dom-deps)
+         (for/lists (_1 _2) ([d (in-list dom)]) (values (t->sc/neg d) (filter dom-id? (free-ids d)))))
+       (define pre*
+         (if (TrueProp? pre)
+             #f
+             (t->sc/neg pre)))
+       (define pre-deps (filter dom-id? (free-ids pre)))
+       (define rng* (map t->sc rngs))
+       (define rng-deps
+         (filter dom-id? (remove-duplicates (apply append (map free-ids rngs)) free-identifier=?)))
+       (->i/sc (from-typed? typed-side) ids dom* dom-deps pre* pre-deps rng* rng-deps))
      (handle-range rng continue)]))
 
 ;; Generate a contract for a object/class method clause
 ;; Precondition: type is a valid method type
 (define (t->sc/method type fail typed-side recursive-values loop)
   ;; helper for mutually recursive calls in Poly cases
-  (define (rec body #:recursive-values rv)
-    (t->sc/method body fail typed-side rv loop))
   (match type
-    [(? Poly?)
-     (t->sc/poly type fail typed-side recursive-values rec)]
-    [(? PolyDots?)
-     (t->sc/polydots type fail typed-side recursive-values rec)]
-    [(? PolyRow?)
-     (t->sc/polyrow type fail typed-side recursive-values rec)]
-    [(? Fun?)
-     (t->sc/function type fail typed-side recursive-values loop #t)]
+    [(? Poly?) (t->sc/poly type fail typed-side recursive-values rec)]
+    [(? PolyDots?) (t->sc/polydots type fail typed-side recursive-values rec)]
+    [(? PolyRow?) (t->sc/polyrow type fail typed-side recursive-values rec)]
+    [(? Fun?) (t->sc/function type fail typed-side recursive-values loop #t)]
     [_ (fail #:reason "invalid method type")]))
 
 (define (is-a-function-type? initial)
@@ -1546,11 +1523,16 @@
   (require racket/extflonum)
   (provide nonnegative? nonpositive?
            extflonum? extflzero? extflnonnegative? extflnonpositive?)
-  (define nonnegative? (lambda (x) (>= x 0)))
-  (define nonpositive? (lambda (x) (<= x 0)))
-  (define extflzero? (lambda (x) (extfl= x 0.0t0)))
-  (define extflnonnegative? (lambda (x) (extfl>= x 0.0t0)))
-  (define extflnonpositive? (lambda (x) (extfl<= x 0.0t0))))
+  (define (nonnegative? x)
+    (>= x 0))
+  (define (nonpositive? x)
+    (<= x 0))
+  (define (extflzero? x)
+    (extfl= x 0.0t0))
+  (define (extflnonnegative? x)
+    (extfl>= x 0.0t0))
+  (define (extflnonpositive? x)
+    (extfl<= x 0.0t0)))
 
 (module numeric-contracts racket/base
   (require
diff --git a/typed-racket-lib/typed-racket/private/user-defined-type-constr.rkt b/typed-racket-lib/typed-racket/private/user-defined-type-constr.rkt
index 0f9f51ee3..6f3d1ce2d 100644
--- a/typed-racket-lib/typed-racket/private/user-defined-type-constr.rkt
+++ b/typed-racket-lib/typed-racket/private/user-defined-type-constr.rkt
@@ -1,7 +1,7 @@
 #lang racket/base
-(require "../rep/type-constr.rkt"
+(require racket/lazy-require
          racket/match
-         racket/lazy-require)
+         "../rep/type-constr.rkt")
 
 (lazy-require ["../types/substitute.rkt"
                (subst-all make-simple-substitution)])
@@ -30,7 +30,8 @@
     [_ #f]))
 
 (define (recursive-type-constr? constr)
-  (match constr
-    [(struct* TypeConstructor
-              ([real-trep-constr (struct* user-defined-type-op ([recursive? recursive?]))]))
-     recursive?]))
+  (match-define (struct* TypeConstructor
+                         ([real-trep-constr
+                           (struct* user-defined-type-op ([recursive? recursive?]))]))
+    constr)
+  recursive?)
diff --git a/typed-racket-lib/typed-racket/private/with-types.rkt b/typed-racket-lib/typed-racket/private/with-types.rkt
index ce24257c4..20bc9f113 100644
--- a/typed-racket-lib/typed-racket/private/with-types.rkt
+++ b/typed-racket-lib/typed-racket/private/with-types.rkt
@@ -1,46 +1,84 @@
 #lang racket/base
 
-(require "../utils/utils.rkt"
-         "../base-env/base-types-extra.rkt"
+(require (for-template (except-in racket/base
+                                  for
+                                  for*
+                                  with-handlers
+                                  with-handlers*
+                                  lambda
+                                  λ
+                                  define
+                                  let
+                                  let*
+                                  letrec
+                                  letrec-values
+                                  let-values
+                                  let*-values
+                                  let/cc
+                                  let/ec
+                                  do
+                                  case-lambda
+                                  struct
+                                  define-struct
+                                  default-continuation-prompt-tag
+                                  for/list
+                                  for/vector
+                                  for/hash
+                                  for/hasheq
+                                  for/hasheqv
+                                  for/hashalw
+                                  for/and
+                                  for/or
+                                  for/sum
+                                  for/product
+                                  for/lists
+                                  for/first
+                                  for/last
+                                  for/fold
+                                  for/foldr
+                                  for*/list
+                                  for*/lists
+                                  for*/vector
+                                  for*/hash
+                                  for*/hasheq
+                                  for*/hasheqv
+                                  for*/hashalw
+                                  for*/and
+                                  for*/or
+                                  for*/sum
+                                  for*/product
+                                  for*/first
+                                  for*/last
+                                  for*/fold
+                                  for*/foldr)
+                       (prefix-in c: racket/contract/region)
+                       "../base-env/prims.rkt")
+         (for-label racket/base
+                    "../base-env/base-types-extra.rkt")
+         racket/promise
+         racket/sequence
+         racket/syntax
+         syntax/flatten-begin
+         syntax/parse
          (except-in "../base-env/prims.rkt" with-handlers λ lambda define)
-         "../env/type-name-env.rkt"
-         "../env/type-alias-env.rkt"
+         "../base-env/base-types-extra.rkt"
          "../env/global-env.rkt"
-         "parse-type.rkt"
-         "type-contract.rkt"
-         "syntax-properties.rkt"
+         "../env/type-alias-env.rkt"
+         "../env/type-name-env.rkt"
+         "../standard-inits.rkt"
+         "../tc-setup.rkt"
          "../typecheck/tc-toplevel.rkt"
          "../typecheck/typechecker.rkt"
          "../types/utils.rkt"
-         "../utils/lift.rkt"
-         "../utils/tc-utils.rkt"
-         "../utils/disarm.rkt"
          "../utils/arm.rkt"
+         "../utils/disarm.rkt"
+         "../utils/lift.rkt"
          "../utils/literal-syntax-class.rkt"
-         racket/promise
-         racket/syntax
-         syntax/flatten-begin
-         syntax/parse
-         racket/sequence
-         "../tc-setup.rkt"
-         "../standard-inits.rkt"
-         (for-template
-          (except-in racket/base for for* with-handlers with-handlers*
-                     lambda λ define
-                     let let* letrec letrec-values let-values let*-values
-                     let/cc let/ec do case-lambda struct define-struct
-                     default-continuation-prompt-tag
-                     for/list for/vector for/hash for/hasheq for/hasheqv for/hashalw
-                     for/and for/or for/sum for/product for/lists
-                     for/first for/last for/fold for/foldr for*/list for*/lists
-                     for*/vector for*/hash for*/hasheq for*/hasheqv for*/hashalw
-                     for*/and
-                     for*/or for*/sum for*/product for*/first for*/last
-                     for*/fold for*/foldr)
-          "../base-env/prims.rkt"
-          (prefix-in c: racket/contract/region))
-         (for-label racket/base
-                    "../base-env/base-types-extra.rkt"))
+         "../utils/tc-utils.rkt"
+         "../utils/utils.rkt"
+         "parse-type.rkt"
+         "syntax-properties.rkt"
+         "type-contract.rkt")
 
 (define-literal-syntax-class #:for-label Values)
 (define-literal-syntax-class #:for-label values)
@@ -50,7 +88,7 @@
 (define (with-type-helper stx body fvids fvtys exids extys resty expr? ctx te-mode)
   (define old-context (unbox typed-context?))
   (define old-te-mode (unbox type-enforcement-mode))
-  (unless (not old-context)
+  (when old-context
     (tc-error/stx stx (format "with-type cannot be used in a typed module. ~a " old-context)))
   (set-box! typed-context? #t)
   (set-box! type-enforcement-mode te-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..418080a8c 100644
--- a/typed-racket-lib/typed-racket/typecheck/check-below.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/check-below.rkt
@@ -1,19 +1,20 @@
 #lang racket/base
 
-(require "../utils/utils.rkt"
-         racket/match (prefix-in - (contract-req))
-         racket/format
+(require racket/format
+         racket/match
+         (prefix-in - (contract-req))
          "../env/lexical-env.rkt"
-         "../types/utils.rkt"
-         "../types/subtype.rkt"
-         "../types/prop-ops.rkt"
+         "../rep/object-rep.rkt"
+         "../rep/prop-rep.rkt"
+         "../rep/type-rep.rkt"
          "../types/abbrev.rkt"
+         "../types/prop-ops.rkt"
+         "../types/subtype.rkt"
          "../types/tc-result.rkt"
-         "../utils/tc-utils.rkt"
+         "../types/utils.rkt"
          "../utils/shallow-utils.rkt"
-         "../rep/type-rep.rkt"
-         "../rep/object-rep.rkt"
-         "../rep/prop-rep.rkt"
+         "../utils/tc-utils.rkt"
+         "../utils/utils.rkt"
          "error-message.rkt"
          "tc-envops.rkt")
 
@@ -83,40 +84,30 @@
   (define (prop-better? p1 p2)
     (or (not p2)
         (implies? p1 p2)))
-  (define (RestDots-better? rdots1 rdots2)
-    (match* (rdots1 rdots2)
-      [(rd rd) #t]
-      [((RestDots: dty1 dbound)
-        (RestDots: dty2 dbound))
-       (subtype dty1 dty2)]
-      [(_ _) #f]))
-
   (match* (tr1 expected)
-
+  
     [((tc-result1: t1 p1 o1) (? Type? t2))
      (cond
        [(with-refinements?)
-        (with-naively-extended-lexical-env
-            [#:props (list (-is-type o1 t1)
-                           (-or (PropSet-thn p1) (PropSet-els p1)))]
-          (unless (subtype t1 t2 o1)
-            (expected-but-got t2 t1)))]
-       [else (unless (subtype t1 t2 o1)
-               (expected-but-got t2 t1))])
+        (with-naively-extended-lexical-env [#:props (list (-is-type o1 t1)
+                                                          (-or (PropSet-thn p1) (PropSet-els p1)))]
+                                           (unless (subtype t1 t2 o1)
+                                             (expected-but-got t2 t1)))]
+       [else
+        (unless (subtype t1 t2 o1)
+          (expected-but-got t2 t1))])
      (upgrade-trusted-rng t1 t2)]
     ;; This case has to be first so that bottom (exceptions, etc.) can be allowed in cases
     ;; where multiple values are expected.
     ;; We can ignore the props and objects in the actual value because they would never be about a value
-    [((tc-result1: (? Bottom?)) _)
-     (fix-results/bottom expected)]
-
+    [((tc-result1: (? Bottom?)) _) (fix-results/bottom expected)]
+  
     [((tc-any-results: p1) (tc-any-results: p2))
      (unless (prop-better? p1 p2)
        (type-mismatch p2 p1 "mismatch in proposition"))
      (-tc-any-results (fix-props p2 p1))]
-
-    [((tc-results: tcrs _)
-      (tc-any-results: p2))
+  
+    [((tc-results: tcrs _) (tc-any-results: p2))
      (define merged-prop
        (apply -and
               (map (match-lambda
@@ -125,77 +116,65 @@
      (unless (prop-better? merged-prop p2)
        (type-mismatch p2 merged-prop "mismatch in proposition"))
      (-tc-any-results (fix-props p2 merged-prop))]
-
+  
     [((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")])
        (ret (upgrade-trusted-rng t1 t2) (fix-props p2 p1) (fix-object o2 o1)))
      (cond
        [(with-refinements?)
-        (with-naively-extended-lexical-env
-            [#:props (list (-is-type o1 t1)
-                           (-or (PropSet-thn p1) (PropSet-els p1)))]
-          (perform-check!))]
+        (with-naively-extended-lexical-env [#:props (list (-is-type o1 t1)
+                                                          (-or (PropSet-thn p1) (PropSet-els p1)))]
+                                           (perform-check!))]
        [else (perform-check!)])]
-
+  
     ;; case where expected is like (Values a ... a) but got something else
     [((tc-results: _ #f) (tc-results: _ (? RestDots?)))
      (value-mismatch expected tr1)
      (fix-results expected)]
-
+  
     ;; case where you have (Values a ... a) but expected something else
     [((tc-results: _ (? RestDots?)) (tc-results: _ #f))
      (value-mismatch expected tr1)
      (fix-results expected)]
-
+  
     ;; case where both have no '...', or both have '...'
-    [((tc-results: tcrs1 db1)
-      (tc-results: tcrs2 db2))
+    [((tc-results: tcrs1 db1) (tc-results: tcrs2 db2))
      (cond
        [(= (length tcrs1) (length tcrs2))
-        (unless (andmap (match-lambda**
-                         [((tc-result: t1 ps1 o1)
-                           (tc-result: t2 ps2 o2))
-                          (and (subtype t1 t2 o1)
-                               (prop-set-better? ps1 ps2)
-                               (object-better? o1 o2))])
-                        tcrs1
-                        tcrs2)
-          (expected-but-got (stringify (map tc-result-t tcrs1))
-                            (stringify (map tc-result-t tcrs2))))
+        (unless (andmap
+                 (match-lambda**
+                   [((tc-result: t1 ps1 o1) (tc-result: t2 ps2 o2))
+                    (and (subtype t1 t2 o1) (prop-set-better? ps1 ps2) (object-better? o1 o2))])
+                 tcrs1
+                 tcrs2)
+          (expected-but-got (stringify (map tc-result-t tcrs1)) (stringify (map tc-result-t tcrs2))))
         (match* (db1 db2)
-          [((RestDots: dty1 dbound1)
-            (RestDots: dty2 dbound2))
-           #:when (not (and (eq? dbound1 dbound2)
-                            (subtype dty1 dty2)))
+          [((RestDots: dty1 dbound1) (RestDots: dty2 dbound2))
+           #:when (not (and (eq? dbound1 dbound2) (subtype dty1 dty2)))
            (type-mismatch dty2 dty1 "mismatch in ... argument")]
           [(_ _) (void)])]
-       [else
-        (value-mismatch expected tr1)])
+       [else (value-mismatch expected tr1)])
      (fix-results expected)]
-
+  
     [((tc-any-results: _) (? tc-results?))
      (value-mismatch expected tr1)
      (fix-results expected)]
-
+  
     [((? Type? t1) (? Type? t2))
      (unless (subtype t1 t2)
        (expected-but-got t2 t1))
      (upgrade-trusted-rng t1 expected)]
-
+  
     [(a b) (int-err "unexpected input for check-below: ~a ~a" a b)]))
 
 ;; shallow: if the top-level arrow on t1 is reliable, then upgrade the top-level arrow in t2
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/integer-refinements.rkt b/typed-racket-lib/typed-racket/typecheck/integer-refinements.rkt
index 2a6f18883..cb64b043b 100644
--- a/typed-racket-lib/typed-racket/typecheck/integer-refinements.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/integer-refinements.rkt
@@ -1,17 +1,17 @@
 #lang racket/base
 
-(require "../utils/utils.rkt"
+(require (for-syntax racket/base)
+         racket/match
+         syntax/parse
+         syntax/private/id-table
          (prefix-in c: (contract-req))
          "../types/abbrev.rkt"
-         "../types/subtype.rkt"
          "../types/numeric-tower.rkt"
          "../types/prop-ops.rkt"
+         "../types/subtype.rkt"
          "../types/tc-result.rkt"
          "../types/type-table.rkt"
-         racket/match
-         syntax/private/id-table
-         syntax/parse
-         (for-syntax racket/base))
+         "../utils/utils.rkt")
 
 (provide/cond-contract
  [has-linear-integer-refinements? (c:-> identifier? boolean?)]
@@ -71,19 +71,19 @@
            #: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?)
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/tc-expr-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
index 336eaeb09..4dcc784fc 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
diff --git a/typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt b/typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt
index 29aacdf6c..4b5b3c15c 100644
--- a/typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt
@@ -8,9 +8,9 @@
 ;; take over and keep head local-expanding until `begin` forms are exhausted,
 ;; at which point the syntax can be fully-expanded and checked normally.
 
-(require syntax/parse
-         "../private/syntax-properties.rkt"
-         (for-template racket/base))
+(require (for-template racket/base)
+         syntax/parse
+         "../private/syntax-properties.rkt")
 
 (provide tc-toplevel-start)
 
@@ -36,39 +36,39 @@
                        syntax/kerncase
                        syntax/parse
                        syntax/stx
-                       "../rep/values-rep.rkt"
+                       (only-in "../types/subtype.rkt" subtype)
+                       "../env/mvar-env.rkt"
                        "../optimizer/optimizer.rkt"
                        "../private/shallow-rewrite.rkt"
-                       "../types/utils.rkt"
+                       "../private/syntax-properties.rkt"
+                       "../private/type-contract.rkt"
+                       "../rep/values-rep.rkt"
                        "../types/abbrev.rkt"
                        "../types/printer.rkt"
                        "../types/tc-result.rkt"
-                       "tc-toplevel.rkt"
-                       "../private/type-contract.rkt"
-                       "../private/syntax-properties.rkt"
-                       (only-in "../types/subtype.rkt" subtype)
-                       "../env/mvar-env.rkt"
+                       "../types/utils.rkt"
+                       "../utils/arm.rkt"
                        "../utils/disarm.rkt"
                        "../utils/lift.rkt"
-                       "../utils/utils.rkt"
-                       "../utils/timing.rkt"
+                       "../utils/mutated-vars.rkt"
                        "../utils/tc-utils.rkt"
-                       "../utils/arm.rkt"
-                       "../utils/mutated-vars.rkt"))
+                       "../utils/timing.rkt"
+                       "../utils/utils.rkt"
+                       "tc-toplevel.rkt"))
 
   (provide tc-toplevel-trampoline
            tc-toplevel-trampoline/report)
 
   (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)