diff --git a/typed-racket-lib/typed-racket/private/shallow-rewrite.rkt b/typed-racket-lib/typed-racket/private/shallow-rewrite.rkt
index bf1d1a124..e9cb715b2 100644
--- a/typed-racket-lib/typed-racket/private/shallow-rewrite.rkt
+++ b/typed-racket-lib/typed-racket/private/shallow-rewrite.rkt
@@ -232,27 +232,29 @@
                                    (cond
                                      [(pair? args) (values (car args) (cdr args))]
                                      [(syntax? args)
-                                      (let ([e (syntax-e args)]) (values (car e) (cdr e)))]
+                                      (define 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))])
+                                   (let ([dom+ (for/fold ([acc '()])
+                                                         ([dom (in-list dom*)]
+                                                          #:when (pair? dom))
+                                                 (cons (cdr dom) acc))])
                                      (protect-loop rst dom+)))
+                                 (define ann-ty
+                                   (and (type-annotation fst #:infer #f)
+                                        (get-type fst #:infer #t #:default Univ)))
                                  (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))))))
+                                   (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)
@@ -306,29 +308,27 @@
                                                   (cond
                                                     [(pair? args) (values (car args) (cdr args))]
                                                     [(syntax? args)
-                                                     (let ([e (syntax-e args)])
-                                                       (values (car e) (cdr e)))]
+                                                     (define 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 dom+
+                                                  (for/fold ([acc '()])
+                                                            ([dom (in-list dom*)]
+                                                             #:when (pair? dom))
+                                                    (cons (cdr dom) acc)))
+                                                (define check* (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)))))
+                                                                       ([dom (in-list dom*)]
+                                                                        #:when (pair? dom))
+                                                               (cons (car dom) acc)))))
                                                 (define-values (ex* fst+)
                                                   (if skip-dom?
                                                       (values '() #f)
@@ -479,7 +479,8 @@
        (define-values (fst rst)
          (cond
            [(pair? v) (values (car v) (cdr v))]
-           [(syntax? v) (let ([e (syntax-e v)]) (values (car e) (cdr e)))]
+           [(syntax? v) (define e (syntax-e v))
+                        (values (car e) (cdr e))]
            [else (raise-syntax-error 'formals-fold "lambda formals" stx)]))
        (f (loop rst) fst)])))
 
diff --git a/typed-racket-lib/typed-racket/private/type-annotation.rkt b/typed-racket-lib/typed-racket/private/type-annotation.rkt
index a826de157..4226e8499 100644
--- a/typed-racket-lib/typed-racket/private/type-annotation.rkt
+++ b/typed-racket-lib/typed-racket/private/type-annotation.rkt
@@ -122,16 +122,15 @@
                (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)])]))])]))]))
+                 (match-define (tc-result: ty ps o) tcr)
+                 (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 c01edbb43..460c7b383 100644
--- a/typed-racket-lib/typed-racket/private/type-contract.rkt
+++ b/typed-racket-lib/typed-racket/private/type-contract.rkt
@@ -830,10 +830,10 @@
       (match p
         [(TypeProp: 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 (is-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"))
+         (is-flat-type/sc (obj->sc o) sc)]
         [(NotTypeProp: o t)
          (define sc (t->sc t bound-all-vars))
          (unless (equal? flat-sym (get-max-contract-kind sc))
diff --git a/typed-racket-lib/typed-racket/rep/base-union.rkt b/typed-racket-lib/typed-racket/rep/base-union.rkt
index c68b8cdb2..bdcffa2c7 100644
--- a/typed-racket-lib/typed-racket/rep/base-union.rkt
+++ b/typed-racket-lib/typed-racket/rep/base-union.rkt
@@ -59,10 +59,8 @@
                      (app BaseUnion-bases bases)))])))
 
 (define (BaseUnion-bases t)
-  (match t
-    [(BaseUnion: bbits nbits)
-     (cond
-       [(eqv? bbits 0) (nbits->base-types nbits)]
-       [(eqv? nbits 0) (bbits->base-types bbits)]
-       [else (append (bbits->base-types bbits)
-                     (nbits->base-types nbits))])]))
+  (match-define (BaseUnion: bbits nbits) t)
+  (cond
+    [(eqv? bbits 0) (nbits->base-types nbits)]
+    [(eqv? nbits 0) (bbits->base-types bbits)]
+    [else (append (bbits->base-types bbits) (nbits->base-types nbits))]))
diff --git a/typed-racket-lib/typed-racket/rep/core-rep.rkt b/typed-racket-lib/typed-racket/rep/core-rep.rkt
index 3e32e576f..c3178cf4d 100644
--- a/typed-racket-lib/typed-racket/rep/core-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/core-rep.rkt
@@ -247,7 +247,7 @@
   (-> Result? Result?)
   (match-define (Result: type propset optobject n-existentials) result)
   (cond
-    [(> n-existentials 0)
+    [(positive? n-existentials)
      (define syms (hash-ref type-var-name-table result (build-list n-existentials (lambda _ (gensym)))))
      (define vars (map make-F syms))
      (make-Result (instantiate-type type vars) (instantiate-propset propset vars) optobject n-existentials)]
diff --git a/typed-racket-lib/typed-racket/rep/free-ids.rkt b/typed-racket-lib/typed-racket/rep/free-ids.rkt
index f069dd39a..6c8235874 100644
--- a/typed-racket-lib/typed-racket/rep/free-ids.rkt
+++ b/typed-racket-lib/typed-racket/rep/free-ids.rkt
@@ -69,11 +69,9 @@
     (cond
       [(member x seen free-identifier=?) (cons x seen)]
       [else
-       (begin0
-         (let ([seen+x (cons x seen)])
-           (for/or ([neighbor (in-list (cdr (assoc x deps free-identifier=?)))])
-             (and (not (member neighbor visited free-identifier=?))
-                  (visit neighbor seen+x))))
+       (define seen+x (cons x seen))
+       (begin0 (for/or ([neighbor (in-list (cdr (assoc x deps free-identifier=?)))])
+                 (and (not (member neighbor visited free-identifier=?)) (visit neighbor seen+x)))
          (set! visited (cons x visited)))]))
   (match (for/or ([entry (in-list deps)])
            (visit (car entry) '()))
diff --git a/typed-racket-lib/typed-racket/rep/free-variance.rkt b/typed-racket-lib/typed-racket/rep/free-variance.rkt
index 7a97a12c6..2d16803c1 100644
--- a/typed-racket-lib/typed-racket/rep/free-variance.rkt
+++ b/typed-racket-lib/typed-racket/rep/free-variance.rkt
@@ -123,18 +123,14 @@
     (for/fold ([hash (hasheq)]
                [computed null])
               ([frees (in-list freess)])
-      (match frees
-        [(combined-frees new-hash new-computed)
-         (values (combine-hashes (list hash new-hash))
-                 (append new-computed computed))])))
+      (match-define (combined-frees new-hash new-computed) frees)
+      (values (combine-hashes (list hash new-hash)) (append new-computed computed))))
   (combined-frees hash computed))
 
 
 (define (free-vars-remove frees name)
-  (match frees
-    [(combined-frees hash computed)
-     (combined-frees (hash-remove hash name)
-                     (map (λ (v) (remove-frees v name)) computed))]))
+  (match-define (combined-frees hash computed) frees)
+  (combined-frees (hash-remove hash name) (map (λ (v) (remove-frees v name)) computed)))
 
 ;;
 (define (free-vars-names vars)
diff --git a/typed-racket-lib/typed-racket/rep/object-rep.rkt b/typed-racket-lib/typed-racket/rep/object-rep.rkt
index 418563b55..d9b1e3212 100644
--- a/typed-racket-lib/typed-racket/rep/object-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/object-rep.rkt
@@ -268,10 +268,10 @@
       [(list (? exact-integer? coeff) (? Path? p))
        (values c (terms-set ts p (+ coeff (terms-ref ts p))))]
       [(list (? exact-integer? coeff) (? name-ref/c nm))
-       (let ([p (-id-path nm)])
-         (if (Empty? nm)
-             (values c ts)
-             (values c (terms-set ts p (+ coeff (terms-ref ts p))))))]
+       (define p (-id-path nm))
+       (if (Empty? nm)
+           (values c ts)
+           (values c (terms-set ts p (+ coeff (terms-ref ts p)))))]
       [(? exact-integer? new-const)
        (values (+ new-const c) ts)]
       [(LExp: c* ts*)
@@ -313,9 +313,7 @@
   (-> OptObject? (or/c #f exact-integer?))
   (match l
     [(LExp: c terms)
-     (if (hash-empty? terms)
-         c
-         #f)]
+     (and (hash-empty? terms) c)]
     [_ #f]))
 
 (define/cond-contract (in-LExp? obj l)
@@ -388,6 +386,5 @@
      (make-LExp* (+ c1 c2) (terms-add terms1 terms2))]))
 
 (define (add-path-to-lexp p l)
-  (match l
-    [(LExp: const terms)
-     (make-LExp* const (terms-set terms p (add1 (terms-ref terms p))))]))
+  (match-define (LExp: const terms) l)
+  (make-LExp* const (terms-set terms p (add1 (terms-ref terms p)))))
diff --git a/typed-racket-lib/typed-racket/rep/prop-rep.rkt b/typed-racket-lib/typed-racket/rep/prop-rep.rkt
index 953332504..069950753 100644
--- a/typed-racket-lib/typed-racket/rep/prop-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/prop-rep.rkt
@@ -143,8 +143,7 @@
   [#:for-each (f) (for-each f ps)]
   [#:custom-constructor/contract
    (-> (listof (or/c TypeProp? NotTypeProp? LeqProp?)) OrProp?)
-   (let ([ps (sort ps (λ (p q) (unsafe-fx<= (eq-hash-code p)
-                                            (eq-hash-code q))))])
+   (let ([ps (sort ps unsafe-fx<= #:key eq-hash-code)])
      (intern-single-ref!
       orprop-intern-table
       ps
diff --git a/typed-racket-lib/typed-racket/rep/rep-switch.rkt b/typed-racket-lib/typed-racket/rep/rep-switch.rkt
index 97be1d125..d260e76c8 100644
--- a/typed-racket-lib/typed-racket/rep/rep-switch.rkt
+++ b/typed-racket-lib/typed-racket/rep/rep-switch.rkt
@@ -35,7 +35,7 @@
         (~var clause (switch-clause #'(pre-args ...) #'arg #'(post-args ...))) ...
         [(~datum else:) . default])
      (define name-symbols (map syntax->datum (syntax->list #'(clause.name ...))))
-     (unless (not (null? name-symbols))
+     (when (null? name-symbols)
        (raise-syntax-error 'define-switch "switch cannot be null" stx))
      (define sorted-name-symbols (sort name-symbols symbol<?))
      (unless (eq? (first name-symbols) (first sorted-name-symbols))
diff --git a/typed-racket-lib/typed-racket/rep/rep-utils.rkt b/typed-racket-lib/typed-racket/rep/rep-utils.rkt
index 1a01e562a..18bd1027b 100644
--- a/typed-racket-lib/typed-racket/rep/rep-utils.rkt
+++ b/typed-racket-lib/typed-racket/rep/rep-utils.rkt
@@ -117,9 +117,7 @@
 ;; NOTE: the #:construct expression is only run if there
 ;; is no interned copy, so we should avoid unnecessary
 ;; allocation w/ this approach
-(define-simple-macro (intern-single-ref! table-exp:expr
-                                         key-exp:expr
-                                         #:construct val-exp:expr)
+(define-syntax-parse-rule (intern-single-ref! table-exp:expr key-exp:expr #:construct val-exp:expr)
   (let ([table table-exp])
     (define key key-exp)
     (define intern-box (hash-ref table key #f))
@@ -132,13 +130,11 @@
 
 ;; fetches an interned Rep based on the given _two_ keys
 ;; see 'intern-single-ref!'
-(define-simple-macro (intern-double-ref! table:id
-                                         key-exp1:expr
-                                         key-exp2:expr
-                                         #:construct val-exp:expr)
-  (intern-single-ref! (hash-ref! table key-exp1 make-hash)
-                      key-exp2
-                      #:construct val-exp))
+(define-syntax-parse-rule (intern-double-ref! table:id
+                                              key-exp1:expr
+                                              key-exp2:expr
+                                              #:construct val-exp:expr)
+  (intern-single-ref! (hash-ref! table key-exp1 make-hash) key-exp2 #:construct val-exp))
 
 
 
@@ -398,7 +394,7 @@
      ;; singletons cannot have fields or #:no-provide
      (when (and (attribute singleton)
                 (or (attribute no-provide?-kw)
-                    (> (length (syntax->list #'flds)) 0)))
+                    (positive? (length (syntax->list #'flds)))))
        (raise-syntax-error 'def-rep "singletons cannot have fields or the #:no-provide option"
                            #'var))
      (when (and (attribute base?)
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 1cb38e9ae..3e8f1ae0a 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -1161,8 +1161,8 @@
           (match ts
             [(list) (-refine Univ prop)]
             [(list t) (-refine t prop)]
-            [_ (let ([t (make-Intersection ts -tt elems)])
-                 (-refine t prop))])]
+            [_ (define t (make-Intersection ts -tt elems))
+               (-refine t prop)])]
          [(cons arg args)
           (match arg
             [(Univ:) (loop ts elems prop args)]
@@ -1813,7 +1813,7 @@
 
 ;; sorts the given field of a Row by the member name
 (define (sort-row-clauses clauses)
-  (sort clauses (λ (x y) (symbol<? (car x) (car y)))))
+  (sort clauses symbol<? #:key car))
 
 (define-match-expander Class:*
   (λ (stx)
diff --git a/typed-racket-lib/typed-racket/typecheck/error-message.rkt b/typed-racket-lib/typed-racket/typecheck/error-message.rkt
index fd909f39f..165d672f0 100644
--- a/typed-racket-lib/typed-racket/typecheck/error-message.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/error-message.rkt
@@ -80,9 +80,9 @@
   (unless object?
     (when (and (F? row) (not (F? row*)))
       (type-mismatch (format "Class with row variable `~a'" row)
-                     (format "Class with no row variable")))
+                     "Class with no row variable"))
     (when (and (F? row*) (not (F? row)))
-      (type-mismatch (format "Class with no row variable")
+      (type-mismatch "Class with no row variable"
                      (format "Class with row variable `~a'" row*)))
     (when (and (F? row) (F? row) (not (equal? row row*)))
       (type-mismatch (format "Class with row variable `~a'" row)
diff --git a/typed-racket-lib/typed-racket/typecheck/renamer.rkt b/typed-racket-lib/typed-racket/typecheck/renamer.rkt
index e38625ffe..90837be87 100644
--- a/typed-racket-lib/typed-racket/typecheck/renamer.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/renamer.rkt
@@ -43,9 +43,8 @@
 ;;
 ;; The syntax-transforming check is for unit tests
 (define (un-rename id)
-  (if (syntax-transforming?)
-      (let-values (((binding new-id) (syntax-local-value/immediate id (lambda () (values #f #f)))))
-        (if (typed-renaming? binding)
-            new-id
-            id))
-      id))
+  (cond
+    [(syntax-transforming?)
+     (define-values (binding new-id) (syntax-local-value/immediate id (lambda () (values #f #f))))
+     (if (typed-renaming? binding) new-id id)]
+    [else id]))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
index e440fab57..ff780b7ca 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
@@ -42,17 +42,17 @@
     [else
      (define-values (props atoms^) (combine-props ps (env-props env)))
 
-     (define atoms (if atoms^
+     (define atoms (and atoms^
                         ;; fix the order of paths to the same object.
                         ;; move objects with fewer path elements forward.
-                        (sort atoms^ (lambda (x y)
-                                       (match* (x y)
-                                         [((TypeProp: (Path: pes1 (? identifier? var1)) _)
-                                           (TypeProp: (Path: pes2 (? identifier? var2)) _))
-                                          #:when (equal? var1 var2)
-                                          (and (< (length pes1) (length pes2)))]
-                                         [(_ _) #f])))
-                        atoms^))
+                        (sort atoms^
+                              (lambda (x y)
+                                (match* (x y)
+                                  [((TypeProp: (Path: pes1 (? identifier? var1)) _)
+                                    (TypeProp: (Path: pes2 (? identifier? var2)) _))
+                                   #:when (equal? var1 var2)
+                                   (and (< (length pes1) (length pes2)))]
+                                  [(_ _) #f])))))
      (cond
        [props
         (let loop ([todo atoms]
@@ -82,35 +82,36 @@
                           (env-set-obj-type Γ obj new-t*))])))
              (match p
                [(TypeProp: (and obj (Path: pes (? identifier? x))) pt)
-                (let ([t (lookup-id-type/lexical x Γ #:fail (λ (_) Univ))])
-                  (define new-t (update t pt #t pes))
-                  (cond
-                    [(Bottom? new-t) #f]
-                    [(equal? t new-t)
-                     (cond
-                       [(ormap uninterpreted-PE? pes)
-                        (update-obj-pos-type new Γ obj pt)]
-                       [else (loop ps (cons p atoms) negs new Γ)])]
-                    [else
-                     ;; it's a new type! check if there are any logical propositions that can
-                     ;; be extracted from new-t
-                     (define-values (new-t* new-props) (extract-props (-id-path x) new-t))
-                     (cond
-                       ;; if the path contains an uninterpreted path element,
-                       ;; we need to update the object's type in addition to
-                       ;; the identifier's type
-                       [(ormap uninterpreted-PE? pes)
-                        (update-obj-pos-type (append new-props new)
-                                             (env-set-id-type Γ x new-t*)
-                                             obj
-                                             pt)]
-                       [(path-type pes new-t*) => (lambda (pt)
-                                                    (loop ps
-                                                          (cons (-is-type obj pt) atoms)
-                                                          negs
-                                                          (append new-props new)
-                                                          (env-set-id-type Γ x new-t*)))]
-                       [else #f])]))]
+                (define t (lookup-id-type/lexical x Γ #:fail (λ (_) Univ)))
+                (define new-t (update t pt #t pes))
+                (cond
+                  [(Bottom? new-t) #f]
+                  [(equal? t new-t)
+                   (cond
+                     [(ormap uninterpreted-PE? pes) (update-obj-pos-type new Γ obj pt)]
+                     [else (loop ps (cons p atoms) negs new Γ)])]
+                  [else
+                   ;; it's a new type! check if there are any logical propositions that can
+                   ;; be extracted from new-t
+                   (define-values (new-t* new-props) (extract-props (-id-path x) new-t))
+                   (cond
+                     ;; if the path contains an uninterpreted path element,
+                     ;; we need to update the object's type in addition to
+                     ;; the identifier's type
+                     [(ormap uninterpreted-PE? pes)
+                      (update-obj-pos-type (append new-props new)
+                                           (env-set-id-type Γ x new-t*)
+                                           obj
+                                           pt)]
+                     [(path-type pes new-t*)
+                      =>
+                      (lambda (pt)
+                        (loop ps
+                              (cons (-is-type obj pt) atoms)
+                              negs
+                              (append new-props new)
+                              (env-set-id-type Γ x new-t*)))]
+                     [else #f])])]
                [(TypeProp: obj pt)
                 (update-obj-pos-type new Γ obj pt)]
                ;; process negative info _after_ positive info so we don't miss anything!
@@ -145,33 +146,32 @@
                                  (env-set-obj-type Γ obj new-t*))])))
                     (match p
                       [(NotTypeProp: (and obj (Path: pes (? identifier? x))) pt)
-                       (let ([t (lookup-id-type/lexical x Γ #:fail (λ (_) Univ))])
-                         (define new-t (update t pt #f pes))
-                         (cond
-                           [(Bottom? new-t) #f]
-                           [(equal? t new-t)
-                            (cond
-                              [(ormap uninterpreted-PE? pes)
-                               (update-obj-neg-type new Γ obj pt)]
-                              [else (loop negs (cons p atoms) new Γ)])]
-                           [else
-                            ;; it's a new type! check if there are any logical propositions that can
-                            ;; be extracted from new-t
-                            (define-values (new-t* new-props) (extract-props (-id-path x) new-t))
-                            (cond
-                              ;; if the path contains an uninterpreted path element,
-                              ;; we need to update the object's type in addition to
-                              ;; the identifier's type
-                              [(ormap uninterpreted-PE? pes)
-                               (update-obj-neg-type (append new-props new)
-                                                    (env-set-id-type Γ x new-t*)
-                                                    obj
-                                                    pt)]
-                              [else
-                               (loop negs
-                                     (cons p atoms)
-                                     (append new-props new)
-                                     (env-set-id-type Γ x new-t*))])]))]
+                       (define t (lookup-id-type/lexical x Γ #:fail (λ (_) Univ)))
+                       (define new-t (update t pt #f pes))
+                       (cond
+                         [(Bottom? new-t) #f]
+                         [(equal? t new-t)
+                          (cond
+                            [(ormap uninterpreted-PE? pes) (update-obj-neg-type new Γ obj pt)]
+                            [else (loop negs (cons p atoms) new Γ)])]
+                         [else
+                          ;; it's a new type! check if there are any logical propositions that can
+                          ;; be extracted from new-t
+                          (define-values (new-t* new-props) (extract-props (-id-path x) new-t))
+                          (cond
+                            ;; if the path contains an uninterpreted path element,
+                            ;; we need to update the object's type in addition to
+                            ;; the identifier's type
+                            [(ormap uninterpreted-PE? pes)
+                             (update-obj-neg-type (append new-props new)
+                                                  (env-set-id-type Γ x new-t*)
+                                                  obj
+                                                  pt)]
+                            [else
+                             (loop negs
+                                   (cons p atoms)
+                                   (append new-props new)
+                                   (env-set-id-type Γ x new-t*))])])]
                       [(NotTypeProp: obj pt)
                        (update-obj-neg-type new Γ obj pt)])]
                    [_
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
index 7f237be3b..cb4c15bcb 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
@@ -134,24 +134,30 @@
        (cond
          ;; find the first function where the argument types match
          [(ormap (match-lambda
-                   [(and a (Arrow: dom rst _ _))
-                    (and (subtypes/varargs argtys dom rst) a)])
+                   [(and a (Arrow: dom rst _ _)) (and (subtypes/varargs argtys dom rst) a)])
                  arrows)
-          => (λ (a)
-               ;; then typecheck here -- we call the separate function so that we get
-               ;; the appropriate props/objects
-               (tc/funapp1 f-stx args-stx a args-res expected #:check #f))]
+          =>
+          (λ (a)
+            ;; then typecheck here -- we call the separate function so that we get
+            ;; the appropriate props/objects
+            (tc/funapp1 f-stx args-stx a args-res expected #:check #f))]
          [else
           ;; if nothing matched, error
-          (match arrows
-            [(list (Arrow: doms rsts _ rngs) ...)
-             (domain-mismatches
-              f-stx args-stx f-type doms rsts rngs args-res #f #f
-              #:expected expected
-              #:msg-thunk (lambda (dom)
-                            (string-append
-                             "No function domains matched in function application:\n"
-                             dom)))])])]
+          (match-define (list (Arrow: doms rsts _ rngs) ...) arrows)
+          (domain-mismatches f-stx
+                             args-stx
+                             f-type
+                             doms
+                             rsts
+                             rngs
+                             args-res
+                             #f
+                             #f
+                             #:expected expected
+                             #:msg-thunk
+                             (lambda (dom)
+                               (string-append "No function domains matched in function application:\n"
+                                              dom)))])]
       ;; any kind of dotted polymorphic function without mandatory keyword args
       [(PolyDots: (list fixed-vars ... dotted-var)
                   (Fun: arrows))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
index 36f666762..6af500811 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
@@ -336,7 +336,7 @@
       [_ #f]))
 
   (cond
-    [(and (> (free-id-table-count aux-table) 0) (not rest-id))
+    [(and (positive? (free-id-table-count aux-table)) (not rest-id))
      (tc/opt-lambda-clause arg-list body aux-table)]
     [else
      (define arg-types (get-types arg-list #:default (lambda () #f)))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
index 6720c4d93..013763f7c 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
@@ -259,8 +259,8 @@
            (λ ()
              (for ([expr (in-list remaining-exprs)]
                    [results (in-list given-rhs-types)])
-               (match results
-                 [(list (tc-result: ts fs os) ...) (tc-expr/check expr (ret ts fs os))]))
+               (match-define (list (tc-result: ts fs os) ...) results)
+               (tc-expr/check expr (ret ts fs os)))
              (check-thunk)))])))))
 
 ;; An lr-clause is a
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index ad7b816a8..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]
@@ -462,9 +462,8 @@
   (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)
@@ -512,28 +511,29 @@
        (match ty
          [(Fun: (list arrs ...))
           (make-Fun
-           (map (lambda (arr)
-                  (Arrow-update
-                   arr
-                   dom
-                   (lambda (doms)
-                     (match (car doms)
-                       [(Name/simple: n)
-                        #:when (free-identifier=? n st-name)
-                        (void)]
-                       [(App: (Name/simple: rator) vars)
-                        #:when (free-identifier=? rator st-name)
-                        (void)]
-                       [(Univ:)
-                        (void)]
-                       [(or (Name/simple: (app syntax-e n)) n)
-                        (tc-error/fields "type mismatch in the first parameter of the function for prop:procedure"
-                                         "expected" (syntax-e st-name)
-                                         "got" n
-                                         #:stx (st-proc-ty-property #'ty-stx))])
-
-                     (cdr doms))))
-                arrs))]
+           (for/list ([arr (in-list arrs)])
+             (Arrow-update
+              arr
+              dom
+              (lambda (doms)
+                (match (car doms)
+                  [(Name/simple: n)
+                   #:when (free-identifier=? n st-name)
+                   (void)]
+                  [(App: (Name/simple: rator) vars)
+                   #:when (free-identifier=? rator st-name)
+                   (void)]
+                  [(Univ:) (void)]
+                  [(or (Name/simple: (app syntax-e n)) n)
+                   (tc-error/fields
+                    "type mismatch in the first parameter of the function for prop:procedure"
+                    "expected"
+                    (syntax-e st-name)
+                    "got"
+                    n
+                    #:stx (st-proc-ty-property #'ty-stx))])
+           
+                (cdr doms)))))]
          [_
           (tc-error/fields "type mismatch"
                            "expected"
diff --git a/typed-racket-lib/typed-racket/types/printer.rkt b/typed-racket-lib/typed-racket/types/printer.rkt
index aa517c73e..42b5ab46f 100644
--- a/typed-racket-lib/typed-racket/types/printer.rkt
+++ b/typed-racket-lib/typed-racket/types/printer.rkt
@@ -341,10 +341,10 @@
                     [max-cover (covers-how-many? (car candidates))]
                     #:result next)
                    ([c (in-list candidates)])
-           (let ([how-many? (covers-how-many? c)])
-             (if (> how-many? max-cover)
-                 (values c how-many?)
-                 (values next max-cover)))))
+           (define how-many? (covers-how-many? c))
+           (if (> how-many? max-cover)
+               (values c how-many?)
+               (values next max-cover))))
        (loop (set-subtract to-cover (cdr next)) (remove next candidates) (cons next coverage))])))
 
 ;; arr->sexp : arr -> s-expression