From a0560d88d07cca5d82ccdfa5a1de12d3ba48b0dc Mon Sep 17 00:00:00 2001
From: "resyntax-ci[bot]" <181813515+resyntax-ci[bot]@users.noreply.github.com>
Date: Fri, 20 Dec 2024 00:33:26 +0000
Subject: [PATCH 01/12] Fix 1 occurrence of `zero-comparison-to-positive?`

This expression is equivalent to calling the `positive?` predicate.
---
 typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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)))

From 280ee69f5defcec0f9b063d0e5b694ba0a63b75d Mon Sep 17 00:00:00 2001
From: "resyntax-ci[bot]" <181813515+resyntax-ci[bot]@users.noreply.github.com>
Date: Fri, 20 Dec 2024 00:33:26 +0000
Subject: [PATCH 02/12] Fix 6 occurrences of
 `single-clause-match-to-match-define`

This `match` expression can be simplified using `match-define`.
---
 .../typecheck/tc-app/tc-app-lambda.rkt         |  4 ++--
 .../typecheck/tc-app/tc-app-values.rkt         |  5 +++--
 .../typed-racket/typecheck/tc-expr-unit.rkt    |  4 ++--
 .../typed-racket/typecheck/tc-structs.rkt      | 18 ++++++++----------
 4 files changed, 15 insertions(+), 16 deletions(-)

diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
index 4eaf0f242..21a6e7e5c 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
@@ -46,8 +46,8 @@
    (let* ([res (tc/let-values #'((x) ...) #'(args ...) #'body expected)]
           [dom-ts
            (for/list ([arg (in-list (syntax-e #'(args ...)))])
-             (match (type-of arg)
-              [(tc-result1: t) t]))]
+             (match-define (tc-result1: t) (type-of arg))
+             t)]
           [cod-t (tc-results->values res)])
      (add-typeof-expr #'lam (ret (->* dom-ts cod-t :T+ #t)))
      res))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt
index 574126137..90ec93407 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt
@@ -68,8 +68,9 @@
          (-tc-results
            (for/list ([arg (in-syntax #'args)]
                       [tcr (in-list/rest tcrs #f)])
-             (match (single-value arg (and tcr (-tc-results (list tcr) #f)))
-               [(tc-results: (list res) #f) res])) #f))
+             (match-define (tc-results: (list res) #f)
+               (single-value arg (and tcr (-tc-results (list tcr) #f))))
+             res) #f))
        (define return-ty (tc-results->values res))
        (define arg-tys (match return-ty [(Values: (list (Result: t* _ _) ...)) t*]))
        (add-typeof-expr #'op-name (ret (->* arg-tys return-ty :T+ #t)))
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..aa3819be5 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)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index 66496b11b..061656729 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]
@@ -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)

From 959bce1e6e5e64518bd1049ebd495e85ab0a2db0 Mon Sep 17 00:00:00 2001
From: "resyntax-ci[bot]" <181813515+resyntax-ci[bot]@users.noreply.github.com>
Date: Fri, 20 Dec 2024 00:33:26 +0000
Subject: [PATCH 03/12] Fix 5 occurrences of `let-to-define`

Internal definitions are recommended instead of `let` expressions, to reduce nesting.
---
 .../typecheck/tc-app/tc-app-lambda.rkt        |   8 +-
 .../typed-racket/typecheck/tc-envops.rkt      | 112 +++++++++---------
 .../typed-racket/typecheck/tc-expr-unit.rkt   |   4 +-
 .../typed-racket/typecheck/tc-structs.rkt     |   6 +-
 4 files changed, 65 insertions(+), 65 deletions(-)

diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
index 21a6e7e5c..2d7e8a86a 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
@@ -82,10 +82,10 @@
      (let* ([ts1 (generalize (tc-expr/t #'actual))]
             [ann-ts (for/list ([a (in-syntax #'(acc ...))]
                                [ac (in-syntax #'(actuals ...))])
-                      (let ([type (find-annotation #'inner-body a)])
-                        (if type
-                            (tc-expr/check/t ac (ret type))
-                            (generalize (tc-expr/t ac)))))]
+                      (define type (find-annotation #'inner-body a))
+                      (if type
+                          (tc-expr/check/t ac (ret type))
+                          (generalize (tc-expr/t ac))))]
             [ts (cons ts1 ann-ts)])
        ;; check that the actual arguments are ok here
        (for/list ([a (in-syntax #'(actuals ...))]
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
index e440fab57..db8b5ffaa 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
@@ -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 aa3819be5..b7083e28b 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
@@ -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)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index 061656729..ff83230e9 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
@@ -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))

From d89f5c539e9885bcc41efe4afdf43d599692a5d7 Mon Sep 17 00:00:00 2001
From: "resyntax-ci[bot]" <181813515+resyntax-ci[bot]@users.noreply.github.com>
Date: Fri, 20 Dec 2024 00:33:26 +0000
Subject: [PATCH 04/12] Fix 13 occurrences of `tidy-require`

Keep imports in `require` sorted and grouped by phase, with collections before files.
---
 .../typecheck/provide-handling.rkt            | 10 +++---
 .../typecheck/tc-app-combined.rkt             | 10 +++---
 .../typecheck/tc-app/tc-app-contracts.rkt     | 14 ++++----
 .../typecheck/tc-app/tc-app-eq.rkt            | 24 +++++++------
 .../typecheck/tc-app/tc-app-hetero.rkt        | 34 +++++++++++--------
 .../typecheck/tc-app/tc-app-main.rkt          | 33 ++++++++----------
 .../typecheck/tc-app/tc-app-objects.rkt       | 19 ++++++-----
 .../typecheck/tc-app/tc-app-values.rkt        | 26 +++++++-------
 .../typed-racket/typecheck/tc-app/utils.rkt   |  7 ++--
 typed-racket-lib/typed/untyped-utils.rkt      |  6 ++--
 .../external/historical-counterexamples.rkt   |  5 ++-
 .../external/tr-random-testing.rkt            | 17 ++++++----
 12 files changed, 112 insertions(+), 93 deletions(-)

diff --git a/typed-racket-lib/typed-racket/typecheck/provide-handling.rkt b/typed-racket-lib/typed-racket/typecheck/provide-handling.rkt
index e3e665b47..0895a9f5e 100644
--- a/typed-racket-lib/typed-racket/typecheck/provide-handling.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/provide-handling.rkt
@@ -1,13 +1,13 @@
 #lang racket/base
 
-(require "../utils/utils.rkt"
+(require (for-syntax racket/base)
+         (for-template racket/base)
          racket/sequence
          syntax/parse
-         "../private/syntax-properties.rkt"
-         "def-binding.rkt"
          "../env/env-utils.rkt"
-         (for-syntax racket/base)
-         (for-template racket/base))
+         "../private/syntax-properties.rkt"
+         "../utils/utils.rkt"
+         "def-binding.rkt")
 
 (provide remove-provides provide? generate-prov)
 
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app-combined.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app-combined.rkt
index fe6fb00ba..e447ad6b4 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app-combined.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app-combined.rkt
@@ -1,17 +1,17 @@
 #lang racket/base
 
-(require "tc-app/tc-app-apply.rkt"
+(require "signatures.rkt"
+         "tc-app/tc-app-apply.rkt"
+         "tc-app/tc-app-contracts.rkt"
          "tc-app/tc-app-eq.rkt"
          "tc-app/tc-app-hetero.rkt"
          "tc-app/tc-app-keywords.rkt"
          "tc-app/tc-app-lambda.rkt"
          "tc-app/tc-app-list.rkt"
+         "tc-app/tc-app-main.rkt"
          "tc-app/tc-app-objects.rkt"
          "tc-app/tc-app-special.rkt"
-         "tc-app/tc-app-values.rkt"
-         "tc-app/tc-app-contracts.rkt"
-         "tc-app/tc-app-main.rkt"
-         "signatures.rkt")
+         "tc-app/tc-app-values.rkt")
 
 (require racket/unit)
 (provide tc-app-combined@)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-contracts.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-contracts.rkt
index e3288a296..f67726360 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-contracts.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-contracts.rkt
@@ -3,16 +3,16 @@
 ;; This module provides custom type-checking rules for the expansion
 ;; of contracted values
 
-(require "../../utils/utils.rkt"
-         "signatures.rkt"
-         "utils.rkt"
+(require (for-template racket/base
+                       ;; shift -1 because it's provided +1
+                       racket/contract/private/provide)
          syntax/parse
-         "../signatures.rkt"
          (only-in typed-racket/types/type-table add-typeof-expr)
          (only-in typed-racket/types/tc-result ret)
-         (for-template racket/base
-                       ;; shift -1 because it's provided +1
-                       racket/contract/private/provide))
+         "../../utils/utils.rkt"
+         "../signatures.rkt"
+         "signatures.rkt"
+         "utils.rkt")
 
 (import tc-expr^)
 (export tc-app-contracts^)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-eq.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-eq.rkt
index f0864d4ff..baec6d393 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-eq.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-eq.rkt
@@ -1,19 +1,23 @@
 #lang racket/unit
 
-(require "../../utils/utils.rkt"
-         "signatures.rkt"
-         "utils.rkt"
+(require (for-label racket/base
+                    racket/bool)
+         racket/match
+         racket/unsafe/undefined
+         syntax/parse
+         syntax/stx
          (only-in "../../infer/infer.rkt" intersect)
-         syntax/parse syntax/stx racket/match racket/unsafe/undefined
-         "../signatures.rkt"
-         "../tc-funapp.rkt"
+         "../../rep/object-rep.rkt"
+         "../../rep/type-rep.rkt"
          "../../types/abbrev.rkt"
+         "../../types/match-expanders.rkt"
          "../../types/prop-ops.rkt"
          "../../types/utils.rkt"
-         "../../types/match-expanders.rkt"
-         "../../rep/type-rep.rkt"
-         "../../rep/object-rep.rkt"
-         (for-label racket/base racket/bool))
+         "../../utils/utils.rkt"
+         "../signatures.rkt"
+         "../tc-funapp.rkt"
+         "signatures.rkt"
+         "utils.rkt")
 
 (import tc-expr^)
 (export tc-app-eq^)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
index ed3d9622d..c342c4965 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
@@ -1,26 +1,32 @@
 #lang racket/unit
 
-(require "../../utils/utils.rkt"
+(require (for-syntax racket/base
+                     racket/syntax
+                     syntax/parse)
+         (for-label racket/base
+                    racket/unsafe/ops)
          racket/list
-         syntax/parse syntax/stx racket/match racket/sequence
-         (for-syntax racket/base syntax/parse racket/syntax)
-         "signatures.rkt"
-         "utils.rkt"
-         "../../utils/prefab.rkt"
+         racket/match
+         racket/sequence
+         syntax/parse
+         syntax/stx
          (only-in "../../infer/infer.rkt" intersect)
-         "../../types/utils.rkt"
+         "../../rep/rep-utils.rkt"
+         "../../rep/type-mask.rkt"
+         "../../rep/type-rep.rkt"
          "../../types/abbrev.rkt"
+         "../../types/generalize.rkt"
+         "../../types/match-expanders.rkt"
          "../../types/numeric-tower.rkt"
          "../../types/resolve.rkt"
          "../../types/type-table.rkt"
-         "../../types/generalize.rkt"
-         "../../types/match-expanders.rkt"
-         "../signatures.rkt"
+         "../../types/utils.rkt"
+         "../../utils/prefab.rkt"
+         "../../utils/utils.rkt"
          "../check-below.rkt"
-         "../../rep/type-rep.rkt"
-         "../../rep/type-mask.rkt"
-         "../../rep/rep-utils.rkt"
-         (for-label racket/unsafe/ops racket/base))
+         "../signatures.rkt"
+         "signatures.rkt"
+         "utils.rkt")
 
 (import tc-expr^ tc-app^ tc-literal^)
 (export tc-app-hetero^)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-main.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-main.rkt
index a6d8ec7f7..1c0e405d3 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-main.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-main.rkt
@@ -1,29 +1,26 @@
 #lang racket/unit
 
-(require "../../utils/utils.rkt"
-         "signatures.rkt"
-         "utils.rkt"
-         "../../utils/tc-utils.rkt"
+(require racket/match
+         syntax/parse
+         syntax/parse/experimental/reflect
          "../../env/lexical-env.rkt"
-         "../../rep/type-rep.rkt"
-         "../../rep/prop-rep.rkt"
          "../../rep/object-rep.rkt"
+         "../../rep/prop-rep.rkt"
+         "../../rep/type-rep.rkt"
          "../../rep/values-rep.rkt"
-         syntax/parse racket/match
-         syntax/parse/experimental/reflect
-         "../signatures.rkt" "../tc-funapp.rkt"
-         "../integer-refinements.rkt"
          "../../types/abbrev.rkt"
-         "../../types/utils.rkt"
          "../../types/prop-ops.rkt"
-         "../../env/lexical-env.rkt"
-         "../tc-subst.rkt"
-         "../tc-envops.rkt"
+         "../../types/utils.rkt"
+         "../../utils/tc-utils.rkt"
+         "../../utils/utils.rkt"
          "../check-below.rkt"
-         "../../rep/type-rep.rkt"
-         "../../rep/prop-rep.rkt"
-         "../../rep/object-rep.rkt"
-         "../../rep/values-rep.rkt")
+         "../integer-refinements.rkt"
+         "../signatures.rkt"
+         "../tc-envops.rkt"
+         "../tc-funapp.rkt"
+         "../tc-subst.rkt"
+         "signatures.rkt"
+         "utils.rkt")
 
 (import tc-expr^ tc-app-keywords^
         tc-app-hetero^ tc-app-list^ tc-app-apply^ tc-app-values^
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-objects.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-objects.rkt
index 3c9c2c0db..b55fc58f8 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-objects.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-objects.rkt
@@ -1,21 +1,24 @@
 #lang racket/unit
 
-(require "../../utils/utils.rkt"
-         "signatures.rkt"
-         "utils.rkt"
-         syntax/parse syntax/stx racket/match racket/sequence
+(require (for-template racket/base)
+         (for-label racket/base)
          racket/format
          racket/list
-         "../signatures.rkt"
+         racket/match
+         racket/sequence
+         syntax/parse
+         syntax/stx
+         "../../rep/type-rep.rkt"
          "../../types/base-abbrev.rkt"
          "../../types/resolve.rkt"
          "../../types/subtype.rkt"
          "../../types/type-table.rkt"
          "../../types/utils.rkt"
-         "../../rep/type-rep.rkt"
          "../../utils/tc-utils.rkt"
-         (for-template racket/base)
-         (for-label racket/base))
+         "../../utils/utils.rkt"
+         "../signatures.rkt"
+         "signatures.rkt"
+         "utils.rkt")
 
 
 (import tc-expr^)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt
index 90ec93407..ce2d75fa0 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt
@@ -1,20 +1,22 @@
 #lang racket/unit
 
-(require "../../utils/utils.rkt"
-         "signatures.rkt"
-         "utils.rkt"
-         syntax/parse racket/match racket/sequence racket/list
-         "../signatures.rkt"
-         "../tc-funapp.rkt"
-         "../tc-metafunctions.rkt"
-         "../../types/base-abbrev.rkt"
+(require (for-label racket/base)
+         racket/list
+         racket/match
+         racket/sequence
+         syntax/parse
+         typed-racket/utils/shallow-utils
+         "../../rep/values-rep.rkt"
          "../../types/abbrev.rkt"
+         "../../types/base-abbrev.rkt"
          "../../types/type-table.rkt"
          "../../types/utils.rkt"
-         "../../rep/values-rep.rkt"
-         typed-racket/utils/shallow-utils
-
-         (for-label racket/base))
+         "../../utils/utils.rkt"
+         "../signatures.rkt"
+         "../tc-funapp.rkt"
+         "../tc-metafunctions.rkt"
+         "signatures.rkt"
+         "utils.rkt")
 
 
 (import tc-expr^ tc-app^)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/utils.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/utils.rkt
index bebf670d4..5433711e6 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/utils.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/utils.rkt
@@ -1,8 +1,9 @@
 #lang racket/base
 
-(require syntax/parse
-         syntax/parse/experimental/reflect
-         (for-syntax racket/base syntax/parse))
+(require (for-syntax racket/base
+                     syntax/parse)
+         syntax/parse
+         syntax/parse/experimental/reflect)
 
 (provide define-reified-syntax-class define-tc/app-syntax-class)
 
diff --git a/typed-racket-lib/typed/untyped-utils.rkt b/typed-racket-lib/typed/untyped-utils.rkt
index 4545aaafc..85fb87438 100644
--- a/typed-racket-lib/typed/untyped-utils.rkt
+++ b/typed-racket-lib/typed/untyped-utils.rkt
@@ -1,11 +1,11 @@
 #lang racket/base
 
 (require (for-syntax racket/base
+                     racket/syntax
                      syntax/parse
                      syntax/stx
-                     racket/syntax
-                     typed-racket/utils/tc-utils
-                     typed-racket/typecheck/renamer)
+                     typed-racket/typecheck/renamer
+                     typed-racket/utils/tc-utils)
          typed-racket/utils/tc-utils)
 
 (provide syntax-local-typed-context?
diff --git a/typed-racket-test/external/historical-counterexamples.rkt b/typed-racket-test/external/historical-counterexamples.rkt
index 82b1cf92e..215c1bbae 100644
--- a/typed-racket-test/external/historical-counterexamples.rkt
+++ b/typed-racket-test/external/historical-counterexamples.rkt
@@ -1,6 +1,9 @@
 #lang racket/base
 
-(require "tr-random-testing.rkt" racket/runtime-path racket/file racket/list)
+(require racket/file
+         racket/list
+         racket/runtime-path
+         "tr-random-testing.rkt")
 
 ;; list of all the counterexamples that the random tester found on drdr,
 ;; as of drdr run #32529
diff --git a/typed-racket-test/external/tr-random-testing.rkt b/typed-racket-test/external/tr-random-testing.rkt
index cdb13b790..722b2da45 100644
--- a/typed-racket-test/external/tr-random-testing.rkt
+++ b/typed-racket-test/external/tr-random-testing.rkt
@@ -2,16 +2,19 @@
 
 ;; Random testing of the TR numeric base environment, and numeric optimizations
 
-(require redex/reduction-semantics
-         racket/flonum racket/unsafe/ops
-         racket/runtime-path racket/sandbox racket/cmdline
+(require racket/cmdline
+         racket/flonum
+         racket/runtime-path
+         racket/sandbox
+         racket/unsafe/ops
+         redex/reduction-semantics
          "random-real.rkt")
 
-(require typed-racket/utils/utils
-         typed-racket/typecheck/typechecker
-         typed-racket/utils/tc-utils
+(require typed-racket/typecheck/typechecker
          typed-racket/types/subtype
-         typed-racket/types/utils)
+         typed-racket/types/utils
+         typed-racket/utils/tc-utils
+         typed-racket/utils/utils)
 
 (require (prefix-in b: typed-racket/base-env/base-env)
          (prefix-in n: typed-racket/base-env/base-env-numeric))

From 57568bbe394ec0a4213f2f8ac1c04e19240a31d8 Mon Sep 17 00:00:00 2001
From: "resyntax-ci[bot]" <181813515+resyntax-ci[bot]@users.noreply.github.com>
Date: Fri, 20 Dec 2024 00:33:26 +0000
Subject: [PATCH 05/12] Fix 1 occurrence of `if-x-else-x-to-and`

This conditional expression can be replaced with a simpler, equivalent expression.
---
 .../typed-racket/typecheck/tc-envops.rkt       | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
index db8b5ffaa..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]

From 3554fa64a46ea73be30e8d35738ec1e13ff317c1 Mon Sep 17 00:00:00 2001
From: "resyntax-ci[bot]" <181813515+resyntax-ci[bot]@users.noreply.github.com>
Date: Fri, 20 Dec 2024 00:33:26 +0000
Subject: [PATCH 06/12] Fix 2 occurrences of `map-to-for`

This `map` operation can be replaced with a `for/list` loop.
---
 .../typed-racket/typecheck/tc-structs.rkt     | 45 ++++++++++---------
 .../performance/infer-timing.rkt              |  6 +--
 2 files changed, 25 insertions(+), 26 deletions(-)

diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index ff83230e9..7f391d921 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
@@ -511,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-test/performance/infer-timing.rkt b/typed-racket-test/performance/infer-timing.rkt
index 72e09b02b..3176cd6a2 100644
--- a/typed-racket-test/performance/infer-timing.rkt
+++ b/typed-racket-test/performance/infer-timing.rkt
@@ -64,10 +64,8 @@
   ;; once we have a set of props that are true/false based on reaching
   ;; a certain point, this will be more useful
   (define (fx-from-cases . cases)
-    (apply from-cases (map (lambda (x)
-                             (add-unconditional-prop-all-args
-                              x -Fixnum))
-                           (flatten cases))))
+    (apply from-cases (for/list ([x (in-list (flatten cases))])
+                        (add-unconditional-prop-all-args x -Fixnum))))
 
   (define (binop t [r t])
     (t t . -> . r))

From 58f9b9a5d622db0ef1a75ca626a1f1d050c7b36f Mon Sep 17 00:00:00 2001
From: "resyntax-ci[bot]" <181813515+resyntax-ci[bot]@users.noreply.github.com>
Date: Fri, 20 Dec 2024 00:33:26 +0000
Subject: [PATCH 07/12] Fix 9 occurrences of `define-lambda-to-define`

The `define` form supports a shorthand for defining functions.
---
 .../typecheck/integer-refinements.rkt         | 224 ++++++++----------
 .../performance/infer-timing.rkt              |   3 +-
 2 files changed, 106 insertions(+), 121 deletions(-)

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-test/performance/infer-timing.rkt b/typed-racket-test/performance/infer-timing.rkt
index 3176cd6a2..c095da01e 100644
--- a/typed-racket-test/performance/infer-timing.rkt
+++ b/typed-racket-test/performance/infer-timing.rkt
@@ -405,7 +405,8 @@
   (displayln `(big ,n))
   (define ty-list (append ts ts))
   (collect-garbage) (collect-garbage) (collect-garbage)
-  (define run (λ () (void (bigcall n ty-list))))
+  (define (run)
+    (void (bigcall n ty-list)))
   (cond [hsbencher
          (define-values (vs t r gc)
            (time-apply run null))

From 489f8c926322282387ded3e0b0c4561738bb0055 Mon Sep 17 00:00:00 2001
From: "resyntax-ci[bot]" <181813515+resyntax-ci[bot]@users.noreply.github.com>
Date: Fri, 20 Dec 2024 00:33:26 +0000
Subject: [PATCH 08/12] Fix 1 occurrence of `format-identity`

This use of `format` does nothing.
---
 typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 b7083e28b..4dcc784fc 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
@@ -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

From 8e83b1aafdc26d634c8e288a0c540d2746faa22a Mon Sep 17 00:00:00 2001
From: "resyntax-ci[bot]" <181813515+resyntax-ci[bot]@users.noreply.github.com>
Date: Fri, 20 Dec 2024 00:33:26 +0000
Subject: [PATCH 09/12] Fix 2 occurrences of `if-begin-to-cond`

Using `cond` instead of `if` here makes `begin` unnecessary
---
 .../typed-racket/typecheck/tc-expr-unit.rkt            |  8 +++++---
 typed-racket-test/external/tr-random-testing.rkt       | 10 +++++-----
 2 files changed, 10 insertions(+), 8 deletions(-)

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 4dcc784fc..e26f1ccda 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
@@ -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-test/external/tr-random-testing.rkt b/typed-racket-test/external/tr-random-testing.rkt
index 722b2da45..495fd2074 100644
--- a/typed-racket-test/external/tr-random-testing.rkt
+++ b/typed-racket-test/external/tr-random-testing.rkt
@@ -337,11 +337,11 @@
           )))
   (or both-failed?
       (and (not racket-failed?)
-           (if (same-result? racket-result racketbc-result)
-               #t
-               (begin (printf "not same as bc: racketcs: ~s racketbc: ~s\n"
-                              racket-result racketbc-result)
-                      #f)))))
+           (cond
+             [(same-result? racket-result racketbc-result) #t]
+             [else
+              (printf "not same as bc: racketcs: ~s racketbc: ~s\n" racket-result racketbc-result)
+              #f]))))
 
 (define num-exceptions 0)
 

From 97c1968ad24295db4e2dba78b1b057882a0ceb1f Mon Sep 17 00:00:00 2001
From: "resyntax-ci[bot]" <181813515+resyntax-ci[bot]@users.noreply.github.com>
Date: Fri, 20 Dec 2024 00:33:26 +0000
Subject: [PATCH 10/12] Fix 1 occurrence of `zero-comparison-to-negative?`

This expression is equivalent to calling the `negative?` predicate.
---
 .../typed-racket/typecheck/tc-app/tc-app-hetero.rkt             | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
index c342c4965..196a81dfa 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
@@ -57,7 +57,7 @@
   (cond
     [(not (and (integer? i-val) (exact? i-val)))
      (tc-error/expr #:stx expr "expected exact integer for ~a index, but got ~a" name i-val)]
-    [(< i-val 0)
+    [(negative? i-val)
      (tc-error/expr #:stx expr "index ~a too small for ~a ~a" i-val name type)]
     [(not (< i-val i-bound))
      (tc-error/expr #:stx expr "index ~a too large for ~a ~a" i-val name type)]))

From 273d389f2b5a54d79e2dea6352e9d006f7cd1fc7 Mon Sep 17 00:00:00 2001
From: "resyntax-ci[bot]" <181813515+resyntax-ci[bot]@users.noreply.github.com>
Date: Fri, 20 Dec 2024 00:33:26 +0000
Subject: [PATCH 11/12] Fix 1 occurrence of `and-match-to-match`

This `and` expression can be turned into a clause of the inner `match` expression, reducing nesting.
---
 .../typed-racket/typecheck/possible-domains.rkt        | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

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

From a1333288a3ca886639fac3b1098e53b0acca7710 Mon Sep 17 00:00:00 2001
From: "resyntax-ci[bot]" <181813515+resyntax-ci[bot]@users.noreply.github.com>
Date: Fri, 20 Dec 2024 00:33:26 +0000
Subject: [PATCH 12/12] Fix 1 occurrence of `let-to-define`

Internal definitions are recommended instead of `let` expressions, to reduce nesting.
---
 typed-racket-lib/typed-racket/typecheck/tc-structs.rkt | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index 7f391d921..3afd62dd8 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
@@ -195,8 +195,8 @@
           (loop (cddr l) (cons (car l) getters) (cons (cadr l) 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)))
+  (define-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]