diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/rep-utils.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/rep-utils.rkt
index 69ac9a4977..2411522289 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/rep-utils.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/rep-utils.rkt
@@ -7,6 +7,7 @@
          "interning.rkt"
          racket/lazy-require
          racket/stxparam
+         racket/unsafe/ops
          (for-syntax
           racket/match
           (except-in syntax/parse id identifier keyword)
@@ -353,6 +354,11 @@
                 [Object def-object #:Object object-case print-object object-name-ht object-rec-id]
                 [PathElem def-pathelem #:PathElem pathelem-case print-pathelem pathelem-name-ht pathelem-rec-id])
 
+;; NOTE: change these if the definitions above change, or everything will segfault
+(define-syntax-rule (unsafe-Rep-seq v) (unsafe-struct*-ref v 0))
+(define-syntax-rule (unsafe-Type-key v) (unsafe-struct*-ref v 1))
+(provide unsafe-Rep-seq unsafe-Type-key)
+
 (define (Rep-values rep)
   (match rep
     [(? (lambda (e) (or (Filter? e)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 1322902a23..a0914621ae 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -8,7 +8,7 @@
 ;; TODO use contract-req
 (require (utils tc-utils)
          "rep-utils.rkt" "object-rep.rkt" "filter-rep.rkt" "free-variance.rkt"
-         racket/match
+         racket/match racket/list
          racket/contract
          racket/lazy-require
          (for-syntax racket/base syntax/parse))
@@ -100,11 +100,13 @@
 
 ;; free type variables
 ;; n is a Name
-(def-type F ([n symbol?]) [#:frees (single-free-var n) empty-free-vars] [#:fold-rhs #:base])
+(def-type F ([n symbol?]) [#:frees (single-free-var n) empty-free-vars]
+  [#:fold-rhs #:base])
 
 ;; id is an Identifier
 ;; This will always resolve to a struct
-(def-type Name ([id identifier?]) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base])
+(def-type Name ([id identifier?]) [#:intern (hash-id id)] [#:frees #f]
+  [#:fold-rhs #:base])
 
 ;; rator is a type
 ;; rands is a list of types
@@ -180,7 +182,7 @@
 
 ;; elem is a Type
 (def-type Set ([elem Type/c])
-  [#:key 'set])
+  [#:key #f])
 
 ;; result is a Type
 (def-type Evt ([result Type/c])
@@ -197,7 +199,6 @@
   [#:key (if numeric?
              'number
              (case name
-               [(Number Integer) 'number]
                [(Boolean) 'boolean]
                [(String) 'string]
                [(Symbol) 'symbol]
@@ -375,10 +376,13 @@
   [#:fold-rhs #:base] [#:key 'continuation-mark-key])
 
 ;; v : Racket Value
-(def-type Value (v) [#:frees #f] [#:fold-rhs #:base] [#:key (cond [(number? v) 'number]
-                                                                  [(boolean? v) 'boolean]
-                                                                  [(null? v) 'null]
-                                                                  [else #f])])
+(def-type Value (v) [#:frees #f] [#:fold-rhs #:base]
+  [#:key (cond [(or (eq? v 0) (eq? v 1)) 'number]
+               ;; other numbers don't work with the optimizations in subtype.rkt
+               ;; which assume that unions of numbers are subtyped in simple ways
+               [(boolean? v) 'boolean]
+               [(null? v) 'null]
+               [else #f])])
 
 ;; elems : Listof[Type]
 (def-type Union ([elems (and/c (listof Type/c)
@@ -394,12 +398,18 @@
                                        sorted?))))])
   [#:frees (λ (f) (combine-frees (map f elems)))]
   [#:fold-rhs (apply Un (map type-rec-id elems))]
-  [#:key (let loop ([res null] [ts elems])
-           (if (null? ts) res
-               (let ([k (Type-key (car ts))])
-                 (cond [(pair? k) (loop (append k res) (cdr ts))]
-                       [k (loop (cons k res) (cdr ts))]
-                       [else #f]))))])
+  [#:key 
+   (let ()
+     (define d
+       (let loop ([ts elems] [res null])
+         (cond [(null? ts) res]
+               [else
+                (define k (Type-key (car ts)))
+                (cond [(not k) (list #f)]
+                      [(pair? k) (loop (cdr ts) (append k res))]
+                      [else (loop (cdr ts) (cons k res))])])))
+     (define d* (remove-duplicates d))
+     (if (and (pair? d*) (null? (cdr d*))) (car d*) d*))])
 
 (def-type Univ () [#:frees #f] [#:fold-rhs #:base])
 
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/current-seen.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/current-seen.rkt
index b68d01ca85..3cb86c0842 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/current-seen.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/current-seen.rkt
@@ -1,5 +1,5 @@
 #lang racket/base
-(require "../utils/utils.rkt")
+(require "../utils/utils.rkt" racket/unsafe/ops)
 (require (rep type-rep) (contract-req))
 
 (provide (except-out (all-defined-out) current-seen))
@@ -7,8 +7,16 @@
 
 (define current-seen (make-parameter null))
 (define (currently-subtyping?) (not (null? (current-seen))))
-
 (define (seen-before s t) (cons (Type-seq s) (Type-seq t)))
-(define (remember s t A) (cons (seen-before s t) A))
-(define (seen? s t) (member (seen-before s t) (current-seen)))
+
+(define (remember s t A) 
+  (if (or (Mu? s) (Mu? t)
+          (Name? s) (Name? t)
+          (Struct? s) (Struct? t) 
+          (App? s) (App? t))
+      (cons (seen-before s t) A)
+      A))
+(define (seen? ss st cs)
+  (for/or ([i (in-list cs)])
+    (and (eq? ss (unsafe-car i)) (eq? st (unsafe-cdr i)))))
 
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
index 2b2b716f73..f90c2300ef 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
@@ -1,6 +1,7 @@
 #lang racket/base
 (require (except-in "../utils/utils.rkt" infer)
          racket/match racket/function racket/lazy-require racket/list
+         racket/unsafe/ops
          (prefix-in c: (contract-req))
          (rep type-rep filter-rep object-rep rep-utils)
          (utils tc-utils)
@@ -13,12 +14,6 @@
   ("../infer/infer.rkt" (infer)))
 
 (define subtype-cache (make-hash))
-(define (cache-types s t)
-  (cache-keys (Type-seq s) (Type-seq t)))
-(define (cache-keys ks kt)
-  (hash-set! subtype-cache (cons ks kt) #t))
-(define (cached? s t)
-  (hash-ref subtype-cache (cons (Type-seq s) (Type-seq t)) #f))
 
 (define-syntax-rule (handle-failure e)
   e)
@@ -27,10 +22,7 @@
 ;; type type -> boolean
 (define/cond-contract (subtype s t)
   (c:-> (c:or/c Type/c SomeValues/c) (c:or/c Type/c SomeValues/c) boolean?)
-  (define k (cons (Type-seq s) (Type-seq t)))
-  ((if (currently-subtyping?) hash-ref hash-ref!)
-   subtype-cache k 
-   (lambda () (and (subtype* (current-seen) s t) #t))))
+  (and (subtype* (current-seen) s t) #t))
 
 ;; are all the s's subtypes of all the t's?
 ;; [type] [type] -> boolean
@@ -221,366 +213,371 @@
 	       (subtype* s t)
 	       (subtype* t s)))
 
+(define-syntax (early-return stx)
+  (syntax-parse stx
+    [(_ e:expr ... #:return-when e0:expr e1:expr rest ...)
+     #'(let ()
+         e ...
+         (if e0 e1
+             (early-return rest ...)))]
+    [(_ e:expr ...) #'(let () e ...)]))
+
+
+(define bottom-key (Rep-seq -Bottom))
+(define top-key (Rep-seq Univ))
+
 ;; the algorithm for recursive types transcribed directly from TAPL, pg 305
-;; List[(cons Number Number)] type type -> List[(cons Number Number)]
-;; potentially raises exn:subtype, when the algorithm fails
-;; is s a subtype of t, taking into account constraints A
+;; List[(cons Number Number)] type type -> List[(cons Number Number)] or #f
+;; is s a subtype of t, taking into account previously seen pairs A
 (define/cond-contract (subtype* A s t)
-  (c:-> list? Type? Type? c:any/c)
-  (define =t (lambda (a b) (if (and (Rep? a) (Rep? b)) (type-equal? a b) (equal? a b))))
-  (parameterize ([match-equality-test =t]
-                 [current-seen A])
-    (let ([ks (Type-key s)] [kt (Type-key t)])
-      (cond
-       [(or (seen? s t) (type-equal? s t)) A]
-       [(and (symbol? ks) (symbol? kt) (not (eq? ks kt))) #f]
-       [(and (symbol? ks) (pair? kt) (not (memq ks kt))) #f]
-       [(and (pair? ks) (pair? kt)
-             (for/and ([i (in-list ks)]) (not (memq i kt))))
-        #f]
-       [else
-        (let* ([A0 (remember s t A)])
-          (parameterize ([current-seen A0])
-            (match* (s t)
-              [(_ (Univ:)) A0]
-              [((or (ValuesDots: _ _ _) (Values: _) (AnyValues:)) (AnyValues:)) A0]
-              ;; error is top and bot
-              [(_ (Error:)) A0]
-              [((Error:) _) A0]
-              ;; (Un) is bot
-              [(_ (Union: (list))) #f]
-              [((Union: (list)) _) A0]
-              ;; value types
-              [((Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
-              ;; values are subtypes of their "type"
-              [((Value: v) (Base: _ _ pred _)) (if (pred v) A0 #f)]
-              ;; tvars are equal if they are the same variable
-              [((F: t) (F: t*)) (if (eq? t t*) A0 #f)]
-              ;; Avoid needing to resolve things that refer to different structs.
-              ;; Saves us from non-termination
-              ;; Must happen *before* the sequence cases, which sometimes call `resolve' in match expanders
-              [((or (? Struct? s1) (NameStruct: s1)) (or (? Struct? s2) (NameStruct: s2)))
-               (=> unmatch)
-               (cond [(unrelated-structs s1 s2)
-                      ;(dprintf "found unrelated structs: ~a ~a\n" s1 s2)
-                      #f]
-                     [else (unmatch)])]
-              ;; similar case for structs and base types, which are obviously unrelated
-              [((Base: _ _ _ _) (or (? Struct? s1) (NameStruct: s1)))
-               #f]
-              [((or (? Struct? s1) (NameStruct: s1)) (Base: _ _ _ _))
-               #f]
-              ;; same for all values.
-              [((Value: (? (negate struct?) _)) (or (? Struct? s1) (NameStruct: s1)))
-               #f]
-              [((or (? Struct? s1) (NameStruct: s1)) (Value: (? (negate struct?) _)))
-               #f]
-              ;; just checking if s/t is a struct misses recursive/union/etc cases
-              [((? (lambda (_) (eq? ks 'struct))) (Base: _ _ _ _)) #f]
-              [((Base: _ _ _ _) (? (lambda (_) (eq? kt 'struct)))) #f]
-              ;; sequences are covariant
-              [((Sequence: ts) (Sequence: ts*))
-               (subtypes* A0 ts ts*)]
-              [((Listof: t) (Sequence: (list t*)))
-               (subtype* A0 t t*)]
-              [((Pair: t1 t2) (Sequence: (list t*)))
-               (subtype-seq A0 (subtype* t1 t*) (subtype* t2 (-lst t*)))]
-              [((MListof: t) (Sequence: (list t*)))
-               (subtype* A0 t t*)]
-              ;; To check that mutable pair is a sequence we check that the cdr
-              ;; is both an mutable list and a sequence
-              [((MPair: t1 t2) (Sequence: (list t*)))
-               (subtype-seq A0
-                            (subtype* t1 t*)
-                            (subtype* t2 (simple-Un (-val null) (make-MPairTop)))
-                            (subtype* t2 t))]
-              [((List: ts) (Sequence: (list t*)))
-               (subtypes* A0 ts (map (λ (_) t*) ts))]
-              [((HeterogeneousVector: ts) (Sequence: (list t*)))
-               (subtypes* A0 ts (map (λ (_) t*) ts))]
-              [((Vector: t) (Sequence: (list t*)))
-               (subtype* A0 t t*)]
-              [((Base: 'String _ _ _) (Sequence: (list t*)))
-               (subtype* A0 -Char t*)]
-              [((Base: 'Bytes _ _ _) (Sequence: (list t*)))
-               (subtype* A0 -Byte t*)]
-              [((Base: 'Input-Port _ _ _) (Sequence: (list t*)))
-               (subtype* A0 -Nat t*)]
-              [((Value: (? exact-nonnegative-integer? n)) (Sequence: (list t*)))
-               (define possibilities
-                 (list
-                   (list byte? -Byte)
-                   (list portable-index? -Index)
-                   (list portable-fixnum? -NonNegFixnum)
-                   (list values -Nat)))
-               (define type
-                 (for/or ((pred-type (in-list possibilities)))
-                   (match pred-type
-                     ((list pred? type)
-                      (and (pred? n) type)))))
-               (subtype* A0 type t*)]
-              [((Base: _ _ _ #t) (Sequence: (list t*)))
-               (define type
-                 ;; FIXME: thread the store through here
-                 (for/or ((t (in-list (list -Byte -Index -NonNegFixnum -Nat))))
-                   (or (and (subtype* A0 s t) t))))
-               (if type
-                   (subtype* A0 type t*)
-                   #f)]
-              [((Hashtable: k v) (Sequence: (list k* v*)))
-               (subtypes* A0 (list k v) (list k* v*))]
-              [((Set: t) (Sequence: (list t*)))
-               (subtype* A0 t t*)]
-              ;; special-case for case-lambda/union with only one argument              
-              [((Function: arr1) (Function: (list arr2)))
-               (cond [(null? arr1) #f]
-                     [else
-                      (define comb (combine-arrs arr1))
-                      (or (and comb (arr-subtype*/no-fail A0 comb arr2))
-                          (supertype-of-one/arr A0 arr2 arr1))])]
-              ;; case-lambda
-              [((Function: arr1) (Function: arr2))
-               (when (null? arr1) #f)
-               (let loop-arities ([A* A0]
-                                  [arr2 arr2])
-                 (cond
+  (c:-> (listof (cons/c fixnum? fixnum?)) Type? Type? c:any/c)
+  (define ss (unsafe-Rep-seq s))
+  (define st (unsafe-Rep-seq t))
+  (early-return
+   #:return-when (or (eq? ss st) (seen? ss st A)) A
+   (define cr (hash-ref subtype-cache (cons ss st) 'missing))
+   #:return-when (boolean? cr) (and cr A)
+   (define ks (unsafe-Type-key s))
+   (define kt (unsafe-Type-key t))
+   #:return-when (and (symbol? ks) (symbol? kt) (not (eq? ks kt))) #f
+   #:return-when (and (symbol? ks) (pair? kt) (not (memq ks kt))) #f
+   #:return-when 
+   (and (pair? ks) (pair? kt)
+        (for/and ([i (in-list ks)]) (not (memq i kt))))
+   #f
+   #:return-when (eq? ss bottom-key) A
+   #:return-when (eq? st top-key) A
+   (define A0 (remember s t A))
+   (define r
+     ;; FIXME -- make this go into only the places that need it -- slows down new-metrics.rkt significantly
+     (parameterize ([current-seen A0]) 
+       (match* (s t)
+         ;; these cases are above as special cases
+         ;; [((Union: (list)) _) A0] ;; this is extremely common, so it goes first
+         ;; [(_ (Univ:)) A0]
+         [((or (ValuesDots: _ _ _) (Values: _) (AnyValues:)) (AnyValues:)) A0]
+         ;; error is top and bot
+         [(_ (Error:)) A0]
+         [((Error:) _) A0]
+         ;; (Un) is bot
+         [(_ (Union: (list))) #f]
+         ;; value types
+         [((Value: v1) (Value: v2))
+          #:when (equal? v1 v2) A0]
+         ;; values are subtypes of their "type"
+         [((Value: v) (Base: _ _ pred _)) (if (pred v) A0 #f)]
+         ;; tvars are equal if they are the same variable
+         [((F: t) (F: t*)) (if (eq? t t*) A0 #f)]
+         ;; Avoid needing to resolve things that refer to different structs.
+         ;; Saves us from non-termination
+         ;; Must happen *before* the sequence cases, which sometimes call `resolve' in match expanders
+         [((or (? Struct? s1) (NameStruct: s1)) (or (? Struct? s2) (NameStruct: s2)))
+          #:when (unrelated-structs s1 s2)
+          #f]
+         ;; similar case for structs and base types, which are obviously unrelated
+         [((Base: _ _ _ _) (or (? Struct? s1) (NameStruct: s1)))
+          #f]
+         [((or (? Struct? s1) (NameStruct: s1)) (Base: _ _ _ _))
+          #f]
+         ;; same for all values.
+         [((Value: (? (negate struct?) _)) (or (? Struct? s1) (NameStruct: s1)))
+          #f]
+         [((or (? Struct? s1) (NameStruct: s1)) (Value: (? (negate struct?) _)))
+          #f]
+         ;; sequences are covariant
+         [((Sequence: ts) (Sequence: ts*))
+          (subtypes* A0 ts ts*)]
+         [((Listof: t) (Sequence: (list t*)))
+          (subtype* A0 t t*)]
+         [((Pair: t1 t2) (Sequence: (list t*)))
+          (subtype-seq A0 (subtype* t1 t*) (subtype* t2 (-lst t*)))]
+         [((MListof: t) (Sequence: (list t*)))
+          (subtype* A0 t t*)]
+         ;; To check that mutable pair is a sequence we check that the cdr
+         ;; is both an mutable list and a sequence
+         [((MPair: t1 t2) (Sequence: (list t*)))
+          (subtype-seq A0
+                       (subtype* t1 t*)
+                       (subtype* t2 (simple-Un (-val null) (make-MPairTop)))
+                       (subtype* t2 t))]
+         [((List: ts) (Sequence: (list t*)))
+          (subtypes* A0 ts (map (λ (_) t*) ts))]
+         [((HeterogeneousVector: ts) (Sequence: (list t*)))
+          (subtypes* A0 ts (map (λ (_) t*) ts))]
+         [((Vector: t) (Sequence: (list t*)))
+          (subtype* A0 t t*)]
+         [((Base: 'String _ _ _) (Sequence: (list t*)))
+          (subtype* A0 -Char t*)]
+         [((Base: 'Bytes _ _ _) (Sequence: (list t*)))
+          (subtype* A0 -Byte t*)]
+         [((Base: 'Input-Port _ _ _) (Sequence: (list t*)))
+          (subtype* A0 -Nat t*)]
+         [((Value: (? exact-nonnegative-integer? n)) (Sequence: (list t*)))
+          (define possibilities
+            (list
+             (list byte? -Byte)
+             (list portable-index? -Index)
+             (list portable-fixnum? -NonNegFixnum)
+             (list values -Nat)))
+          (define type
+            (for/or ((pred-type (in-list possibilities)))
+              (match pred-type
+                ((list pred? type)
+                 (and (pred? n) type)))))
+          (subtype* A0 type t*)]
+         [((Base: _ _ _ #t) (Sequence: (list t*)))
+          (define type
+            ;; FIXME: thread the store through here
+            (for/or ((t (in-list (list -Byte -Index -NonNegFixnum -Nat))))
+              (or (and (subtype* A0 s t) t))))
+          (if type
+              (subtype* A0 type t*)
+              #f)]
+         [((Hashtable: k v) (Sequence: (list k* v*)))
+          (subtypes* A0 (list k v) (list k* v*))]
+         [((Set: t) (Sequence: (list t*)))
+          (subtype* A0 t t*)]
+         ;; special-case for case-lambda/union with only one argument              
+         [((Function: arr1) (Function: (list arr2)))
+          (cond [(null? arr1) #f]
+                [else
+                 (define comb (combine-arrs arr1))
+                 (or (and comb (arr-subtype*/no-fail A0 comb arr2))
+                     (supertype-of-one/arr A0 arr2 arr1))])]
+         ;; case-lambda
+         [((Function: arr1) (Function: arr2))
+          (if (null? arr1) #f
+              (let loop-arities ([A* A0]
+                                 [arr2 arr2])
+                (cond
                   [(null? arr2) A*]
                   [(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))]
-                  [else #f]))]
-              ;; recur structurally on pairs
-              [((Pair: a d) (Pair: a* d*))
-               (subtypes* A0 (list a d) (list a* d*))]
-              ;; recur structurally on dotted lists, assuming same bounds
-              [((ListDots: s-dty dbound) (ListDots: t-dty dbound))
-               (subtype* A0 s-dty t-dty)]
-              ;; For dotted lists and regular lists, we check that (All (dbound) s-dty) is a subtype
-              ;; of t-elem, so that no matter what dbound is instatiated with s-dty is still a subtype
-              ;; of t-elem. We cannot just replace dbound with Univ because of variance issues.
-              [((ListDots: s-dty dbound) (Listof: t-elem))
-               (subtype* A0 (-poly (dbound) s-dty) t-elem)]
-              ;; quantification over two types preserves subtyping
-              [((Poly: ns b1) (Poly: ms b2))
-               (=> unmatch)
-               (unless (= (length ns) (length ms))
-                 (unmatch))
-               ;; substitute ns for ms in b2 to make it look like b1
-               (subtype* A0 b1 (subst-all (make-simple-substitution ms (map make-F ns)) b2))]
-              [((PolyDots: (list ns ... n-dotted) b1)
-                (PolyDots: (list ms ... m-dotted) b2))
-               (cond
-                 [(< (length ns) (length ms))
-                  (define-values (short-ms rest-ms) (split-at ms (length ns)))
-                  ;; substitute ms for ns in b1 to make it look like b2
-                  (define subst
-                    (hash-set (make-simple-substitution ns (map make-F short-ms))
-                              n-dotted (i-subst/dotted (map make-F rest-ms) (make-F m-dotted) m-dotted)))
-                  (subtype* A0 (subst-all subst b1) b2)]
-                 [else
-                  (define-values (short-ns rest-ns) (split-at ns (length ms)))
-                  ;; substitute ns for ms in b2 to make it look like b1
-                  (define subst
-                    (hash-set (make-simple-substitution ms (map make-F short-ns))
-                              m-dotted (i-subst/dotted (map make-F rest-ns) (make-F n-dotted) n-dotted)))
-                  (subtype* A0 b1 (subst-all subst b2))])]
-              [((PolyDots: (list ns ... n-dotted) b1)
-                (Poly: (list ms ...) b2))
-               (=> unmatch)
-               (unless (<= (length ns) (length ms))
-                 (unmatch))
-               ;; substitute ms for ns in b1 to make it look like b2
-               (define subst
-                 (hash-set (make-simple-substitution ns (map make-F (take ms (length ns))))
-                           n-dotted (i-subst (map make-F (drop ms (length ns))))))
-               (subtype* A0 (subst-all subst b1) b2)]
-              [((Refinement: par _) t)
-               (subtype* A0 par t)]
-              ;; use unification to see if we can use the polytype here
-              [((Poly: vs b) s)
-               (=> unmatch)
-               (if (infer vs null (list b) (list s) Univ) A0 (unmatch))]
-              [((PolyDots: (list vs ... vdotted) b) s)
-               (=> unmatch)
-               (if (infer vs (list vdotted) (list b) (list s) Univ)
-                   A0
-                   (unmatch))]
-              [(s (or (Poly: vs b) (PolyDots: vs b)))
-               (=> unmatch)
-               (if (null? (fv b)) (subtype* A0 s b) (unmatch))]
-              ;; rec types, applications and names (that aren't the same)
-              [((? needs-resolving? s) other)
-               (let ([s* (resolve-once s)])
-                 (if (Type/c? s*) ;; needed in case this was a name that hasn't been resolved yet
-                     (subtype* A0 s* other)
-                     #f))]
-              [(other (? needs-resolving? t))
-               (let ([t* (resolve-once t)])
-                 (if (Type/c? t*) ;; needed in case this was a name that hasn't been resolved yet
-                     (subtype* A0 other t*)
-                     #f))]
-              ;; for unions, we check the cross-product
-              ;; some special cases for better performance
-              ;; first, if both types are numeric, they will be built from the same base types
-              ;; so we can check for simple set inclusion of the union components
-              [((Base: _ _ _ _) (Union: l2))
-               (=> unmatch)
-               (if (and (eq? ks 'number) (eq? kt 'number))
-                   (if (memq s l2) A0 #f)
-                   (unmatch))]
-              [((Union: l1) (Union: l2))
-               (=> unmatch)
-               (if (and (eq? ks 'number) (eq? kt 'number))
-                   ;; l1 should be a subset of l2
-                   ;; since union elements are sorted, a linear scan works
-                   (let loop ([l1 l1] [l2 l2])
-                     (cond [(null? l1)
-                            A0]
-                           [(null? l2)
-                            #f]
-                           [(eq? (car l1) (car l2))
-                            (loop (cdr l1) (cdr l2))]
-                           [else
-                            (loop l1 (cdr l2))]))
-                   (unmatch))]
-              [((Union: (list e1 e2)) t)
-               (and (and (subtype* A0 e1 t) (subtype* A0 e2 t))
-                    A0)]
-              [((Union: (list e1 e2 e3)) t)
-               (and (and (subtype* A0 e1 t) (subtype* A0 e2 t) (subtype* A0 e3 t))
-                    A0)]
-              [((Union: es) t)
-               (and (for/and ([elem (in-list es)])
-                     (subtype* A0 elem t))
-                    A0)]
-              [(s (Union: es))
-               (and (for/or ([elem (in-list es)])
-                       (subtype* A0 s elem))
-                    A0)]
-              ;; subtyping on immutable structs is covariant
-              [((Struct: nm _ flds proc _ _) (Struct: nm* _ flds* proc* _ _))
-	       (=> unmatch)
-               (unless (free-identifier=? nm nm*) (unmatch))
-               (let ([A (cond [(and proc proc*) (subtype* A0 proc proc*)]
-                              [proc* #f]
-                              [else A0])])
-		 (and A (subtype/flds* A flds flds*)))]
-              [((Struct: nm _ _ _ _ _) (StructTop: (Struct: nm* _ _ _ _ _)))
-	       (=> unmatch)
-               (unless (free-identifier=? nm nm*) (unmatch))
-               A0]
-              ;; Promises are covariant
-              [((Promise: s) (Promise: t))
-               (subtype* A0 s t)]
-              ;ephemerons are covariant
-              [((Ephemeron: s) (Ephemeron: t))
-               (subtype* A0 s t)]
-              [((CustodianBox: s) (CustodianBox: t))
-               (subtype* A0 s t)]
-              [((Set: t) (Set: t*)) (subtype* A0 t t*)]
-              ;; Evts are covariant
-              [((Evt: t) (Evt: t*)) (subtype* A0 t t*)]
-              [((Base: 'Semaphore _ _ _) (Evt: t))
-               (subtype* A0 s t)]
-              [((Base: 'Output-Port _ _ _) (Evt: t))
-               (subtype* A0 s t)]
-              [((Base: 'Input-Port _ _ _) (Evt: t))
-               (subtype* A0 s t)]
-              [((Base: 'TCP-Listener _ _ _) (Evt: t))
-               (subtype* A0 s t)]
-              [((Base: 'Thread _ _ _) (Evt: t))
-               (subtype* A0 s t)]
-              [((Base: 'Subprocess _ _ _) (Evt: t))
-               (subtype* A0 s t)]
-              [((Base: 'Will-Executor _ _ _) (Evt: t))
-               (subtype* A0 s t)]
-              [((Base: 'LogReceiver _ _ _) (Evt: t))
-               (subtype* A0
-                         (make-HeterogeneousVector
-                          (list -Symbol -String Univ
-                                (Un (-val #f) -Symbol)))
-                         t)]
-              [((CustodianBox: t) (Evt: t*))
-               ;; Note that it's the whole box type that's being
-               ;; compared against t* here
-               (subtype* A0 s t*)]
-              [((Channel: t) (Evt: t*)) (subtype* A0 t t*)]
-              ;; Invariant types
-              [((Box: s) (Box: t)) (type-equiv? A0 s t)]
-              [((Box: _) (BoxTop:)) A0]
-              [((ThreadCell: s) (ThreadCell: t)) (type-equiv? A0 s t)]
-              [((ThreadCell: _) (ThreadCellTop:)) A0]
-              [((Channel: s) (Channel: t)) (type-equiv? A0 s t)]
-              [((Channel: _) (ChannelTop:)) A0]
-              [((Vector: s) (Vector: t)) (type-equiv? A0 s t)]
-              [((Vector: _) (VectorTop:)) A0]
-              [((HeterogeneousVector: _) (VectorTop:)) A0]
-              [((HeterogeneousVector: (list e ...)) (Vector: e*))
-               (for/fold ((A A0)) ((e (in-list e)) #:break (not A))
-                 (and A (type-equiv? A e e*)))]
-              [((HeterogeneousVector: (list s* ...)) (HeterogeneousVector: (list t* ...)))
-               (if (= (length s*) (length t*))
-                   (for/fold ((A A0)) ((s (in-list s*)) (t (in-list t*)) #:break (not A))
-                     (type-equiv? A s t))
-                   #f)]
-              [((MPair: s1 s2) (MPair: t1 t2))
-	       (subtype-seq A0
-			    (type-equiv? s1 t1)
-			    (type-equiv? s2 t2))]
-              [((MPair: _ _) (MPairTop:)) A0]
-              [((Hashtable: s1 s2) (Hashtable: t1 t2))
-	       (subtype-seq A0
-			    (type-equiv? s1 t1)
-			    (type-equiv? s2 t2))]
-              [((Hashtable: _ _) (HashtableTop:)) A0]
-              [((Prompt-Tagof: s1 s2) (Prompt-Tagof: t1 t2))
-	       (subtype-seq A0
-			    (type-equiv? s1 t1)
-			    (type-equiv? s2 t2))]
-              [((Prompt-Tagof: _ _) (Prompt-TagTop:)) A0]
-              [((Continuation-Mark-Keyof: s) (Continuation-Mark-Keyof: t))
-               (type-equiv? A0 s t)]
-              [((Continuation-Mark-Keyof: _) (Continuation-Mark-KeyTop:)) A0]
-              ;; subtyping on structs follows the declared hierarchy
-              [((Struct: nm (? Type/c? parent) _ _ _ _) other)
-               ;(dprintf "subtype - hierarchy : ~a ~a ~a\n" nm parent other)
-               (subtype* A0 parent other)]
-              ;; subtyping on values is pointwise
-              [((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
-              [((ValuesDots: s-rs s-dty dbound) (ValuesDots: t-rs t-dty dbound))
-               (subtype* (subtypes* A0 s-rs t-rs) s-dty t-dty)]
-              [((Result: t (FilterSet: ft ff) o) (Result: t* (FilterSet: ft* ff*) o))
-               (subtype-seq A0
-                 (subtype* t t*)
-                 (filter-subtype* ft ft*)
-                 (filter-subtype* ff ff*))]
-              [((Result: t (FilterSet: ft ff) o) (Result: t* (FilterSet: ft* ff*) (Empty:)))
-               (subtype-seq A0
-                 (subtype* t t*)
-                 (filter-subtype* ft ft*)
-                 (filter-subtype* ff ff*))]
-              ;; subtyping on other stuff
-              [((Syntax: t) (Syntax: t*))
-               (subtype* A0 t t*)]
-              [((Future: t) (Future: t*))
-               (subtype* A0 t t*)]
-              [((Param: s-in s-out) (Param: t-in t-out))
-	       (subtype-seq A0
-			    (subtype* t-in s-in)
-			    (subtype* s-out t-out))]
-              [((Param: in out) t)
-               (subtype* A0 (cl->* (-> out) (-> in -Void)) t)]
-              [((Instance: t) (Instance: t*))
-               (subtype* A0 t t*)]
-              [((Class: '() '() (list (and s  (list names  meths )) ...))
-                (Class: '() '() (list (and s* (list names* meths*)) ...)))
-               (for/fold ([A A0])
-                         ([n (in-list names*)] [m (in-list meths*)] #:break (not A))
-                         (and A (cond [(assq n s) => (lambda (spec) (subtype* A (cadr spec) m))]
-                                      [else #f])))]
-              ;; otherwise, not a subtype
-              [(_ _) #f #;(dprintf "failed")])))]))))
+                  [else #f])))]
+         ;; recur structurally on pairs
+         [((Pair: a d) (Pair: a* d*))
+          (subtypes* A0 (list a d) (list a* d*))]
+         ;; recur structurally on dotted lists, assuming same bounds
+         [((ListDots: s-dty dbound) (ListDots: t-dty dbound*))
+          (and (eq? dbound dbound*)
+               (subtype* A0 s-dty t-dty))]
+         ;; For dotted lists and regular lists, we check that (All (dbound) s-dty) is a subtype
+         ;; of t-elem, so that no matter what dbound is instatiated with s-dty is still a subtype
+         ;; of t-elem. We cannot just replace dbound with Univ because of variance issues.
+         [((ListDots: s-dty dbound) (Listof: t-elem))
+          (subtype* A0 (-poly (dbound) s-dty) t-elem)]
+         ;; quantification over two types preserves subtyping
+         [((Poly: ns b1) (Poly: ms b2))               
+          #:when (= (length ns) (length ms))
+          ;; substitute ns for ms in b2 to make it look like b1
+          (subtype* A0 b1 (subst-all (make-simple-substitution ms (map make-F ns)) b2))]
+         [((PolyDots: (list ns ... n-dotted) b1)
+           (PolyDots: (list ms ... m-dotted) b2))
+          (cond
+            [(< (length ns) (length ms))
+             (define-values (short-ms rest-ms) (split-at ms (length ns)))
+             ;; substitute ms for ns in b1 to make it look like b2
+             (define subst
+               (hash-set (make-simple-substitution ns (map make-F short-ms))
+                         n-dotted (i-subst/dotted (map make-F rest-ms) (make-F m-dotted) m-dotted)))
+             (subtype* A0 (subst-all subst b1) b2)]
+            [else
+             (define-values (short-ns rest-ns) (split-at ns (length ms)))
+             ;; substitute ns for ms in b2 to make it look like b1
+             (define subst
+               (hash-set (make-simple-substitution ms (map make-F short-ns))
+                         m-dotted (i-subst/dotted (map make-F rest-ns) (make-F n-dotted) n-dotted)))
+             (subtype* A0 b1 (subst-all subst b2))])]
+         [((PolyDots: (list ns ... n-dotted) b1)
+           (Poly: (list ms ...) b2))
+          #:when (<= (length ns) (length ms))
+          ;; substitute ms for ns in b1 to make it look like b2
+          (define subst
+            (hash-set (make-simple-substitution ns (map make-F (take ms (length ns))))
+                      n-dotted (i-subst (map make-F (drop ms (length ns))))))
+          (subtype* A0 (subst-all subst b1) b2)]
+         [((Refinement: par _) t)
+          (subtype* A0 par t)]
+         ;; use unification to see if we can use the polytype here
+         [((Poly: vs b) s)
+          #:when (infer vs null (list b) (list s) Univ)
+          A0]
+         [((PolyDots: (list vs ... vdotted) b) s)
+          #:when (infer vs (list vdotted) (list b) (list s) Univ)
+          A0]
+         [(s (or (Poly: vs b) (PolyDots: vs b)))
+          #:when (null? (fv b))
+          (subtype* A0 s b)]
+         ;; rec types, applications and names (that aren't the same)
+         [((? needs-resolving? s) other)
+          (let ([s* (resolve-once s)])
+            (if (Type/c? s*) ;; needed in case this was a name that hasn't been resolved yet
+                (subtype* A0 s* other)
+                #f))]
+         [(other (? needs-resolving? t))
+          (let ([t* (resolve-once t)])
+            (if (Type/c? t*) ;; needed in case this was a name that hasn't been resolved yet
+                (subtype* A0 other t*)
+                #f))]
+         ;; for unions, we check the cross-product
+         ;; some special cases for better performance
+         ;; first, if both types are numeric, they will be built from the same base types
+         ;; so we can check for simple set inclusion of the union components
+         [((Base: _ _ _ #t) (Union: l2))
+          #:when (eq? kt 'number)
+          (and (memq s l2) A0)]
+         ;; this appears to never be called
+         [((Union: l1) (Union: l2))
+          #:when (and (eq? ks 'number) (eq? kt 'number))
+          ;; l1 should be a subset of l2
+          ;; since union elements are sorted, a linear scan works
+          (let loop ([l1 l1] [l2 l2])
+            (cond [(null? l1)
+                   A0]
+                  [(null? l2)
+                   #f]
+                  [(eq? (car l1) (car l2))
+                   (loop (cdr l1) (cdr l2))]
+                  [else
+                   (loop l1 (cdr l2))]))]
+         [((Union: es) t)
+          ;(set! lengths (cons (length es) lengths))
+          (and 
+           (for/and ([elem (in-list es)])
+             (subtype* A0 elem t))
+           A0)]
+         [(s (Union: es))
+          ;(set! lengths (cons (length es) lengths))
+          (and (for/or ([elem (in-list es)])
+                 (subtype* A0 s elem))
+               A0)]
+         ;; subtyping on immutable structs is covariant
+         [((Struct: nm _ flds proc _ _) (Struct: nm* _ flds* proc* _ _)) 
+          #:when (free-identifier=? nm nm*) 
+          (let ([A (cond [(and proc proc*) (subtype* A0 proc proc*)]
+                         [proc* #f]
+                         [else A0])])
+            (and A (subtype/flds* A flds flds*)))]
+         [((Struct: nm _ _ _ _ _) (StructTop: (Struct: nm* _ _ _ _ _)))
+          #:when (free-identifier=? nm nm*)
+          A0]
+         ;; Promises are covariant
+         [((Promise: s) (Promise: t))
+          (subtype* A0 s t)]
+         ;ephemerons are covariant
+         [((Ephemeron: s) (Ephemeron: t))
+          (subtype* A0 s t)]
+         [((CustodianBox: s) (CustodianBox: t))
+          (subtype* A0 s t)]
+         [((Set: t) (Set: t*)) (subtype* A0 t t*)]
+         ;; Evts are covariant
+         [((Evt: t) (Evt: t*)) (subtype* A0 t t*)]
+         [((Base: 'Semaphore _ _ _) (Evt: t))
+          (subtype* A0 s t)]
+         [((Base: 'Output-Port _ _ _) (Evt: t))
+          (subtype* A0 s t)]
+         [((Base: 'Input-Port _ _ _) (Evt: t))
+          (subtype* A0 s t)]
+         [((Base: 'TCP-Listener _ _ _) (Evt: t))
+          (subtype* A0 s t)]
+         [((Base: 'Thread _ _ _) (Evt: t))
+          (subtype* A0 s t)]
+         [((Base: 'Subprocess _ _ _) (Evt: t))
+          (subtype* A0 s t)]
+         [((Base: 'Will-Executor _ _ _) (Evt: t))
+          (subtype* A0 s t)]
+         [((Base: 'LogReceiver _ _ _) (Evt: t))
+          (subtype* A0
+                    (make-HeterogeneousVector
+                     (list -Symbol -String Univ
+                           (Un (-val #f) -Symbol)))
+                    t)]
+         [((CustodianBox: t) (Evt: t*))
+          ;; Note that it's the whole box type that's being
+          ;; compared against t* here
+          (subtype* A0 s t*)]
+         [((Channel: t) (Evt: t*)) (subtype* A0 t t*)]
+         ;; Invariant types
+         [((Box: s) (Box: t)) (type-equiv? A0 s t)]
+         [((Box: _) (BoxTop:)) A0]
+         [((ThreadCell: s) (ThreadCell: t)) (type-equiv? A0 s t)]
+         [((ThreadCell: _) (ThreadCellTop:)) A0]
+         [((Channel: s) (Channel: t)) (type-equiv? A0 s t)]
+         [((Channel: _) (ChannelTop:)) A0]
+         [((Vector: s) (Vector: t)) (type-equiv? A0 s t)]
+         [((Vector: _) (VectorTop:)) A0]
+         [((HeterogeneousVector: _) (VectorTop:)) A0]
+         [((HeterogeneousVector: (list e ...)) (Vector: e*))
+          (for/fold ((A A0)) ((e (in-list e)) #:break (not A))
+            (and A (type-equiv? A e e*)))]
+         [((HeterogeneousVector: (list s* ...)) (HeterogeneousVector: (list t* ...)))
+          (if (= (length s*) (length t*))
+              (for/fold ((A A0)) ((s (in-list s*)) (t (in-list t*)) #:break (not A))
+                (type-equiv? A s t))
+              #f)]
+         [((MPair: s1 s2) (MPair: t1 t2))
+          (subtype-seq A0
+                       (type-equiv? s1 t1)
+                       (type-equiv? s2 t2))]
+         [((MPair: _ _) (MPairTop:)) A0]
+         [((Hashtable: s1 s2) (Hashtable: t1 t2))
+          (subtype-seq A0
+                       (type-equiv? s1 t1)
+                       (type-equiv? s2 t2))]
+         [((Hashtable: _ _) (HashtableTop:)) A0]
+         [((Prompt-Tagof: s1 s2) (Prompt-Tagof: t1 t2))
+          (subtype-seq A0
+                       (type-equiv? s1 t1)
+                       (type-equiv? s2 t2))]
+         [((Prompt-Tagof: _ _) (Prompt-TagTop:)) A0]
+         [((Continuation-Mark-Keyof: s) (Continuation-Mark-Keyof: t))
+          (type-equiv? A0 s t)]
+         [((Continuation-Mark-Keyof: _) (Continuation-Mark-KeyTop:)) A0]
+         ;; subtyping on structs follows the declared hierarchy
+         [((Struct: nm (? Type/c? parent) _ _ _ _) other)
+          ;(dprintf "subtype - hierarchy : ~a ~a ~a\n" nm parent other)
+          (subtype* A0 parent other)]
+         ;; subtyping on values is pointwise
+         [((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
+         [((ValuesDots: s-rs s-dty dbound) (ValuesDots: t-rs t-dty dbound))
+          (subtype* (subtypes* A0 s-rs t-rs) s-dty t-dty)]
+         [((Result: t (FilterSet: ft ff) o) (Result: t* (FilterSet: ft* ff*) o))
+          (subtype-seq A0
+                       (subtype* t t*)
+                       (filter-subtype* ft ft*)
+                       (filter-subtype* ff ff*))]
+         [((Result: t (FilterSet: ft ff) o) (Result: t* (FilterSet: ft* ff*) (Empty:)))
+          (subtype-seq A0
+                       (subtype* t t*)
+                       (filter-subtype* ft ft*)
+                       (filter-subtype* ff ff*))]
+         ;; subtyping on other stuff
+         [((Syntax: t) (Syntax: t*))
+          (subtype* A0 t t*)]
+         [((Future: t) (Future: t*))
+          (subtype* A0 t t*)]
+         [((Param: s-in s-out) (Param: t-in t-out))
+          (subtype-seq A0
+                       (subtype* t-in s-in)
+                       (subtype* s-out t-out))]
+         [((Param: in out) t)
+          (subtype* A0 (cl->* (-> out) (-> in -Void)) t)]
+         [((Instance: t) (Instance: t*))
+          (subtype* A0 t t*)]
+         [((Class: '() '() (list (and s  (list names  meths )) ...))
+           (Class: '() '() (list (and s* (list names* meths*)) ...)))
+          (for/fold ([A A0])
+            ([n (in-list names*)] [m (in-list meths*)] #:break (not A))
+            (and A (cond [(assq n s) => (lambda (spec) (subtype* A (cadr spec) m))]
+                         [else #f])))]
+         ;; otherwise, not a subtype
+         [(_ _) #f])))
+     (when (null? A)
+       (hash-set! subtype-cache (cons ss st) r))
+     r))
 
 (define (type-compare? a b)
-  (and (subtype a b) (subtype b a)))
+  (or (type-equal? a b)
+      (and (subtype a b) (subtype b a))))
 
 ;; List[(cons Number Number)] type type -> maybe[List[(cons Number Number)]]
 (define subtype*/no-fail subtype*)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/utils.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/utils.rkt
index 19f1463ee5..ae2d0f7700 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/utils.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/utils.rkt
@@ -165,7 +165,7 @@ at least theoretically.
       (lambda (stx)
         (syntax-parse stx
           [(_ head cnt . body)
-           #'(define head . body)]))))
+           (syntax/loc stx (define head . body))]))))
 
 (define-syntax define-struct/cond-contract
   (if enable-contracts?