diff --git a/typed-racket-lib/typed-racket/base-env/base-special-env.rkt b/typed-racket-lib/typed-racket/base-env/base-special-env.rkt
index 015c9676..073c1105 100644
--- a/typed-racket-lib/typed-racket/base-env/base-special-env.rkt
+++ b/typed-racket-lib/typed-racket/base-env/base-special-env.rkt
@@ -11,8 +11,7 @@
  (for-template (only-in racket/private/kw kw-expander-proc kw-expander-impl)
                racket/base racket/file racket/port racket/path racket/list)
  (env init-envs)
- (rename-in (types abbrev numeric-tower)
-            [make-arr* make-arr])
+ (types abbrev numeric-tower)
  (for-syntax racket/base syntax/parse
              (only-in racket/syntax syntax-local-eval)))
 (provide make-template-identifier)
diff --git a/typed-racket-lib/typed-racket/base-env/top-interaction.rkt b/typed-racket-lib/typed-racket/base-env/top-interaction.rkt
index a7580275..87218d76 100644
--- a/typed-racket-lib/typed-racket/base-env/top-interaction.rkt
+++ b/typed-racket-lib/typed-racket/base-env/top-interaction.rkt
@@ -95,7 +95,8 @@
          #,(pretty-format-rep
             (match type
               [(tc-result1: t f o) t]
-              [(tc-results: t) (-values t)]
+              [(tc-results: (list (tc-result: ts) ...) _)
+               (-values ts)]
               [(tc-any-results: f) (-AnyValues f)]))))
     "must be applied to exactly one argument")
 
@@ -110,20 +111,20 @@
        #`(display
           #,(pretty-format-rep
              (match type
-               [(tc-result1: (and t (Function: _)) f o) t]))))
+               [(tc-result1: (and t (? Fun?)) f o) t]))))
      "must be applied to at least one argument" )
 
   ;; given a function and a desired return type, fill in the blanks
   (define-repl-op :query-type/result-impl (_ op desired-type) #'op
     (λ (type)
       (match type
-        [(tc-result1: (and t (Function: _)) f o)
+        [(tc-result1: (and t (? Fun?)) f o)
          (let ([cleaned (cleanup-type t (parse-type #'desired-type) #f)])
            #`(display
               #,(match cleaned
-                  [(Function: '())
+                  [(Fun: '())
                    "Desired return type not in the given function's range.\n"]
-                  [(Function: arrs)
+                  [(Fun: _)
                    (pretty-format-rep cleaned)])))]
         [_ (error (format "~a: not a function" (syntax->datum #'op)))]))
     "must be applied to exactly two arguments"))
diff --git a/typed-racket-lib/typed-racket/env/init-envs.rkt b/typed-racket-lib/typed-racket/env/init-envs.rkt
index d3e17b97..51f77928 100644
--- a/typed-racket-lib/typed-racket/env/init-envs.rkt
+++ b/typed-racket-lib/typed-racket/env/init-envs.rkt
@@ -160,32 +160,42 @@
      `(make-Immutable-HashTable ,(type->sexp key) ,(type->sexp val))]
     [(Weak-HashTable: key val)
      `(make-Weak-HashTable ,(type->sexp key) ,(type->sexp val))]
-    [(Function: (list (arr: dom (Values: (list (Result: t
-                                                        (PropSet: (TrueProp:)
-                                                                  (TrueProp:))
-                                                        (Empty:))))
-                            #f #f '())))
+    [(Fun: (list (Arrow: dom #f '()
+                         (Values:
+                          (list
+                           (Result: t
+                                    (PropSet: (TrueProp:)
+                                              (TrueProp:))
+                                    (Empty:)))))))
      `(simple-> (list ,@(map type->sexp dom)) ,(type->sexp t))]
-    [(Function: (list (arr: dom (Values: (list (Result: t (PropSet: (TypeProp: pth ft)
-                                                                    (NotTypeProp: pth ft))
-                                                        (Empty:))))
-                            #f #f '())))
+    [(Fun: (list (Arrow: dom #f'()
+                         (Values:
+                          (list
+                           (Result: t
+                                    (PropSet:
+                                     (TypeProp: pth ft)
+                                     (NotTypeProp: pth ft))
+                                    (Empty:)))))))
      `(make-pred-ty (list ,@(map type->sexp dom))
                     ,(type->sexp t)
                     ,(type->sexp ft)
                     ,(object->sexp pth))]
-    [(Function: (list (arr: dom (Values: (list (Result: t (PropSet: (NotTypeProp: (Path: pth (cons 0 0))
-                                                                                  (== -False))
-                                                                    (TypeProp: (Path: pth (cons 0 0))
-                                                                               (== -False)))
-                                                        (Path: pth (cons 0 0)))))
-                            #f #f '())))
+    [(Fun: (list (Arrow: dom #f '()
+                         (Values:
+                          (list
+                           (Result: t
+                                    (PropSet:
+                                     (NotTypeProp: (Path: pth (cons 0 0))
+                                                   (== -False))
+                                     (TypeProp: (Path: pth (cons 0 0))
+                                                (== -False)))
+                                    (Path: pth (cons 0 0))))))))
      `(->acc (list ,@(map type->sexp dom))
              ,(type->sexp t)
              (list ,@(map path-elem->sexp pth)))]
-    [(Function: (? has-optional-args? arrs))
-     (match-define (arr: fdoms rng rest _ *kws) (first arrs))
-     (match-define (arr: ldoms _ _ _ _) (last arrs))
+    [(Fun: (? has-optional-args? arrs))
+     (match-define (Arrow: fdoms rest *kws rng) (first arrs))
+     (match-define (Arrow: ldoms _ _ _) (last arrs))
      (define opts (drop ldoms (length fdoms)))
      (define kws (map type->sexp *kws))
      `(opt-fn (list ,@(map type->sexp fdoms))
@@ -193,8 +203,7 @@
               ,(type->sexp rng)
               ,@(if rest `(#:rest ,rest) '())
               ,@(if (null? kws) '() `(#:kws (list ,@kws))))]
-    [(Function: arrs)
-     `(make-Function (list ,@(map type->sexp arrs)))]
+    [(Fun: arrs) `(make-Fun (list ,@(map type->sexp arrs)))]
     [(Keyword: kw ty required?)
      `(make-Keyword (quote ,kw) ,(type->sexp ty) ,required?)]
     [(Values: rs)
@@ -293,22 +302,24 @@
                  (list ,@(map type->sexp exports))
                  (list ,@(map type->sexp init-depends))
                  ,(type->sexp result))]
-    [(arr: dom (Values: (list (Result: t (PropSet: (TrueProp:)
-                                                   (TrueProp:))
-                                       (Empty:))))
-           #f #f '())
-     `(make-arr* (list ,@(map type->sexp dom))
-                 ,(type->sexp t))]
-    [(arr: dom rng #f #f '())
-     `(make-arr* (list ,@(map type->sexp dom))
-                 ,(type->sexp rng))]
-    [(arr: dom rng rest drest kws)
-     `(make-arr (list ,@(map type->sexp dom))
-                ,(type->sexp rng)
-                ,(and rest (type->sexp rest))
-                ,(and drest `(cons ,(type->sexp (car drest))
-                                   (quote ,(cdr drest))))
-                (list ,@(map type->sexp kws)))]
+    [(Arrow: dom #f '()
+             (Values: (list (Result: t (PropSet: (TrueProp:)
+                                                 (TrueProp:))
+                                     (Empty:)))))
+     `(-Arrow (list ,@(map type->sexp dom))
+              ,(type->sexp t))]
+    [(Arrow: dom #f '() rng)
+     `(-Arrow (list ,@(map type->sexp dom))
+              ,(type->sexp rng))]
+    [(Arrow: dom rest kws rng)
+     `(make-Arrow
+       (list ,@(map type->sexp dom))
+       ,(and rest (type->sexp rest))
+       (list ,@(map type->sexp kws))
+       ,(type->sexp rng))]
+    [(RestDots: ty db)
+     `(make-RestDots ,(type->sexp ty)
+                     (quote ,db))]
     [(Distinction: nm id ty)
      `(make-Distinction (quote ,nm)
                         (quote ,id)
diff --git a/typed-racket-lib/typed-racket/env/lexical-env.rkt b/typed-racket-lib/typed-racket/env/lexical-env.rkt
index 81d8a473..fe77cfe1 100644
--- a/typed-racket-lib/typed-racket/env/lexical-env.rkt
+++ b/typed-racket-lib/typed-racket/env/lexical-env.rkt
@@ -39,6 +39,7 @@
 (define (add-props-to-current-lexical! ps)
   (lexical-env (env-replace-props (lexical-env) (append ps (env-props (lexical-env))))))
 
+
 ;; run code in an extended env
 (define-syntax (with-extended-lexical-env stx)
   (syntax-parse stx
@@ -48,15 +49,19 @@
                     #:defaults ([objs #'#f]))]
         . body)
      (syntax/loc stx
-       (let ([idents ids]
+       (let ([cur-env (lexical-env)]
+             [idents ids]
              [types tys])
-         (let ([ps (apply append
-                          (for*/list ([(id ty) (in-parallel (in-list idents) (in-list types))]
-                                      [props (in-value (extract-props (-id-path id) ty))]
-                                      #:unless (null? props))
-                            props))])
-           (with-lexical-env (env-replace-props (env-extend/bindings (lexical-env) ids tys objs)
-                                                (append ps (env-props (lexical-env))))
+         (let ([ps (apply
+                    append
+                    (for*/list ([(id ty) (in-parallel (in-list idents) (in-list types))]
+                                [props (in-value (extract-props (-id-path id) ty))]
+                                #:unless (null? props))
+                      props))])
+           (with-lexical-env
+               (env-replace-props
+                (env-extend/bindings cur-env ids tys objs)
+                (append ps (env-props cur-env)))
              . body))))]))
 
 ;; find the type of identifier i, looking first in the lexical env, then in the top-level env
diff --git a/typed-racket-lib/typed-racket/env/type-env-structs.rkt b/typed-racket-lib/typed-racket/env/type-env-structs.rkt
index 609ab957..b405c3cc 100644
--- a/typed-racket-lib/typed-racket/env/type-env-structs.rkt
+++ b/typed-racket-lib/typed-racket/env/type-env-structs.rkt
@@ -2,6 +2,7 @@
 
 (require racket/match
          syntax/id-table
+         racket/sequence
          (except-in "../utils/utils.rkt" env)
          (contract-req)
          ;; dict ops only used for convenient printing
@@ -68,10 +69,22 @@
 ;; simplifications like env+ in tc-envops.rkt)
 (define-syntax (with-naively-extended-lexical-env stx)
   (syntax-parse stx
-    [(_ [#:props ps:expr]
+    [(_ [(~optional (~seq #:identifiers ids-expr:expr
+                          #:types ts-expr:expr)
+                    #:defaults ([ids-expr #'(list)]
+                                [ts-expr #'(list)]))
+         (~optional (~seq #:props ps:expr)
+                    #:defaults ([ps #'(list)]))]
         . body)
      (syntax/loc stx
-       (with-lexical-env (env-replace-props (lexical-env) (append ps (env-props (lexical-env)))) . body))]))
+       (let ([cur-env (lexical-env)]
+             [ids ids-expr]
+             [ts ts-expr])
+         (with-lexical-env
+             (env-replace-props
+              (env-extend/bindings cur-env ids ts #f)
+              (append ps (env-props cur-env)))
+           . body)))]))
 
 
 (define (env-replace-props e props)
diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index 59a2bc71..e110f425 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -367,18 +367,20 @@
         (extend-tvars (list dbound)
           (cgen/seq (context-add context #:bounds (list dbound)) (seq ss (uniform-end s-dty)) t-seq))])]))
 
-(define/cond-contract (cgen/arr context s-arr t-arr)
-  (context? arr? arr? . -> . (or/c #f cset?))
+(define/cond-contract (cgen/arrow context s-arr t-arr)
+  (context? Arrow? Arrow? . -> . (or/c #f cset?))
   (match* (s-arr t-arr)
-    [((arr: ss s s-rest s-drest s-kws) (arr: ts t t-rest t-drest t-kws))
-     (define (rest->end rest drest)
-       (cond
-         [rest (uniform-end rest)]
-         [drest (dotted-end (car drest) (cdr drest))]
-         [else (null-end)]))
+    [((Arrow: ss s-rest s-kws s)
+      (Arrow: ts t-rest t-kws t))
+     (define (rest->end rest)
+       (match rest
+         [(? Type?) (uniform-end rest)]
+         [(RestDots: ty dbound)
+          (dotted-end ty dbound)]
+         [_ (null-end)]))
 
-     (define s-seq (seq ss (rest->end s-rest s-drest)))
-     (define t-seq (seq ts (rest->end t-rest t-drest)))
+     (define s-seq (seq ss (rest->end s-rest)))
+     (define t-seq (seq ts (rest->end t-rest)))
      (and (null? s-kws)
           (null? t-kws)
           (% cset-meet
@@ -545,7 +547,7 @@
            (and cs
                 (implies-in-env? (lexical-env)
                                  (-is-type obj S)
-                                 (instantiate-rep/obj raw-prop obj S))
+                                 (instantiate-obj raw-prop obj))
                 (cset-meet* (cons empty cs))))]
         
         ;; constrain *each* element of es to be below T, and then combine the constraints
@@ -768,14 +770,14 @@
         ;; parameters are just like one-arg functions
         [((Param: in1 out1) (Param: in2 out2))
          (% cset-meet (cg in2 in1) (cg out1 out2))]
-        [((Function: (list s-arr ...))
-          (Function: (list t-arr ...)))
+        [((Fun: s-arr)
+          (Fun: t-arr))
          (% cset-meet*
             (for/list/fail
              ([t-arr (in-list t-arr)])
              ;; for each element of t-arr, we need to get at least one element of s-arr that works
              (let ([results (for*/list ([s-arr (in-list s-arr)]
-                                        [v (in-value (cgen/arr context s-arr t-arr))]
+                                        [v (in-value (cgen/arrow context s-arr t-arr))]
                                         #:when v)
                               v)])
                ;; ensure that something produces a constraint set
diff --git a/typed-racket-lib/typed-racket/infer/promote-demote.rkt b/typed-racket-lib/typed-racket/infer/promote-demote.rkt
index 2cb61638..ab3f829c 100644
--- a/typed-racket-lib/typed-racket/infer/promote-demote.rkt
+++ b/typed-racket-lib/typed-racket/infer/promote-demote.rkt
@@ -36,22 +36,23 @@
   ;; Returns the changed arr or #f if there is no arr above it
   (define (arr-change arr)
     (match arr
-      [(arr: dom rng rest drest kws)
+      [(Arrow: dom rest kws rng)
        (cond
          [(apply V-in? V (get-propsets rng))
           #f]
-         [(and drest (memq (cdr drest) V))
-          (make-arr (map contra dom)
-                    (co rng)
-                    (contra (car drest))
-                    #f
-                    (map contra kws))]
+         [(and (RestDots? rest)
+               (memq (RestDots-nm rest) V))
+          (make-Arrow
+           (map contra dom)
+           (contra (RestDots-ty rest))
+           (map contra kws)
+           (co rng))]
          [else
-          (make-arr (map contra dom)
-                    (co rng)
-                    (and rest (contra rest))
-                    (and drest (cons (contra (car drest)) (cdr drest)))
-                    (map contra kws))])]))
+          (make-Arrow
+           (map contra dom)
+           (and rest (contra rest))
+           (map contra kws)
+           (co rng))])]))
   (match cur
     [(app Rep-variances variances) #:when variances 
      (define mk (Rep-constructor cur))
@@ -72,8 +73,7 @@
     [(F: name) (if (memq name V)
                    (if change Univ -Bottom)
                    cur)]
-    [(Function: arrs)
-     (make-Function (filter-map arr-change arrs))]
+    [(Fun: arrs) (make-Fun (filter-map arr-change arrs))]
     [(HeterogeneousVector: elems)
      (make-HeterogeneousVector (map (λ (t) (if (V-in? V t)
                                                (if change Univ -Bottom)
diff --git a/typed-racket-lib/typed-racket/logic/proves.rkt b/typed-racket-lib/typed-racket/logic/proves.rkt
index cdd93570..d77948e3 100644
--- a/typed-racket-lib/typed-racket/logic/proves.rkt
+++ b/typed-racket-lib/typed-racket/logic/proves.rkt
@@ -7,14 +7,9 @@
  ("../typecheck/tc-subst.rkt" (instantiate-rep/obj)))
 
 (provide (rename-out [implies-in-env?-for-stupid-infer-unit
-                      implies-in-env?]
-                     [instantiate-rep/obj-for-stupid-infer-unit
-                      instantiate-rep/obj]))
+                      implies-in-env?]))
 
 ;; the units for infer currently make it impossible to do
 ;; lazy requires
 (define (implies-in-env?-for-stupid-infer-unit env p q)
-  (implies-in-env? env p q))
-
-(define (instantiate-rep/obj-for-stupid-infer-unit rep obj type)
-  (instantiate-rep/obj rep obj type))
\ No newline at end of file
+  (implies-in-env? env p q))
\ No newline at end of file
diff --git a/typed-racket-lib/typed-racket/optimizer/unboxed-let.rkt b/typed-racket-lib/typed-racket/optimizer/unboxed-let.rkt
index bb605919..64bd5472 100644
--- a/typed-racket-lib/typed-racket/optimizer/unboxed-let.rkt
+++ b/typed-racket-lib/typed-racket/optimizer/unboxed-let.rkt
@@ -128,10 +128,10 @@
   (pattern ((fun-name:constant-var) (~and fun (#%plain-lambda params body ...)))
     #:do [(define doms
             (match (type-of #'fun)
-              [(tc-result1: (Function: (list (arr: doms rngs
-                                                   (and rests #f)
-                                                   (and drests #f)
-                                                   (and kws '())))))
+              [(tc-result1: (Fun: (list (Arrow: doms
+                                                #f  ;; rest arg
+                                                '() ;; kw args
+                                                _))))
                doms]
               [_ #f]))]
     #:when doms
diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt
index 955ae061..a4890b57 100644
--- a/typed-racket-lib/typed-racket/private/parse-type.rkt
+++ b/typed-racket-lib/typed-racket/private/parse-type.rkt
@@ -3,11 +3,10 @@
 ;; This module provides functions for parsing types written by the user
 
 (require (rename-in "../utils/utils.rkt" [infer infer-in])
-         (except-in (rep core-rep type-rep object-rep rep-utils) make-arr)
-         (rename-in (types abbrev utils prop-ops resolve
-                           classes prefab signatures
-                           subtype path-type numeric-tower)
-                    [make-arr* make-arr])
+         (rep core-rep type-rep object-rep rep-utils)
+         (types abbrev utils prop-ops resolve
+                classes prefab signatures
+                subtype path-type numeric-tower)
          (only-in (infer-in infer) intersect)
          (utils tc-utils stxclass-util literal-syntax-class)
          syntax/stx (prefix-in c: (contract-req))
@@ -518,7 +517,7 @@
        (parse-object-type stx)]
       [(:Refinement^ p?:id)
        (match (lookup-id-type/lexical #'p?)
-         [(and t (Function: (list (arr: (list dom) _ #f #f '()))))
+         [(and t (Fun: (list (Arrow: (list dom) #f '() _))))
           (make-Refinement dom #'p?)]
          [t (parse-error "expected a predicate for argument to Refinement"
                          "given" t)])]
@@ -613,11 +612,11 @@
       [(:pred^ t)
        (make-pred-ty (parse-type #'t))]
       [(:case->^ tys ...)
-       (make-Function
+       (make-Fun
         (for/list ([ty (in-syntax #'(tys ...))])
           (let ([t (parse-type ty)])
             (match t
-              [(Function: (list arr)) arr]
+              [(Fun: (list arr)) arr]
               [_ (parse-error
                   #:stx ty
                   "expected a function type for component of case-> type"
@@ -688,10 +687,8 @@
        (with-arity (length doms)
          (let ([doms (for/list ([d (in-list doms)])
                        (parse-type d))])
-           (make-Function
-            (list (make-arr
-                   doms
-                   (parse-type (syntax/loc stx (rest-dom ...))))))))]
+           (make-Fun
+            (list (-Arrow doms (parse-type (syntax/loc stx (rest-dom ...))))))))]
       [(~or (:->^ dom rng :colon^ latent:simple-latent-prop)
             (dom :->^ rng :colon^ latent:simple-latent-prop))
        ;; use parse-type instead of parse-values-type because we need to add the props from the pred-ty
@@ -701,8 +698,8 @@
       [(~or (:->^ dom:non-keyword-ty ... kws:keyword-tys ... rest:non-keyword-ty ddd:star rng)
             (dom:non-keyword-ty ... kws:keyword-tys ... rest:non-keyword-ty ddd:star :->^ rng))
        (with-arity (length (syntax->list #'(dom ...)))
-         (make-Function
-          (list (make-arr
+         (make-Fun
+          (list (-Arrow
                  (parse-types #'(dom ...))
                  (parse-values-type #'rng)
                  #:rest (parse-type #'rest)
@@ -716,7 +713,7 @@
               #:stx #'bound
               "used a type variable not bound with ... as a bound on a ..."
               "variable" bnd))
-           (make-Function
+           (make-Fun
             (list
              (make-arr-dots (parse-types #'(dom ...))
                             (parse-values-type #'rng)
@@ -727,7 +724,7 @@
             (dom:non-keyword-ty ... rest:non-keyword-ty _:ddd :->^ rng))
        (with-arity (length (syntax->list #'(dom ...)))
          (let ([var (infer-index stx)])
-           (make-Function
+           (make-Fun
             (list
              (make-arr-dots (parse-types #'(dom ...))
                             (parse-values-type #'rng)
@@ -744,11 +741,10 @@
        (with-arity (length doms)
          (let ([doms (for/list ([d (in-list doms)])
                        (parse-type d))])
-           (make-Function
-            (list (make-arr
-                   doms
-                   (parse-values-type #'rng)
-                   #:kws (map force (attribute kws.Keyword)))))))]
+           (make-Fun
+            (list (-Arrow doms
+                          (parse-values-type #'rng)
+                          #:kws (map force (attribute kws.Keyword)))))))]
       ;; This case needs to be at the end because it uses cut points to give good error messages.
       [(~or (:->^ ~! dom:non-keyword-ty ... rng:expr
                   :colon^ (~var latent (full-latent (syntax->list #'(dom ...)))))
@@ -1112,7 +1108,7 @@
   ;;       module since it's duplicated elsewhere
   (define (function-type? type)
     (match (resolve type)
-      [(? Function?) #t]
+      [(? Fun?) #t]
       [(Poly: _ body) (function-type? body)]
       [(PolyDots: _ body) (function-type? body)]
       [(PolyRow: _ _ body) (function-type? body)]
@@ -1143,7 +1139,7 @@
      (ret (parse-types #'(t ...))
           empties
           empties)]
-    [:AnyValues^ (tc-any-results #f)]
+    [:AnyValues^ (-tc-any-results #f)]
     [t (ret (parse-type #'t) #f #f)]))
 
 (define parse-type/id (parse/id parse-type))
diff --git a/typed-racket-lib/typed-racket/private/type-annotation.rkt b/typed-racket-lib/typed-racket/private/type-annotation.rkt
index 664d8f37..a0bff3c9 100644
--- a/typed-racket-lib/typed-racket/private/type-annotation.rkt
+++ b/typed-racket-lib/typed-racket/private/type-annotation.rkt
@@ -73,36 +73,49 @@
 ;; tc-expr : a function like `tc-expr' from tc-expr-unit
 ;; tc-expr/check : a function like `tc-expr/check' from tc-expr-unit
 (define/cond-contract (get-type/infer stxs expr tc-expr tc-expr/check)
-  ((listof identifier?) syntax? (syntax? . -> . tc-results/c) (syntax? tc-results/c . -> . tc-results/c)
-   . -> . (listof tc-result?))
+  ((listof identifier?)
+   syntax?
+   (syntax? . -> . tc-results/c)
+   (syntax? tc-results/c . -> . tc-results/c)
+   . -> .
+   (listof tc-result?))
   (match stxs
     [(list stx ...)
-     (let ([anns (for/list ([s (in-list stxs)]) (type-annotation s #:infer #t))])
+     (let ([anns (for/list ([s (in-list stxs)])
+                   (type-annotation s #:infer #t))])
        (if (for/and ([a (in-list anns)]) a)
            (match (tc-expr/check expr (ret anns))
-             [(tc-results: tys fs os)
-              (map tc-result tys fs os)])
-           (let ([res (tc-expr expr)])
-             (match res
-               [(tc-any-results: _)
-                (tc-error/expr
-                 #:return (map (lambda _ (tc-result (Un))) stxs)
-                 "Expression should produce ~a values, but produces an unknown number of values"
-                 (length stxs))]
-               [(tc-results: (list (== -Bottom)) _ _)
-                (for/list ([_ (in-range (length stxs))])
-                  (tc-result -Bottom))]
-               [(tc-results: tys fs os)
-                (if (not (= (length stxs) (length tys)))
-                    (tc-error/expr #:return (map (lambda _ (tc-result (Un))) stxs)
-                                   "Expression should produce ~a values, but produces ~a values of types ~a"
-                                   (length stxs) (length tys) (stringify tys))
-                    (for/list ([stx (in-list stxs)] [ty (in-list tys)]
-                               [a (in-list anns)] [f (in-list fs)] [o (in-list os)])
-                      (cond [a (check-type stx ty a) (tc-result a f o)]
-                            ;; mutated variables get generalized, so that we don't infer too small a type
-                            [(is-var-mutated? stx) (tc-result (generalize ty) f o)]
-                            [else (tc-result ty f o)])))]))))]))
+             [(tc-results: tcrs _) tcrs])
+           (match (tc-expr expr)
+             [(tc-any-results: _)
+              (tc-error/expr
+               #:return (map (λ _ (-tc-result -Bottom)) stxs)
+               "Expression should produce ~a values, but produces an unknown number of values"
+               (length stxs))]
+             [(tc-result1: (== -Bottom))
+              (for/list ([_ (in-range (length stxs))])
+                (-tc-result -Bottom))]
+             [(tc-results: tcrs _)
+              (cond
+                [(not (= (length stxs) (length tcrs)))
+                 (tc-error/expr #:return (map (λ _ (-tc-result -Bottom)) stxs)
+                                "Expression should produce ~a values, but produces ~a values of types ~a"
+                                (length stxs)
+                                (length tcrs)
+                                (stringify (map tc-result-t tcrs)))]
+                [else
+                 (for/list ([stx (in-list stxs)]
+                            [tcr (in-list tcrs)]
+                            [a   (in-list anns)])
+                   (match tcr
+                     [(tc-result: ty ps o)
+                      (cond [a (check-type stx ty a)
+                               (-tc-result a ps o)]
+                            ;; mutated variables get generalized, so that we don't
+                            ;; infer too small a type
+                            [(is-var-mutated? stx)
+                             (-tc-result (generalize ty) ps o)]
+                            [else (-tc-result ty ps o)])]))])])))]))
 
 ;; check that e-type is compatible with ty in context of stx
 ;; otherwise, error
diff --git a/typed-racket-lib/typed-racket/private/type-contract.rkt b/typed-racket-lib/typed-racket/private/type-contract.rkt
index f2f02979..9a416b7a 100644
--- a/typed-racket-lib/typed-racket/private/type-contract.rkt
+++ b/typed-racket-lib/typed-racket/private/type-contract.rkt
@@ -504,7 +504,7 @@
                                  chaperones
                                  (if prop (list prop) '())
                                  impersonators))])]
-       [(and t (Function: arrs))
+       [(and t (Fun: arrs))
         #:when (any->bool? arrs)
         ;; Avoid putting (-> any T) contracts on struct predicates (where Boolean <: T)
         ;; Optimization: if the value is typed, we can assume it's not wrapped
@@ -515,7 +515,7 @@
                                  unsafe-spp/sc
                                  safe-spp/sc)])
           (or/sc optimized/sc (t->sc/fun t)))]
-       [(and t (Function: _)) (t->sc/fun t)]
+       [(and t (? Fun?)) (t->sc/fun t)]
        [(Set: t) (set/sc (t->sc t))]
        [(Sequence: ts) (apply sequence/sc (map t->sc ts))]
        [(Vector: t) (vectorof/sc (t->sc/both t))]
@@ -531,7 +531,7 @@
        [(Continuation-Mark-Keyof: t)
         (continuation-mark-key/sc (t->sc t))]
        ;; TODO: this is not quite right for case->
-       [(Prompt-Tagof: s (Function: (list (arr: (list ts ...) _ _ _ _))))
+       [(Prompt-Tagof: s (Fun: (list (Arrow: ts _ _ _))))
         (prompt-tag/sc (map t->sc ts) (t->sc s))]
        ;; TODO
        [(F: v)
@@ -740,33 +740,34 @@
   ;; handle-range : Arr (-> Static-Contact) -> Static-Contract
   ;; Match the range of an arr and determine if a contract can be generated
   ;; and call the given thunk or raise an error
-  (define (handle-range arr convert-arr)
-    (match arr
+  (define (handle-range arrow convert-arrow)
+    (match arrow
       ;; functions with no props or objects
-      [(arr: dom (Values: (list (Result: rngs
-                                         (PropSet: (TrueProp:)
-                                                   (TrueProp:))
-                                         (Empty:)) ...))
-             rst drst kws)
-       (convert-arr)]
+      [(Arrow: _ _ _
+               (Values: (list (Result: _
+                                       (PropSet: (TrueProp:)
+                                                 (TrueProp:))
+                                       (Empty:)) ...)))
+       (convert-arrow)]
       ;; Functions that don't return
-      [(arr: dom (Values: (list (Result: (== -Bottom) _ _) ...)) rst drst kws)
-       (convert-arr)]
+      [(Arrow: _ _ _
+               (Values: (list (Result: (== -Bottom) _ _) ...)))
+       (convert-arrow)]
       ;; functions with props or objects
-      [(arr: dom (Values: (list (Result: rngs _ _) ...)) rst drst kws)
+      [(Arrow: _ _ _ (Values: (list (Result: rngs _ _) ...)))
        (if (from-untyped? typed-side)
            (fail #:reason (~a "cannot generate contract for function type"
                               " with props or objects."))
-           (convert-arr))]
-      [(arr: dom (? ValuesDots?) rst drst kws)
+           (convert-arrow))]
+      [(Arrow: _ _ _ (? ValuesDots?))
        (fail #:reason (~a "cannot generate contract for function type"
                           " with dotted return values"))]
-      [(arr: dom (? AnyValues?) rst drst kws)
+      [(Arrow: _ _ _ (? AnyValues?))
        (fail #:reason (~a "cannot generate contract for function type"
                           " with unknown return values"))]))
 
   (match f
-    [(Function: arrs)
+    [(Fun: arrows)
      ;; Try to generate a single `->*' contract if possible.
      ;; This allows contracts to be generated for functions with both optional and keyword args.
      ;; (and don't otherwise require full `case->')
@@ -781,15 +782,15 @@
       ;;  since this code would generate contracts that accept any number of arguments between
       ;;  2 and 6, which is wrong.
       ;; TODO sufficient condition, but may not be necessary
-      [(has-optional-args? arrs)
-       (define first-arr (first arrs))
-       (define last-arr (last arrs))
-       (define (convert-arr)
-         (match-define (arr: first-dom (Values: (list (Result: rngs _ _) ...))
-                             rst _ kws)
-                       first-arr)
+      [(has-optional-args? arrows)
+       (define first-arrow (first arrows))
+       (define last-arrow (last arrows))
+       (define (convert-arrow)
+         (match-define (Arrow: first-dom rst kws
+                               (Values: (list (Result: rngs _ _) ...)))
+           first-arrow)
          ;; all but dom is the same for all arrs
-         (match-define (arr: last-dom _ _ _ _) last-arr)
+         (define last-dom (Arrow-dom last-arrow))
          (define mand-args (map t->sc/neg first-dom))
          (define opt-args (map t->sc/neg (drop last-dom (length first-dom))))
          (define-values (mand-kws opt-kws)
@@ -799,12 +800,12 @@
          (define range (map t->sc rngs))
          (define rest (and rst (listof/sc (t->sc/neg rst))))
          (function/sc (from-typed? typed-side) (process-dom mand-args) opt-args mand-kws opt-kws rest range))
-       (handle-range first-arr convert-arr)]
+       (handle-range first-arrow convert-arrow)]
       [else
        (define ((f case->) a)
          (define (convert-arr arr)
            (match arr
-             [(arr: dom (Values: (list (Result: rngs _ _) ...)) rst drst kws)
+             [(Arrow: dom rst kws (Values: (list (Result: rngs _ _) ...)))
               (let-values ([(mand-kws opt-kws) (partition-kws kws)])
                 ;; Garr, I hate case->!
                 (when (and (not (empty? kws)) case->)
@@ -820,23 +821,24 @@
                     null
                     (map conv mand-kws)
                     (map conv opt-kws)
-                    (or
-                      (and rst (listof/sc (t->sc/neg rst)))
-                      (and drst (listof/sc (t->sc/neg (car drst)
-                                                      #:recursive-values
-                                                        (hash-set recursive-values (cdr drst) (same any/sc))))))
+                    (match rst
+                      [(? Type?) (listof/sc (t->sc/neg rst))]
+                      [(RestDots: dty dbound)
+                       (listof/sc
+                        (t->sc/neg dty
+                                   #:recursive-values
+                                   (hash-set recursive-values dbound (same any/sc))))]
+                      [_ #f])
                     (map t->sc rngs))))]))
          (handle-range a (λ () (convert-arr a))))
        (define arities
-         (for/list ([t arrs])
-           (match t
-             [(arr: dom _ _ _ _) (length dom)])))
+         (for/list ([t (in-list arrows)]) (length (Arrow-dom t))))
        (define maybe-dup (check-duplicates arities))
        (when maybe-dup
          (fail #:reason (~a "function type has two cases of arity " maybe-dup)))
-       (if (= (length arrs) 1)
-           ((f #f) (first arrs))
-           (case->/sc (map (f #t) arrs)))])]))
+       (if (= (length arrows) 1)
+           ((f #f) (first arrows))
+           (case->/sc (map (f #t) arrows)))])]))
 
 ;; Generate a contract for a object/class method clause
 ;; Precondition: type is a valid method type
@@ -851,7 +853,7 @@
      (t->sc/polydots type fail typed-side recursive-values rec)]
     [(? PolyRow?)
      (t->sc/polyrow type fail typed-side recursive-values rec)]
-    [(? Function?)
+    [(? Fun?)
      (t->sc/function type fail typed-side recursive-values loop #t)]
     [_ (fail #:reason "invalid method type")]))
 
@@ -868,7 +870,7 @@
         (define function-type?
           (let loop ([ty b])
             (match (resolve ty)
-              [(Function: _) #t]
+              [(? Fun?) #t]
               [(Union: _ elems) (andmap loop elems)]
               [(Intersection: elems _) (ormap loop elems)]
               [(Poly: _ body) (loop body)]
@@ -907,7 +909,7 @@
         (define function-type?
           (let loop ([ty b])
             (match (resolve ty)
-              [(Function: _) #t]
+              [(? Fun?) #t]
               [(Union: _ elems) (andmap loop elems)]
               [(Intersection: elems _) (ormap loop elems)]
               [(Poly: _ body) (loop body)]
@@ -939,9 +941,9 @@
 ;; True if the arities `arrs` are what we'd expect from a struct predicate
 (define (any->bool? arrs)
   (match arrs
-    [(list (arr: (list (Univ:))
-                 (Values: (list (Result: t _ _)))
-                 #f #f '()))
+    [(list (Arrow: (list (Univ:))
+                   #f '()
+                   (Values: (list (Result: t _ _)))))
      (t:subtype -Boolean t)]
     [_ #f]))
 
diff --git a/typed-racket-lib/typed-racket/rep/object-rep.rkt b/typed-racket-lib/typed-racket/rep/object-rep.rkt
index 4ea86f2d..3054a953 100644
--- a/typed-racket-lib/typed-racket/rep/object-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/object-rep.rkt
@@ -29,6 +29,8 @@
          LExp-terms
          LExp:
          genobj
+         make-id-seq
+         id-seq-next
          make-obj-seq
          obj-seq-next
          scale-obj
@@ -66,9 +68,10 @@
   [#:frees (f)  (combine-frees (map f elems))]
   [#:fmap (f) (make-Path (map f elems) name)]
   [#:for-each (f) (for-each f elems)]
-  [#:custom-constructor
-   (cond
-     [(identifier? name)
+  [#:custom-constructor/contract
+   (-> (listof PathElem?) (or/c name-ref/c OptObject?) OptObject?)
+   (match name
+     [(? identifier?)
       ;; we don't want objects for visibly mutated or top level variables
       (if (or (is-var-mutated? name)
               (and (not (identifier-binding name))
@@ -78,20 +81,58 @@
             (intern-double-ref!
              Path-intern-table
              name elems #:construct (make-Path elems name))))]
-     [else (intern-double-ref!
-            Path-intern-table
-            name elems #:construct (make-Path elems name))])])
+     [(? pair?)
+      (intern-double-ref!
+       Path-intern-table
+       name elems #:construct (make-Path elems name))]
+     [(Path: elems* name*)
+      (let ([elems* (append elems elems*)])
+        (intern-double-ref!
+         Path-intern-table
+         name* elems* #:construct (make-Path elems* name*)))]
+     [(? LExp? l) (if (null? elems) l -empty-obj)]
+     [(Empty:) -empty-obj])])
 
 (define Path-intern-table (make-weak-hash))
 
 (define (-id-path name) (make-Path null name))
 
+;; creates an "id sequence" -- use 'id-seq-next'
+;; to iterate through the sequence.
+;; For an example use case, see subtype.rkt,
+;; which uses a seq to reuse fresh ids for subtype
+;; checking for dependent arrows
+(define (make-id-seq)
+  (for/fold ([seq (cons (genid) (box #f))])
+            ([_ (in-range 9)])
+    (cons (genid) seq)))
+
+;; id-seq-next
+;;
+;; returns 2 values
+;; val 1 - the next id
+;; val 2 - the rest of the sequence
+(define (id-seq-next s)
+  (match s
+    [(cons val vals)
+     (values val vals)]
+    [(box (cons val vals))
+     (values val vals)]
+    [(box #f)
+     (define more (make-id-seq))
+     (if (box-cas! s #f more)
+         (id-seq-next more)
+         (id-seq-next s))]))
+
+
+
 ;; generates a fresh id object
 ;; NOTE: use this wisely -- calling this function
 ;; all the time will consume memory leading to GC
 ;; time that may add up during typechecking
 (define (genobj) (-id-path (genid)))
 
+
 ;; creates an "object sequence" -- use 'obj-seq-next'
 ;; to iterate through the sequence.
 ;; For an example use case, see subtype.rkt,
@@ -161,11 +202,11 @@
 
 ;; make-LExp* (provided as make-LExp)
 ;;
-; IF the lexp (exp) contains only 1 variable,
+;; IF the lexp (exp) contains only 1 variable,
 ;;   and that variables its coefficient is 1,
-;    and the constant is 0
-; THEN that lone variable is returned
-; ELSE it returns the LExp
+;;    and the constant is 0
+;; THEN that lone variable is returned
+;; ELSE it returns the LExp
 ;; NOTE 1: We do this so there is a 'canonical form'
 ;; for linear expressions which are actually just
 ;; the underlying object, e.g. insteaf of
@@ -326,4 +367,4 @@
 (define (add-path-to-lexp p l)
   (match l
     [(LExp: const terms)
-     (make-LExp* const (terms-set terms p (add1 (terms-ref terms p))))]))
+     (make-LExp* const (terms-set terms p (add1 (terms-ref terms p))))]))
\ No newline at end of file
diff --git a/typed-racket-lib/typed-racket/rep/rep-utils.rkt b/typed-racket-lib/typed-racket/rep/rep-utils.rkt
index 782d1254..4d93edc9 100644
--- a/typed-racket-lib/typed-racket/rep/rep-utils.rkt
+++ b/typed-racket-lib/typed-racket/rep/rep-utils.rkt
@@ -91,7 +91,6 @@
       (hash-id name)
       (rec name)))
 
-
 ;; This table maps a type to an identifier bound to the type.
 ;; This allows us to avoid reconstructing the type when using
 ;; it from its marshaled representation.
@@ -379,7 +378,7 @@
                 (or (not (attribute frees-spec))
                     (not (attribute for-each-spec))
                     (not (attribute fold-spec))))
-       (raise-syntax-error 'def-rep "non-base reps require #:frees, #:for-each, and #:fold"
+       (raise-syntax-error 'def-rep "non-base reps require #:frees, #:for-each, and #:fmap"
                            #'var))
 
      ;; - - - - - - - - - - - - - - -
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 4df5eb1b..24edae33 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -54,17 +54,18 @@
          Union-all-flat:
          Union/set:
          Intersection?
-         subst-names
-         inc-lvl
-         abstract-names
          -refine
          Refine:
          Refine-obj:
          Refine-name:
          save-term-var-names!
          extract-props
-         (rename-out [instantiate instantiate-raw-type]
-                     [Union:* Union:]
+         instantiate-type
+         abstract-type
+         instantiate-obj
+         abstract-obj
+         substitute-names
+         (rename-out [Union:* Union:]
                      [Intersection:* Intersection:]
                      [make-Intersection* make-Intersection]
                      [Class:* Class:]
@@ -114,6 +115,11 @@
 ;; as it is both Top and Bottom.
 (def-type Error () [#:singleton Err])
 
+;;************************************************************
+;; Type Variables/Applications
+;;************************************************************
+
+
 ;; de Bruijn indexes - should never appear outside of this file
 ;; bound type variables
 ;; i is an nat
@@ -394,9 +400,9 @@
 (def-structural Continuation-Mark-Keyof ([value #:invariant])
   [#:mask mask:continuation-mark-key])
 
-;; * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 
+;;************************************************************
 ;; List/Vector Types (that are not simple structural types)
-;; * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 
+;;************************************************************
 
 ;; dotted list -- after expansion, becomes normal Pair-based list type
 (def-type ListDots ([dty Type?] [dbound (or/c symbol? natural-number/c)])
@@ -422,9 +428,10 @@
   [#:mask mask:vector])
 
 
-;; * * * * * * *
-;; Type Binders
-;; * * * * * * *
+;;************************************************************
+;; Type Binders (Polys, Mus, etc)
+;;************************************************************
+
 
 
 (def-type Mu ([body Type?])
@@ -479,73 +486,83 @@
 
 
 
-;; kw : keyword?
-;; ty : Type
-;; required? : Boolean
+;;************************************************************
+;; Functions, Arrows
+;;************************************************************
+
+
+;; keyword arguments
 (def-rep Keyword ([kw keyword?] [ty Type?] [required? boolean?])
   [#:frees (f) (f ty)]
   [#:fmap (f) (make-Keyword kw (f ty) required?)]
   [#:for-each (f) (f ty)])
 
+(define/provide (Keyword<? kw1 kw2)
+  (keyword<? (Keyword-kw kw1)
+             (Keyword-kw kw2)))
 
-(define (keyword-sorted/c kws)
-  (or (empty? kws)
+;; contract for a sorted keyword list
+(define-for-cond-contract (keyword-sorted/c kws)
+  (or (null? kws)
       (= (length kws) 1)
-      (apply keyword<? (map Keyword-kw kws))))
+      (equal? kws (sort kws Keyword<?))))
 
 
-(def-rep arr ([dom (listof Type?)]
-              [rng SomeValues?]
-              [rest (or/c #f Type?)]
-              [drest (or/c #f (cons/c Type? (or/c natural-number/c symbol?)))]
-              [kws (and/c (listof Keyword?) keyword-sorted/c)])
+(def-rep RestDots ([ty Type?]
+                   [nm (or/c natural-number/c symbol?)])
   [#:frees
    [#:vars (f)
-    (combine-frees
-     (append (map (compose flip-variances f)
-                  (append (if rest (list rest) null)
-                          (map Keyword-ty kws)
-                          dom))
-             (match drest
-               [(cons t (? symbol? bnd))
-                (list (free-vars-remove (flip-variances (f t)) bnd))]
-               [(cons t _)
-                (list (flip-variances (f t)))]
-               [_ null])
-             (list (f rng))))]
+    (cond
+      [(symbol? nm) (free-vars-remove (f ty) nm)]
+      [else (f ty)])]
    [#:idxs (f)
-    (combine-frees
-     (append (map (compose flip-variances f)
-                  (append (if rest (list rest) null)
-                          (map Keyword-ty kws)
-                          dom))
-             (match drest
-               [(cons t (? symbol? bnd))
-                (list (single-free-var bnd variance:contra)
-                      (flip-variances (f t)))]
-               [(cons t _)
-                (list (flip-variances (f t)))]
-               [_ null])
-             (list (f rng))))]]
-  [#:fmap (f) (make-arr (map f dom)
-                        (f rng)
-                        (and rest (f rest))
-                        (and drest (cons (f (car drest)) (cdr drest)))
-                        (map f kws))]
+    (cond
+      [(symbol? nm) (combine-frees (list (f ty) (single-free-var nm)))]
+      [else (f ty)])]]
+  [#:fmap (f) (make-RestDots (f ty) nm)]
+  [#:for-each (f) (f ty)])
+
+
+(def-rep Arrow ([dom (listof Type?)]
+                [rst (or/c #f Type? RestDots?)]
+                [kws (and/c (listof Keyword?) keyword-sorted/c)]
+                [rng SomeValues?])
+  [#:frees (f)
+   (combine-frees
+    (list* (f rng)
+           (if rst
+               (flip-variances (f rst))
+               empty-free-vars)
+           (append
+            (for/list ([kw (in-list kws)])
+              (flip-variances (f kw)))
+            (for/list ([d (in-list dom)])
+              (flip-variances (f d))))))]
+  [#:fmap (f) (make-Arrow (map f dom)
+                          (and rst (f rst))
+                          (map f kws)
+                          (f rng))]
   [#:for-each (f)
    (for-each f dom)
-   (f rng)
-   (when drest (f (car drest)))
-   (when rest (f rest))
-   (for-each f kws)])
+   (when rst (f rst))
+   (for-each f kws)
+   (f rng)])
 
-
-;; arities : Listof[arr]
-(def-type Function ([arities (listof arr?)])
+;; a standard function
+;; + all functions are case-> under the hood (i.e. see 'arrows')
+;; + each Arrow in 'arrows' may have a dependent range
+(def-type Fun ([arrows (listof Arrow?)])
   [#:mask mask:procedure]
-  [#:frees (f) (combine-frees (map f arities))]
-  [#:fmap (f) (make-Function (map f arities))]
-  [#:for-each (f) (for-each f arities)])
+  [#:frees (f) (combine-frees (map f arrows))]
+  [#:fmap (f) (make-Fun (map f arrows))]
+  [#:for-each (f) (for-each f arrows)])
+
+
+
+;;************************************************************
+;; Structs
+;;************************************************************
+
 
 
 (def-rep fld ([t Type?] [acc identifier?] [mutable? boolean?])
@@ -560,7 +577,7 @@
 (def-type Struct ([name identifier?]
                   [parent (or/c #f Struct?)]
                   [flds (listof fld?)]
-                  [proc (or/c #f Function?)]
+                  [proc (or/c #f Fun?)]
                   [poly? boolean?]
                   [pred-id identifier?])
   [#:frees (f) (combine-frees (map f (append (if proc (list proc) null)
@@ -611,6 +628,9 @@
   [#:mask (mask-union mask:struct mask:procedure)])
 
 
+;;************************************************************
+;; Singleton Values (see also Base)
+;;************************************************************
 
 
 ;; v : Racket Value
@@ -634,6 +654,12 @@
      [1 -One]
      [_ (make-Value val)])])
 
+
+;;************************************************************
+;; Unions
+;;************************************************************
+
+
 ;; mask - cached type mask
 ;; base - any Base types, or Bottom if none are present
 ;; ts - the list of types in the union (contains no duplicates,
@@ -785,6 +811,10 @@
 (define (Un . args)
   (Union-fmap (λ (x) x) -Bottom args))
 
+;;************************************************************
+;; Intersection/Refinement
+;;************************************************************
+
 
 ;; Intersection
 ;; ts - the list of types (gives deterministic behavior)
@@ -877,7 +907,7 @@
        [((Intersection: ts prop* tset) _)
         (-refine (make-Intersection ts -tt tset) (-and prop prop*))]
        [(_ _) (make-Intersection (list t) prop (hash t #t))])]
-    [(nm t prop) (-refine t (abstract-names prop (list nm)))]))
+    [(nm t prop) (-refine t (abstract-obj prop nm))]))
 
 (define-match-expander Intersection:*
   (λ (stx) (syntax-case stx ()
@@ -926,6 +956,43 @@
                      (app Intersection-w/o-prop t)
                      (app (λ (i) (Intersection-prop* obj i)) prop)))])))
 
+
+(define (Intersection-prop* obj t)
+  (define p (Intersection-prop t))
+  (and p (instantiate-obj p obj)))
+
+
+;; given the fact that 'obj' is of type 'type',
+;; look inside of type trying to learn
+;; more info about obj
+(define (extract-props obj type)
+  (cond
+    [(Empty? obj) '()]
+    [else
+     (define props '())
+     (let extract! ([rep type]
+                    [obj obj])
+       (match rep
+         [(== -Zero)
+          #:when (with-linear-integer-arithmetic?)
+          (set! props (cons (-eq obj (-lexp 0)) props))]
+         [(== -One)
+          #:when (with-linear-integer-arithmetic?)
+          (set! props (cons (-eq obj (-lexp 1)) props))]
+         [(Pair: t1 t2) (extract! t1 (-car-of obj))
+                        (extract! t2 (-cdr-of obj))]
+         [(Refine-obj: obj t prop)
+          (set! props (cons prop props))
+          (extract! t obj)]
+         [(HeterogeneousVector: ts)
+          #:when (with-linear-integer-arithmetic?)
+          (set! props (cons (-eq (-vec-len-of obj) (-lexp (length ts)))
+                            props))]
+         [(Intersection: ts _ _) (for ([t (in-list ts)])
+                                   (extract! t obj))]
+         [_ (void)]))
+     props]))
+
 ;; refinement based on some predicate function 'pred'
 (def-type Refinement ([parent Type?] [pred identifier?])
   [#:frees (f) (f parent)]
@@ -934,6 +1001,13 @@
   [#:mask (λ (t) (mask (Refinement-parent t)))]
   [#:custom-constructor (make-Refinement parent (normalize-id pred))])
 
+
+;;************************************************************
+;; Object Oriented
+;;************************************************************
+
+
+
 ;; A Row used in type instantiation
 ;; For now, this should not appear in user code. It's used
 ;; internally to perform row instantiations and to represent
@@ -1008,6 +1082,11 @@
   [#:for-each (f) (f cls)]
   [#:mask mask:instance])
 
+;;************************************************************
+;; Units
+;;************************************************************
+
+
 ;; interp:
 ;; name is the id of the signature
 ;; extends is the extended signature or #f
@@ -1084,19 +1163,13 @@
 
 
 ;;************************************************************
-;; Locally Nameles Type Variable Abstraction/Instantiation
+;; Type Variable tools (i.e. Abstraction/Instantiation)
+;; Note: see the 'Locally Nameless' binder
+;;       representation strategy for general
+;;       details on the approach we're using
 ;;************************************************************
 
-
-;; abstract
-;;
-;; abstracts type variable 'name'
-;; to De Bruijn index 0 in 'initial'
-(define/cond-contract (abstract name initial)
-  (-> symbol? Rep? Rep?)
-  (abstract-many (list name) initial))
-
-;; abstract-many
+;; abstract-many/type
 ;;
 ;; abstracts the type variable names from 'names-to-abstract'
 ;; to de bruijn indices in 'initial'.
@@ -1105,97 +1178,93 @@
 ;; names-to-abstract[1] gets mapped to n-2
 ;; ...
 ;; names-to-abstract[n-1] gets mapped to 0
-(define/cond-contract (abstract-many names-to-abstract initial)
-  (-> (listof symbol?) Rep? Rep?)
-  (define n-1 (sub1 (length names-to-abstract)))
-  (define (abstract-name name lvl default dotted?)
-    (match (index-of names-to-abstract name eq?)
-      [#f default]
-      ;; adjust index properly before using (see comments above
-      ;; and note we are under 'lvl' additional binders)
-      [idx (let ([idx (+ lvl (- n-1 idx))])
-             (cond [dotted? idx]
-                   [else (make-B idx)]))]))
-  (let rec/lvl ([cur initial] [lvl 0])
-    (define (rec rep) (rec/lvl rep lvl))
-    (match cur
-      ;; Free type variables
-      [(F: name) (abstract-name name lvl cur #f)]
-      ;; forms w/ (potential) dotted type variables
-      [(arr: dom rng rest drest kws)
-       (make-arr (map rec dom)
-                 (rec rng)
-                 (and rest (rec rest))
-                 (match drest
-                   [(cons d-ty d)
-                    (cons (rec d-ty) (abstract-name d lvl d #t))]
-                   [_ #f])
-                 (map rec kws))]
-      [(ValuesDots: rs dty d)
-       (make-ValuesDots (map rec rs)
-                        (rec dty)
-                        (abstract-name d lvl d #t))]
-      [(ListDots: dty d)
-       (make-ListDots (rec dty)
-                      (abstract-name d lvl d #t))]
-      ;; forms which introduce bindings (increment lvls appropriately)
-      [(Mu: body) (make-Mu (rec/lvl body (add1 lvl)))]
-      [(PolyRow: constraints body)
-       (make-PolyRow constraints (rec/lvl body (add1 lvl)))]
-      [(PolyDots: n body)
-       (make-PolyDots n (rec/lvl body (+ n lvl)))]
-      [(Poly: n body)
-       (make-Poly n (rec/lvl body (+ n lvl)))]
-      [_ (Rep-fmap cur rec)])))
+(define/cond-contract (abstract-type initial names-to-abstract)
+  (-> Rep? (or/c symbol? (listof symbol?)) Rep?)
+  (cond
+    [(null? names-to-abstract) initial]
+    [(not (pair? names-to-abstract))
+     (abstract-type initial (list names-to-abstract))]
+    [else
+     (define n-1 (sub1 (length names-to-abstract)))
+     (define (abstract-name name lvl default dotted?)
+       (cond
+         [(symbol? name)
+          (match (index-of names-to-abstract name eq?)
+            [#f default]
+            ;; adjust index properly before using (see comments above
+            ;; and note we are under 'lvl' additional binders)
+            [idx (let ([idx (+ lvl (- n-1 idx))])
+                   (cond [dotted? idx]
+                         [else (make-B idx)]))])]
+         [else default]))
+     (type-var-transform initial abstract-name)]))
 
 
-;; instantiate
+;; instantiate-type
 ;;
-;; instantiates De Bruijn index 0 with
-;; 'type' in 'initial'
-(define/cond-contract (instantiate type initial)
-  (-> Type? Rep? Rep?)
-  (instantiate-many (list type) initial))
-
-;; instantiate-many
-;;
-;; instantiates De Bruijn indices 0 through
-;; (sub1 (length images)) with the types from images.
+;; instantiates type De Bruijn indices 0 (i.e. (B 0))
+;; through (sub1 (length images)) with images.
+;; (i.e. De Bruin i = (B i))
 ;; Specifically, if n = (length images), then
 ;; index 0 gets mapped to images[n-1]
 ;; index 1 gets mapped to images[n-2]
 ;; ...
 ;; index n-1 gets mapped to images[0]
-(define/cond-contract (instantiate-many images initial)
-  (-> (listof Type?) Rep? Rep?)
-  (define n-1 (sub1 (length images)))
-  (define (instantiate-idx idx lvl default dotted?)
-    ;; adjust for being under 'lvl' binders and for
-    ;; index 0 gets mapped to images[n-1], etc
-    (let ([idx (- n-1 (- idx lvl))])
-      (match (list-ref/default images idx #f)
-        [#f default]
-        [image (cond [dotted? (F-n image)]
-                     [else image])])))
+(define/cond-contract (instantiate-type initial images)
+  (-> Rep? (or/c Type? (listof Type?)) Rep?)
+  (cond
+    [(null? images) initial]
+    [(not (pair? images)) (instantiate-type initial (list images))]
+    [else
+     (define n-1 (sub1 (length images)))
+     (define (instantiate-idx idx lvl default dotted?)
+       (cond
+         [(exact-nonnegative-integer? idx)
+          ;; adjust for being under 'depth' binders and for
+          ;; index 0 gets mapped to images[n-1], etc
+          (let ([idx (- n-1 (- idx lvl))])
+            (match (list-ref/default images idx #f)
+              [#f default]
+              [image (cond [dotted? (F-n image)]
+                           [else image])]))]
+         [else default]))
+     (type-var-transform initial instantiate-idx)]))
+
+
+
+;; type-var-transform
+;;
+;; Helper function for instantiate[-many]/type
+;; and abstract[-many]/type.
+;;
+;; transform : [target : (or nat sym)]
+;;             [lvl : nat]
+;;             [default : (or Type nat sym)]
+;;             [dotted? : boolean]
+;;             ->
+;;             (or Type nat sym)
+;; where 'target' is the thing potentially being replaced
+;; 'depth' is how many binders we're under
+;; 'default' is what it uses if we're not replacing 'target'
+;; 'dotted?' is a flag denoting if this is a dotted var/idx
+(define (type-var-transform initial transform)
   (let rec/lvl ([cur initial] [lvl 0])
     (define (rec rep) (rec/lvl rep lvl))
     (match cur
-      ;; Bound De Bruijn indices
-      [(B: idx) (instantiate-idx idx lvl cur #f)]
-      ;; forms w/ (potential) dotted type indices
-      [(arr: dom rng rest (cons d-ty (? exact-integer? d)) kws)
-       (make-arr (map rec dom)
-                 (rec rng)
-                 (and rest (rec rest))
-                 (cons (rec d-ty) (instantiate-idx d lvl d #t))
-                 (map rec kws))]
-      [(ValuesDots: rs dty (? exact-integer? d))
+      ;; De Bruijn indices
+      [(B: idx) (transform idx lvl cur #f)]
+      ;; Type variables
+      [(F: var) (transform var lvl cur #f)]
+      ;; forms w/ dotted type vars/indices
+      [(RestDots: ty d)
+       (make-RestDots (rec ty) (transform d lvl d #t))]
+      [(ValuesDots: rs dty d)
        (make-ValuesDots (map rec rs)
                         (rec dty)
-                        (instantiate-idx d lvl d #t))]
-      [(ListDots: dty (? exact-integer? d))
+                        (transform d lvl d #t))]
+      [(ListDots: dty d)
        (make-ListDots (rec dty)
-                      (instantiate-idx d lvl d #t))]
+                      (transform d lvl d #t))]
       ;; forms which introduce bindings (increment lvls appropriately)
       [(Mu: body) (make-Mu (rec/lvl body (add1 lvl)))]
       [(PolyRow: constraints body)
@@ -1207,6 +1276,106 @@
       [_ (Rep-fmap cur rec)])))
 
 
+
+;;***************************************************************
+;; Dependent Function/Refinement tools
+;; Note: see the 'Locally Nameless' binder
+;;       representation strategy for general
+;;       details on the approach we're using
+;;***************************************************************
+
+
+
+;; instantiates term De Bruijn indices
+;; '(0 . 0) ... '(0 . (sub1 (length os)))
+;; in 'initial with objects from 'os'
+(define/cond-contract (instantiate-obj initial os)
+  (-> Rep? (or/c identifier?
+                 OptObject?
+                 (listof (or/c identifier? OptObject?)))
+      Rep?)
+  (cond
+    [(null? os) initial]
+    [(not (pair? os)) (instantiate-obj initial (list os))]
+    [else
+     (define (instantiate-idx name cur-lvl)
+       (match name
+         [(cons lvl idx)
+          #:when (eqv? lvl cur-lvl)
+          (list-ref os idx)]
+         [_ name]))
+     (term-var-transform initial instantiate-idx)]))
+
+
+;; abstracts the n identifiers from 'ids-to-abstract'
+;; in 'initial', replacing them with term De Bruijn indices
+;; '(0 . 0) ... '(0 . n-1) (or their appropriate
+;; successors under additional binders)
+(define/cond-contract (abstract-obj initial ids-to-abstract)
+  (-> Rep? (or/c identifier? (listof identifier?)) Rep?)
+  (cond
+    [(null? ids-to-abstract) initial]
+    [(not (pair? ids-to-abstract))
+     (abstract-obj initial (list ids-to-abstract))]
+    [else
+     (define (abstract-id id lvl)
+       (cond
+         [(identifier? id)
+          (match (index-of ids-to-abstract id free-identifier=?)
+            [#f id]
+            ;; adjust index properly before using (see comments above
+            ;; and note we are under 'lvl' additional binders)
+            [idx (cons lvl idx)])]
+         [else id]))
+     (term-var-transform initial abstract-id)]))
+
+
+;; term-binder-transform
+;;
+;; Helper function for abstract[-many]/obj
+;; and instantiate[-many]/obj.
+;;
+;; transform : [target : (or nat sym)]
+;;             [depth : nat]
+;;             ->
+;;             (or nat sym)
+;; where 'target' is the thing potentially being replaced
+;; 'depth' is how many binders we're under
+(define (term-var-transform initial transform)
+  (let rec/lvl ([rep initial] [lvl 0])
+    (define (rec rep) (rec/lvl rep lvl))
+    (define (rec/inc rep) (rec/lvl rep (add1 lvl)))
+    (match rep
+      ;; Functions
+      ;; increment the level of the substituted object
+      [(Arrow: dom rst kws rng)
+       (make-Arrow (map rec dom)
+                   (and rst (rec/inc rst))
+                   (map rec kws)
+                   (rec/inc rng))]
+      ;; Refinement types e.g. {x ∈ τ | ψ(x)}
+      ;; increment the level of the substituted object
+      [(Intersection: ts p _) (-refine
+                               (apply -unsafe-intersect (map rec ts))
+                               (rec/inc p))]
+      [(Path: flds nm)
+       (make-Path (map rec flds)
+                  (transform nm lvl))]
+      [_ (Rep-fmap rep rec)])))
+
+;; simple substitution mapping identifiers to
+;; identifiers (or objects)
+;; pre: (= (length names) (length names-or-objs))
+(define (substitute-names rep names names-or-objs)
+  (let subst ([rep rep])
+    (match rep
+      [(Path: flds (? identifier? name))
+       (make-Path (map subst flds)
+                  (match (index-of names name free-identifier=?)
+                    [#f name]
+                    [idx (list-ref names-or-objs idx)]))]
+      [_ (Rep-fmap rep subst)])))
+
 ;;************************************************************
 ;; Smart Constructors/Destructors for Type Binders
 ;;
@@ -1220,7 +1389,7 @@
 
 ;; the 'smart' constructor
 (define (Mu* name body)
-  (let ([v (make-Mu (abstract name body))])
+  (let ([v (make-Mu (abstract-type body name))])
     (hash-set! type-var-name-table v name)
     v))
 
@@ -1228,13 +1397,13 @@
 (define (Mu-body* name t)
   (match t
     [(Mu: body)
-     (instantiate (make-F name) body)]))
+     (instantiate-type body (make-F name))]))
 
 ;; unfold : Mu -> Type
 (define/cond-contract (unfold t)
   (Mu? . -> . Type?)
   (match t
-    [(Mu-unsafe: body) (instantiate t body)]
+    [(Mu-unsafe: body) (instantiate-type body t)]
     [t (error 'unfold "not a mu! ~a" t)]))
 
 
@@ -1250,7 +1419,7 @@
 ;;
 (define (Poly* names body #:original-names [orig names])
   (if (null? names) body
-      (let ([v (make-Poly (length names) (abstract-many names body))])
+      (let ([v (make-Poly (length names) (abstract-type body names))])
         (hash-set! type-var-name-table v orig)
         v)))
 
@@ -1260,12 +1429,12 @@
     [(Poly: n body)
      (unless (= (length names) n)
        (int-err "Wrong number of names: expected ~a got ~a" n (length names)))
-     (instantiate-many (map make-F names) body)]))
+     (instantiate-type body (map make-F names))]))
 
 ;; PolyDots 'smart' constructor
 (define (PolyDots* names body)
   (if (null? names) body
-      (let ([v (make-PolyDots (length names) (abstract-many names body))])
+      (let ([v (make-PolyDots (length names) (abstract-type body names))])
         (hash-set! type-var-name-table v names)
         v)))
 
@@ -1275,7 +1444,7 @@
     [(PolyDots: n body)
      (unless (= (length names) n)
        (int-err "Wrong number of names: expected ~a got ~a" n (length names)))
-     (instantiate-many (map make-F names) body)]))
+     (instantiate-type body (map make-F names))]))
 
 
 ;; PolyRow 'smart' constructor
@@ -1285,7 +1454,7 @@
 ;; a time. This may change in the future.
 ;;
 (define (PolyRow* names constraints body #:original-names [orig names])
-  (let ([v (make-PolyRow constraints (abstract-many names body))])
+  (let ([v (make-PolyRow constraints (abstract-type body names))])
     (hash-set! type-var-name-table v orig)
     v))
 
@@ -1293,7 +1462,7 @@
 (define (PolyRow-body* names t)
   (match t
     [(PolyRow: constraints body)
-     (instantiate-many (map make-F names) body)]))
+     (instantiate-type body (map make-F names))]))
 
 
 ;;***************************************************************
@@ -1549,110 +1718,3 @@
     (syntax-parse stx
       [(_) #'(Name: _ _ #t)]
       [(_ name-pat) #'(Name: name-pat _ #t)])))
-
-
-;;***************************************************************
-;; Intersection/Refinement related tools
-;;***************************************************************
-
-
-;; inc-lvl
-;; (cons nat nat) -> (cons nat nat)
-;; DeBruijn indexes are represented as a pair of naturals.
-;; This function increments the 'lvl' field of such an index.
-(define (inc-lvl x)
-  (match x
-    [(cons lvl arg) (cons (add1 lvl) arg)]
-    [_ x]))
-
-;; inc-lvls
-;; This function increments the 'lvl' field in all of the targets
-;; and objects of substitution (see 'inc-lvl' above)
-;; (side note: there is a similar but _different_ version
-;; of this function in tc-subst.rkt)
-(define (inc-lvls targets)
-  (for/list ([tgt (in-list targets)])
-    (match tgt
-      [(cons nm1 (Path: flds nm2))
-       (cons (inc-lvl nm1) (make-Path flds (inc-lvl nm2)))]
-      [(cons nm1 rst)
-       (cons (inc-lvl nm1) rst)])))
-
-
-;; name substitution -- like subst-rep in
-;; tc-subst but much simpler
-(define/cond-contract (subst-names rep targets)
-  (-> Rep? (listof (cons/c name-ref/c OptObject?)) Rep?)
-  (define (rec/inc-lvl rep)
-    (subst-names rep (inc-lvls targets)))
-  (let rec ([rep rep])
-    (match rep
-      ;; Functions
-      ;; increment the level of the substituted object
-      [(arr: dom rng rest drest kws)
-       (make-arr (map rec dom)
-                 (rec/inc-lvl rng)
-                 (and rest (rec rest))
-                 (and drest (cons (rec (car drest)) (cdr drest)))
-                 (map rec kws))]
-      ;; Refinement types e.g. {x ∈ τ | ψ(x)}
-      ;; increment the level of the substituted object
-      [(Intersection: ts p _) (-refine
-                               (for/fold ([res Univ])
-                                         ([t (in-list ts)])
-                                 (intersect res (rec t)))
-                               (rec/inc-lvl p))]
-      [(Path: flds nm)
-       (let ([flds (map rec flds)])
-         (cond
-           [(assoc nm targets name-ref=?)
-            => (match-lambda
-                 [(cons _ (Path: flds* nm*)) (make-Path (append flds flds*) nm*)]
-                 [(cons _ (Empty:)) -empty-obj]
-                 [(cons _ (? LExp? l)) #:when (null? flds) l]
-                 [_ -empty-obj])]
-           [else (make-Path flds nm)]))]
-      [_ (Rep-fmap rep rec)])))
-
-(define (abstract-names rep ids)
-  (define sub (for/list ([id (in-list ids)]
-                         [idx (in-range (length ids))])
-                (cons id (-id-path (cons 0 idx)))))
-  (subst-names rep sub))
-
-
-(define (Intersection-prop* obj t)
-  (define p (Intersection-prop t))
-  (and p (subst-names p (list (cons (cons 0 0) obj)))))
-
-
-;; given the fact that 'obj' is of type 'type',
-;; look inside of type trying to learn
-;; more info about obj
-(define (extract-props obj type)
-  (cond
-    [(Empty? obj) '()]
-    [else
-     (define props '())
-     (let extract! ([rep type]
-                    [obj obj])
-       (match rep
-         [(== -Zero)
-          #:when (with-linear-integer-arithmetic?)
-          (set! props (cons (-eq obj (-lexp 0)) props))]
-         [(== -One)
-          #:when (with-linear-integer-arithmetic?)
-          (set! props (cons (-eq obj (-lexp 1)) props))]
-         [(Pair: t1 t2) (extract! t1 (-car-of obj))
-                        (extract! t2 (-cdr-of obj))]
-         [(Refine-obj: obj t prop)
-          (set! props (cons prop props))
-          (extract! t obj)]
-         [(HeterogeneousVector: ts)
-          #:when (with-linear-integer-arithmetic?)
-          (set! props (cons (-eq (-vec-len-of obj) (-lexp (length ts)))
-                            props))]
-         [(Intersection: ts _ _) (for ([t (in-list ts)])
-                                   (extract! t obj))]
-         [_ (void)]))
-     props]))
diff --git a/typed-racket-lib/typed-racket/typecheck/check-below.rkt b/typed-racket-lib/typed-racket/typecheck/check-below.rkt
index 53a8a401..597b6f36 100644
--- a/typed-racket-lib/typed-racket/typecheck/check-below.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/check-below.rkt
@@ -36,10 +36,11 @@
   (define (value-string ty)
     (match ty
       [(tc-result1: _) "1 value"]
-      [(tc-results: ts) (~a (length ts) " values")]
+      [(tc-results: tcrs #f) (~a (length tcrs) " values")]
       ;; TODO simplify this case
-      [(tc-results: ts _ _ dty _) (~a (length ts) " " (if (= (length ts) 1) "value" "values")
-                                      " and `" dty " ...'")]
+      [(tc-results: tcrs (RestDots: dty _))
+       (~a (length tcrs) " " (if (= (length tcrs) 1) "value" "values")
+           " and `" dty " ...'")]
       [(tc-any-results: _) "unknown number"]))
   (type-mismatch
     (value-string expected) (value-string actual)
@@ -73,6 +74,13 @@
   (define (prop-better? p1 p2)
     (or (not p2)
         (implies? p1 p2)))
+  (define (RestDots-better? rdots1 rdots2)
+    (match* (rdots1 rdots2)
+      [(rd rd) #t]
+      [((RestDots: dty1 dbound)
+        (RestDots: dty2 dbound))
+       (subtype dty1 dty2)]
+      [(_ _) #f]))
 
   (match* (tr1 expected)
     ;; This case has to be first so that bottom (exceptions, etc.) can be allowed in cases
@@ -84,15 +92,18 @@
     [((tc-any-results: p1) (tc-any-results: p2))
      (unless (prop-better? p1 p2)
        (type-mismatch p2 p1 "mismatch in proposition"))
-     (tc-any-results (fix-props p2 p1))]
+     (-tc-any-results (fix-props p2 p1))]
 
-    [((or (tc-results: _ (list (PropSet: ps+ ps-) ...) _)
-          (tc-results: _ (list (PropSet: ps+ ps-) ...) _ _ _))
+    [((tc-results: tcrs _)
       (tc-any-results: p2))
-     (define merged-prop (apply -and (map -or ps+ ps-)))
+     (define merged-prop
+       (apply -and
+              (map (match-lambda
+                     [(tc-result: _ (PropSet: p+ p-) _) (-or p+ p-)])
+                   tcrs)))
      (unless (prop-better? merged-prop p2)
        (type-mismatch p2 merged-prop "mismatch in proposition"))
-     (tc-any-results (fix-props p2 merged-prop))]
+     (-tc-any-results (fix-props p2 merged-prop))]
 
 
     [((tc-result1: t1 p1 o1) (tc-result1: t2 p2 o2))
@@ -113,66 +124,47 @@
      (ret t2 (fix-props p2 p1) (fix-object o2 o1))]
 
     ;; case where expected is like (Values a ... a) but got something else
-    [((tc-results: t1 p1 o1) (tc-results: t2 p2 o2 dty dbound))
+    [((tc-results: _ #f) (tc-results: _ (? RestDots?)))
      (value-mismatch expected tr1)
      (fix-results expected)]
 
     ;; case where you have (Values a ... a) but expected something else
-    [((tc-results: t1 p1 o1 dty dbound) (tc-results: t2 p2 o2))
+    [((tc-results: _ (? RestDots?)) (tc-results: _ #f))
      (value-mismatch expected tr1)
      (fix-results expected)]
 
-    [((tc-results: t1 p1 o1 dty1 dbound)
-      (tc-results: t2 (list (or #f (PropSet: (TrueProp:) (TrueProp:))) ...)
-                   (list (or #f (Empty:)) ...) dty2 dbound))
+    ;; case where both have no '...', or both have '...'
+    ;; NOTE: we ignore the propsets and objects... not sure
+    ;;       why---maybe there's an assumption that users
+    ;;       can't specify props/objects for multiple values?
+    ;;       seems like we should add some checks to this doesn't
+    ;;       turn into an error in the future that we can't fix w/o
+    ;;       breaking programs that relied on it being broken.
+    [((tc-results: tcrs1 db1)
+      (tc-results: tcrs2 db2))
      (cond
-       [(= (length t1) (length t2))
-        (unless (andmap subtype t1 t2 o1)
-          (expected-but-got (stringify t2) (stringify t1)))
-        (unless (subtype dty1 dty2)
-          (type-mismatch dty2 dty1 "mismatch in ... argument"))]
+       [(= (length tcrs1) (length tcrs2))
+        (unless (andmap (match-lambda**
+                         [((tc-result: t1 ps1 o1)
+                           (tc-result: t2 ps2 o2))
+                          (and (subtype t1 t2 o1)
+                               (prop-set-better? ps1 ps2)
+                               (object-better? o1 o2))])
+                        tcrs1
+                        tcrs2)
+          (expected-but-got (stringify (map tc-result-t tcrs1))
+                            (stringify (map tc-result-t tcrs2))))
+        (match* (db1 db2)
+          [((RestDots: dty1 dbound1)
+            (RestDots: dty2 dbound2))
+           #:when (not (and (eq? dbound1 dbound2)
+                            (subtype dty1 dty2)))
+           (type-mismatch dty2 dty1 "mismatch in ... argument")]
+          [(_ _) (void)])]
        [else
         (value-mismatch expected tr1)])
      (fix-results expected)]
 
-    [((tc-results: t1 p1 o1 dty1 dbound) (tc-results: t2 p2 o2 dty2 dbound))
-     (cond
-       [(= (length t1) (length t2))
-        (unless (andmap subtype t1 t2 o1)
-          (expected-but-got (stringify t2) (stringify t1)))
-        (unless (subtype dty1 dty2)
-          (type-mismatch dty2 dty1 "mismatch in ... argument"))]
-       [else
-        (value-mismatch expected tr1)])
-     (fix-results expected)]
-
-    [((tc-results: t1 p1 o1)
-      (tc-results: t2 (list (or #f (PropSet: (TrueProp:) (TrueProp:))) ...)
-                   (list (or #f (Empty:)) ...)))
-     (unless (= (length t1) (length t2))
-       (value-mismatch expected tr1))
-     (unless (for/and ([t (in-list t1)]
-                       [s (in-list t2)]
-                       [o (in-list o1)])
-               (subtype t s o))
-       (expected-but-got (stringify t2) (stringify t1)))
-     (fix-results expected)]
-
-    [((tc-results: t1 fs os) (tc-results: t2 fs os))
-     (unless (= (length t1) (length t2))
-       (value-mismatch expected tr1))
-     (unless (for/and ([t (in-list t1)]
-                       [s (in-list t2)]
-                       [o (in-list os)])
-               (subtype t s o))
-       (expected-but-got (stringify t2) (stringify t1)))
-     (fix-results expected)]
-
-    [((tc-results: t1 p1 o1) (tc-results: t2 p2 o2))
-     #:when (not (= (length t1) (length t2)))
-     (value-mismatch expected tr1)
-     (fix-results expected)]
-
     [((tc-any-results: _) (? tc-results?))
      (value-mismatch expected tr1)
      (fix-results expected)]
@@ -181,7 +173,6 @@
      (unless (subtype t1 t2)
        (expected-but-got t2 t1))
      expected]
-    [((tc-results: ts fs os dty dbound) (tc-results: ts* fs* os* dty* dbound*))
-     (int-err "dotted types with different bounds/propositions/objects in check-below nyi: ~a ~a" tr1 expected)]
+    
     [(a b) (int-err "unexpected input for check-below: ~a ~a" a b)]))
 
diff --git a/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt b/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt
index 488f6ba4..5bd1832d 100644
--- a/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt
@@ -1116,9 +1116,7 @@
        ;; so that it has the right environment. An earlier approach did
        ;; check this only in the synthesis stage, but caused some regressions.
        (define temp-names (syntax->list #'(names ...)))
-       (define init-types
-         (match (tc-expr #'val-expr)
-           [(tc-results: xs ) xs]))
+       (define init-types (tc-results-ts (tc-expr #'val-expr)))
        (unless (= (length temp-names) (length init-types))
          (tc-error/expr "wrong number of values: expected ~a but got ~a"
                         (length temp-names) (length init-types)))
@@ -1136,8 +1134,7 @@
 (define (setter->type id)
   (define f-type (lookup-id-type/lexical id))
   (match f-type
-    [(Function: (list (arr: (list _ type) _ _ _ _)))
-     type]
+    [(Fun: (list (Arrow: (list _ t) _ _ _))) t]
     [#f (int-err "setter->type ~a" (syntax-e id))]))
 
 ;; check-init-arg : Id Type Syntax -> Void
@@ -1152,8 +1149,7 @@
            (define type
              (tc-expr/check/t init-val (ret (->* null init-type))))
            (match type
-             [(Function: (list (arr: _ (Values: (list (Result: result _ _)))
-                                     _ _ _)))
+             [(Fun: (list (Arrow: _ _ _ (Values: (list (Result: result _ _))))))
               (check-below result init-type)]
              [_ (int-err "unexpected init value ~a"
                          (syntax->datum init-val))])]
@@ -1204,7 +1200,7 @@
        (define init-types
          ;; this gets re-checked later, so don't throw any errors yet
          (match (tc-expr/check? #'initial-values #f)
-           [(tc-results: xs ) xs]
+           [(? tc-results? tcrs) (tc-results-ts tcrs)]
            ;; We have to return something here so use the most conservative type
            [#f (make-list (length field-names) Univ)]))
        (for ([name (in-list field-names)]
@@ -1586,12 +1582,13 @@
 ;; Fix up a method's arity from a regular function type
 (define (function->method type self-type)
   (match type
-    [(Function: (list arrs ...))
-     (define fixed-arrs
-       (for/list ([arr arrs])
-         (match-define (arr: doms rng rest drest kws) arr)
-         (make-arr (cons self-type doms) rng rest drest kws)))
-     (make-Function fixed-arrs)]
+    [(Fun: arrows)
+     (define fixed-arrows
+       (map (match-lambda
+              [(Arrow: dom rst kws rng)
+               (make-Arrow (cons self-type dom) rst kws rng)])
+            arrows))
+     (make-Fun fixed-arrows)]
     [(Poly-names: ns body)
      (make-Poly ns (function->method body self-type))]
     [(PolyDots-names: ns body)
@@ -1604,12 +1601,13 @@
 ;; Turn a "real" method type back into a function type
 (define (method->function type)
   (match type
-    [(Function: (list arrs ...))
-     (define fixed-arrs
-       (for/list ([arr arrs])
-         (match-define (arr: doms rng rest drest kws) arr)
-         (make-arr (cdr doms) rng rest drest kws)))
-     (make-Function fixed-arrs)]
+    [(Fun: arrows)
+     (define fixed-arrows
+       (map (match-lambda
+              [(Arrow: (cons _ dom) rst kws rng)
+               (make-Arrow dom rst kws rng)])
+            arrows))
+     (make-Fun fixed-arrows)]
     [(Poly-names: ns body)
      (make-Poly ns (method->function body))]
     [(PolyDots-names: ns body)
diff --git a/typed-racket-lib/typed-racket/typecheck/check-subforms-unit.rkt b/typed-racket-lib/typed-racket/typecheck/check-subforms-unit.rkt
index a8de8216..59ec29fa 100644
--- a/typed-racket-lib/typed-racket/typecheck/check-subforms-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/check-subforms-unit.rkt
@@ -44,14 +44,24 @@
   ;; The result of applying the function to a single argument of the type of its first argument.
   ;; Is used when checking forms like with-handlers, for example.
   (define (get-range-result stx t prop-type)
-    (let loop ((t t))
+    (let loop ([t t])
       (match t
-        [(Function: (list _ ... (arr: (list arg1) _ _ #f (list (Keyword: _ _ #f) ...)) _ ...))
+        [(Fun: (list _ ...
+                     (Arrow: (list arg1)
+                             (not (? RestDots?))
+                             (list (Keyword: _ _ #f) ...)
+                             _ )
+                     _ ...))
          #:when (subtype prop-type arg1)
          (tc/funapp #'here #'(here) t (list (ret arg1)) #f)]
-        [(Function: (list _ ... (arr: '() _ (? values rest) #f (list (Keyword: _ _ #f) ...)) _ ...))
-         #:when (subtype prop-type rest)
-         (tc/funapp #'here #'(here) t (list (ret rest)) #f)]
+        [(Fun: (list _ ...
+                     (Arrow: (list)
+                             (? Type? rst)
+                             (list (Keyword: _ _ #f) ...)
+                             _ )
+                     _ ...))
+         #:when (subtype prop-type rst)
+         (tc/funapp #'here #'(here) t (list (ret rst)) #f)]
         [(? resolvable? t)
          (loop (resolve t))]
         [(or (Poly: ns _) (PolyDots: (list ns ... _) _))
diff --git a/typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt b/typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt
index e4e61386..2d02d598 100644
--- a/typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt
@@ -735,7 +735,10 @@
                                        check-exports-thunk))
          (define invoke-type
            (match res
-             [(tc-results: tps) (-values tps)]))
+             [(tc-results: tcrs _)
+              (make-Values
+               (for/list ([tcr (in-list tcrs)])
+                 (-result (tc-result-t tcr))))]))
          (-unit import-signatures
                 export-signatures
                 init-depend-signatures
diff --git a/typed-racket-lib/typed-racket/typecheck/possible-domains.rkt b/typed-racket-lib/typed-racket/typecheck/possible-domains.rkt
index 858fd426..b2640348 100644
--- a/typed-racket-lib/typed-racket/typecheck/possible-domains.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/possible-domains.rkt
@@ -40,7 +40,7 @@
 ;; of domains that would *satisfy* the expected type, e.g. for the :query-type
 ;; forms.
 ;; TODO separating pruning and collapsing into separate functions may be nicer
-(define (possible-domains doms rests drests rngs expected [permissive? #t])
+(define (possible-domains doms rests rngs expected [permissive? #t])
 
   ;; is fun-ty subsumed by a function type in others?
   (define (is-subsumed-in? fun-ty others)
@@ -60,7 +60,7 @@
         (eq? expected-ty #t) ; expected is tc-anyresults, anything is fine
         (and expected-ty ; not some unknown expected tc-result
              (match fun-ty
-               [(Function: (list (arr: _ rng _ _ _)))
+               [(Fun: (list (Arrow: _ _ _ rng)))
                 (let ([rng (match rng
                              [(Values: (list (Result: t _ _)))
                               t]
@@ -69,19 +69,20 @@
                              [_ #f])])
                   (and rng (subtype rng expected-ty)))]))))
 
-  (define orig (map list doms rngs rests drests))
+  (define orig (map list doms rngs rests))
 
   (define cases
-    (map (compose make-Function list make-arr)
+    (map (compose make-Fun list make-Arrow)
          doms
+         rests
+         (make-list (length doms) null)
          (map (match-lambda ; strip props
-               [(AnyValues: f) (-AnyValues -tt)]
-               [(Values: (list (Result: t _ _) ...))
-                (-values t)]
-               [(ValuesDots: (list (Result: t _ _) ...) _ _)
-                (-values t)])
-              rngs)
-         rests drests (make-list (length doms) null)))
+                [(AnyValues: f) (-AnyValues -tt)]
+                [(Values: (list (Result: t _ _) ...))
+                 (-values t)]
+                [(ValuesDots: (list (Result: t _ _) ...) _ _)
+                 (-values t)])
+              rngs)))
 
   ;; iterate in lock step over the function types we analyze and the parts
   ;; that we will need to print the error message, to make sure we throw
@@ -112,10 +113,11 @@
   ;; function types with a return type of any then test for subtyping
   (define fun-tys-ret-any
     (map (match-lambda
-          [(Function: (list (arr: dom _ rest drest _)))
-           (make-Function (list (make-arr dom
-                                          (-values (list Univ))
-                                          rest drest null)))])
+          [(Fun: (list (Arrow: dom rest _ _)))
+           (make-Fun (list (make-Arrow dom
+                                       rest
+                                       null
+                                       (-values (list Univ)))))])
          candidates))
 
   ;; Heuristic: often, the last case in the definition (first at this
@@ -142,17 +144,17 @@
 
          (call-with-values
            (λ ()
-             (for/lists (_1 _2 _3 _4) ([xs (in-list (reverse parts-res))])
-               (values (car xs) (cadr xs) (caddr xs) (cadddr xs))))
+             (for/lists (_1 _2 _3) ([xs (in-list (reverse parts-res))])
+               (values (car xs) (cadr xs) (caddr xs))))
            list)]))
 
 ;; Wrapper over possible-domains that works on types.
 (define (cleanup-type t [expected #f] [permissive? #t])
   (match t
     ;; function type, prune if possible.
-    [(Function/arrs: doms rngs rests drests kws)
-     (match-let ([(list pdoms rngs rests drests)
-                  (possible-domains doms rests drests rngs
+    [(Fun: (list (Arrow: doms rests _ rngs) ...))
+     (match-let ([(list pdoms rngs rests)
+                  (possible-domains doms rests rngs
                                     (and expected (ret expected))
                                     permissive?)])
        (if (= (length pdoms) (length doms))
@@ -161,7 +163,10 @@
            ;;  the original, which may confuse `:print-type''s pruning detection)
            t
            ;; pruning helped, return pruned type
-           (make-Function (map make-arr
-                               pdoms rngs rests drests (make-list (length pdoms) null)))))]
+           (make-Fun (map make-Arrow
+                          pdoms
+                          rests
+                          (make-list (length pdoms) null)
+                          rngs))))]
     ;; not a function type. keep as is.
     [_ t]))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
index 0432d250..bc3c9121 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
@@ -14,16 +14,17 @@
 
 (provide/cond-contract
   [tc/funapp1
-    ((syntax? stx-list? arr? (listof tc-results/c) (or/c #f tc-results/c))
+    ((syntax? stx-list? Arrow? (listof tc-results/c) (or/c #f tc-results/c))
      (#:check boolean?)
      . ->* . full-tc-results/c)])
 (define (tc/funapp1 f-stx args-stx ftype0 argtys expected #:check [check? #t])
   ;; update tooltip-table with inferred function type
-  (add-typeof-expr f-stx (ret (make-Function (list ftype0))))
+  (add-typeof-expr f-stx (ret (make-Fun (list ftype0))))
   (match* (ftype0 argtys)
     ;; we check that all kw args are optional
-    [((arr: dom rng rest #f (and kws (list (Keyword: _ _ #f) ...)))
-      (list (tc-result1: t-a phi-a o-a) ...))
+    [((Arrow: dom rest (and kws (list (Keyword: _ _ #f) ...)) rng)
+      (list (tc-result1: t-a _ o-a) ...))
+     #:when (not (RestDots? rest))
      
      (when check?
        (cond [(and (not rest) (not (= (length dom) (length t-a))))
@@ -42,65 +43,62 @@
              [a (in-syntax args-stx)]
              [arg-t (in-list t-a)])
          (parameterize ([current-orig-stx a]) (check-below arg-t dom-t))))
-     (let* ([dom-count (length dom)])
-       ;; Currently do nothing with rest args and keyword args as there are no support for them in
-       ;; objects yet.
+     (let ([dom-count (length dom)])
+       ;; Currently do nothing with rest args and keyword args
+       ;; as there are no support for them in objects yet.
        (let-values
-           ([(o-a t-a) (for/lists (os ts)
-                         ([_ (in-range dom-count)]
-                          [oa (in-list/rest o-a -empty-obj)]
-                          [ta (in-list/rest t-a Univ)])
-                         (values oa ta))])
-           (values->tc-results rng o-a t-a)))]
+           ([(o-a t-a) (if (= dom-count (length t-a))
+                           (values o-a t-a)
+                           (for/lists (os ts)
+                             ([_ (in-range dom-count)]
+                              [oa (in-list/rest o-a -empty-obj)]
+                              [ta (in-list/rest t-a Univ)])
+                             (values oa ta)))])
+         (values->tc-results rng o-a t-a)))]
     ;; this case should only match if the function type has mandatory keywords
     ;; but no keywords were provided in the application
-    [((arr: _ _ _ _
-            ;; at least one mandatory keyword
-            (app (λ (kws)
-                   (for/or ([keyword (in-list kws)])
-                     (match keyword
-                       [(Keyword: kw _ #t) kw]
-                       [_ #f])))
-                 (? values req-kw))) _)
+    [((Arrow: _ _ kws _) _)
+     #:when (ormap Keyword-required? kws)
      (when check?
        (tc-error/fields "could not apply function"
                         #:more "a required keyword was not supplied"
-                        "missing keyword" req-kw))]
-    [((arr: _ _ _ drest '()) _)
+                        "missing keyword"
+                        (car (filter Keyword-required? kws))))]
+    [((Arrow: _ (? RestDots? drest) '() _) _)
      (int-err "funapp with drest args ~a ~a NYI" drest argtys)]
-    [((arr: _ _ _ _ kws) _)
+    [((Arrow: _ _ kws _) _)
      (int-err "funapp with keyword args ~a NYI" kws)]))
 
 
 (define (make-printable t)
   (match t
     [(tc-result1: t) (cleanup-type t)]
-    [(or (tc-results: ts)
-         (tc-results: ts _ _ _ _))
-     (-values (map cleanup-type ts))]
-    [(tc-any-results: f) (-AnyValues -tt)]
+    [(tc-results: tcrs _)
+     (-values (for/list ([tcr (in-list tcrs)])
+                (cleanup-type (tc-result-t tcr))))]
+    [(tc-any-results: _) (-AnyValues -tt)]
     [_ t]))
 
-(define (stringify-domain dom rst drst [rng #f])
+(define (stringify-domain dom rst [rng #f])
   (let ([doms-string (if (null? dom) "" (string-append (stringify (map make-printable dom)) " "))]
         [rng-string (if rng (format " -> ~a" rng) "")])
-    (cond [drst
-           (format "~a~a ... ~a~a" doms-string (car drst) (cdr drst) rng-string)]
-          [rst
-           (format "~a~a *~a" doms-string rst rng-string)]
-          [else (string-append (stringify (map make-printable dom)) rng-string)])))
+    (match rst
+      [(RestDots: dty dbound)
+       (format "~a~a ... ~a~a" doms-string dty dbound rng-string)]
+      [rst
+       (format "~a~a *~a" doms-string rst rng-string)]
+      [else (string-append (stringify (map make-printable dom)) rng-string)])))
 
 ;; Generates error messages when operand types don't match operator domains.
 (provide/cond-contract
   [domain-mismatches
-   ((syntax? syntax? Type? (listof (listof Type?)) (listof (or/c #f Type?))
-     (listof (or/c #f (cons/c Type? (or/c natural-number/c symbol?))))
+   ((syntax? syntax? Type? (listof (listof Type?)) (listof (or/c #f Type? RestDots?))
      (listof SomeValues?) (listof tc-results?) (or/c #f Type?) any/c)
     (#:expected (or/c #f tc-results/c)
      #:return tc-results?
      #:msg-thunk (-> string? string?))
     . ->* . tc-results/c)])
-(define (domain-mismatches f-stx args-stx ty doms rests drests rngs arg-tys tail-ty tail-bound
+(define (domain-mismatches f-stx args-stx ty doms rests rngs arg-tys tail-ty tail-bound
                            #:expected [expected #f] #:return [return (ret -Bottom)]
                            #:msg-thunk [msg-thunk (lambda (dom) dom)])
   (define arguments-str
@@ -114,7 +112,10 @@
       #:more (format "~a has type Procedure which cannot be applied"
                      (name->function-str (and (identifier? f-stx) f-stx)))
       #:return return)]
-    [(and (= 1 (length doms)) (not (car rests)) (not (car drests)) (not tail-ty) (not tail-bound))
+    [(and (= 1 (length doms))
+          (not (car rests))
+          (not tail-ty)
+          (not tail-bound))
      (tc-error/expr
       #:return return
       (msg-thunk
@@ -140,7 +141,7 @@
       (msg-thunk
        (string-append
         "Domain: "
-        (stringify-domain (car doms) (car rests) (car drests))
+        (stringify-domain (car doms) (car rests))
         "\nArguments: "
         arguments-str
         "\n"
@@ -153,13 +154,13 @@
      (define nl+spc (if expected "\n       " "\n         "))
      ;; we restrict the domains shown in the error messages to those that
      ;; are useful
-     (match-let ([(list pdoms prngs prests pdrests) (possible-domains doms rests drests rngs expected)])
+     (match-let ([(list pdoms prngs prests) (possible-domains doms rests rngs expected)])
        ;; if we somehow eliminate all the cases (bogus expected type) fall back to showing the
        ;; extra cases
-       (let-values ([(pdoms rngs rests drests)
+       (let-values ([(pdoms rngs rests)
                      (if (null? pdoms)
-                         (values doms rngs rests drests)
-                         (values pdoms prngs prests pdrests))])
+                         (values doms rngs rests)
+                         (values pdoms prngs prests))])
          ;; only use `tc/funapp1` if `tail-ty` was *not* provided
          ;; since it either won't error correctly or produces a poor error
          (cond [(and (not tail-ty)
@@ -174,8 +175,10 @@
                 ;; if we narrowed down the possible cases to a single one, have
                 ;; tc/funapp1 generate a better error message
                 (tc/funapp1 f-stx args-stx
-                            (make-arr (car pdoms) (car rngs)
-                                      (car rests) (car drests) null)
+                            (make-Arrow (car pdoms)
+                                        (car rests)
+                                        null
+                                        (car rngs))
                             arg-tys expected)
                 return]
                [else
@@ -184,8 +187,8 @@
                   (string-append
                    label
                    (stringify (if expected
-                                  (map stringify-domain pdoms rests drests rngs)
-                                  (map stringify-domain pdoms rests drests))
+                                  (map stringify-domain pdoms rests rngs)
+                                  (map stringify-domain pdoms rests))
                               nl+spc)
                    "\nArguments: "
                    arguments-str
@@ -207,13 +210,25 @@
   (match t
     [(or (Poly-names:
           msg-vars
-          (Function/arrs: msg-doms msg-rngs msg-rests msg-drests (list (Keyword: _ _ #f) ...)))
+          (Fun: (list (Arrow: msg-doms
+                              msg-rests
+                              (list (Keyword: _ _ #f) ...)
+                              msg-rngs)
+                      ...)))
          (PolyDots-names:
           msg-vars
-          (Function/arrs: msg-doms msg-rngs msg-rests msg-drests (list (Keyword: _ _ #f) ...)))
+          (Fun: (list (Arrow: msg-doms
+                              msg-rests
+                              (list (Keyword: _ _ #f) ...)
+                              msg-rngs)
+                      ...)))
          (PolyRow-names:
           msg-vars _
-          (Function/arrs: msg-doms msg-rngs msg-rests msg-drests (list (Keyword: _ _ #f) ...))))
+          (Fun: (list (Arrow: msg-doms
+                              msg-rests
+                              (list (Keyword: _ _ #f) ...)
+                              msg-rngs)
+                      ...))))
      (let ([fcn-string (name->function-str name)])
        (if (and (andmap null? msg-doms)
                 (null? argtypes))
@@ -221,7 +236,7 @@
                            "Could not infer types for applying polymorphic "
                            fcn-string
                            "\n"))
-           (domain-mismatches f-stx args-stx t msg-doms msg-rests msg-drests
+           (domain-mismatches f-stx args-stx t msg-doms msg-rests
                               msg-rngs argtypes #f #f #:expected expected
                               #:msg-thunk (lambda (dom)
                                             (string-append
@@ -231,9 +246,16 @@
                                                                (list->seteq msg-vars)))
                                                  (string-append "Type Variables: " (stringify msg-vars) "\n")
                                                  ""))))))]
-    [(or (Poly-names: msg-vars (Function/arrs: msg-doms msg-rngs msg-rests msg-drests kws))
-         (PolyDots-names: msg-vars (Function/arrs: msg-doms msg-rngs msg-rests msg-drests kws))
-         (PolyRow-names: msg-vars _ (Function/arrs: msg-doms msg-rngs msg-rests msg-drests kws)))
+    [(or (Poly-names:
+          msg-vars
+          (Fun: (list (Arrow: msg-doms msg-rests kws msg-rngs) ...)))
+         (PolyDots-names:
+          msg-vars
+          (Fun: (list (Arrow: msg-doms msg-rests kws msg-rngs) ...)))
+         (PolyRow-names:
+          msg-vars
+          _
+          (Fun: (list (Arrow: msg-doms msg-rests kws msg-rngs) ...))))
      (let ([fcn-string (if name
                            (format "function with keywords ~a" (syntax->datum name))
                            "function with keywords")])
@@ -243,7 +265,7 @@
                            "Could not infer types for applying polymorphic "
                            fcn-string
                            "\n"))
-           (domain-mismatches f-stx args-stx t msg-doms msg-rests msg-drests
+           (domain-mismatches f-stx args-stx t msg-doms msg-rests
                               msg-rngs argtypes #f #f #:expected expected
                               #:msg-thunk (lambda (dom)
                                             (string-append
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt
index ef25b4bb..66cb1971 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt
@@ -42,7 +42,7 @@
     (match (tc-expr #'fn)
       [(tc-result1:
         (Poly: vars
-               (Function: (list (and ar (arr: dom rng (and rest #f) (and drest #f) kw-formals))))))
+               (Fun: (list (and ar (Arrow: dom #f kw-formals rng))))))
        (=> fail)
        (unless (set-empty? (fv/list kw-formals))
          (fail))
@@ -53,17 +53,17 @@
             (unless subst (fail))
             (tc-keywords #'form (list (subst-all subst ar))
                          (type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected))])]
-      [(tc-result1: (Function: arities))
-       (tc-keywords #'(#%plain-app . form) arities (type->list (tc-expr/t #'kws))
+      [(tc-result1: (Fun: arrows))
+       (tc-keywords #'(#%plain-app . form) arrows (type->list (tc-expr/t #'kws))
                     #'kw-arg-list #'pos-args expected)]
-      [(tc-result1: (Poly: _ (Function: _)))
+      [(tc-result1: (Poly: _ (Fun: _)))
        (tc-error/expr "Inference for polymorphic keyword functions not supported")]
       [(tc-result1: t)
        (tc-error/expr "Cannot apply expression of type ~a, since it is not a function type" t)])))
 
 (define (tc-keywords/internal arity kws kw-args error?)
   (match arity
-    [(arr: dom rng rest #f ktys)
+    [(Arrow: dom (not (? RestDots?)) ktys rng)
      ;; assumes that everything is in sorted order
      (let loop ([actual-kws kws]
                 [actuals (stx-map tc-expr/t kw-args)]
@@ -101,24 +101,25 @@
                 [else ;; otherwise, ignore this formal param, and continue
                  (loop actual-kws actuals form-rest)])]))]))
 
-(define (tc-keywords form arities kws kw-args pos-args expected)
-  (match arities
-    [(list (and a (arr: dom rng rest #f ktys)))
+(define (tc-keywords form arrows kws kw-args pos-args expected)
+  (match arrows
+    [(list (and a (Arrow: dom (and rst (not (? RestDots?))) ktys rng)))
      (tc-keywords/internal a kws kw-args #t)
      (tc/funapp (car (syntax-e form)) kw-args
-                (->* dom rest rng)
+                (->* dom rst rng)
                 (stx-map tc-expr pos-args) expected)]
-    [(list (and a (arr: doms rngs rests (and drests #f) ktyss)) ...)
-     (let ([new-arities
-            (for/list ([a (in-list arities)]
-                       ;; find all the arities where the keywords match
+    [(list (and a (Arrow: doms (and rsts (not (? RestDots?))) _ rngs)) ...)
+     (let ([new-arrows
+            (for/list ([a (in-list arrows)]
+                       ;; find all the arrows where the keywords match
                        #:when (tc-keywords/internal a kws kw-args #f))
               (match a
-                [(arr: dom rng rest #f ktys) (make-arr* dom rng #:rest rest)]))])
-       (if (null? new-arities)
+                [(Arrow: dom (and rst (not (? RestDots?))) ktys rng)
+                 (make-Arrow dom rst '() rng)]))])
+       (if (null? new-arrows)
            (domain-mismatches
             (car (syntax-e form)) (cdr (syntax-e form))
-            (make-Function arities) doms rests drests rngs
+            (make-Fun arrows) doms rsts rngs
             (stx-map tc-expr pos-args)
             #f #f #:expected expected
             #:msg-thunk
@@ -126,7 +127,7 @@
               (string-append "No function domains matched in function application:\n"
                              dom)))
            (tc/funapp (car (syntax-e form)) kw-args
-                      (make-Function new-arities)
+                      (make-Fun new-arrows)
                       (stx-map tc-expr pos-args) expected)))]))
 
 (define (type->list t)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-list.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-list.rkt
index 58d5e6d9..85936634 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-list.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-list.rkt
@@ -56,7 +56,7 @@
                 (tc/funapp #'f #'(arg0 arg ...) f-type (cons (ret t0) (map ret t))
                            expected-elem-type))
          [(tc-result1: t) (ret (make-ListDots t bound0))]
-         [(tc-results: ts)
+         [(tc-results: (list (tc-result: ts)) _)
           (tc-error/expr "Expected one value, but got ~a" (-values ts))])]
       ;; otherwise, if it's not a ListDots, defer to the regular function typechecking
       ;; TODO fix double typechecking
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 09844f1c..2fc665be 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
@@ -47,25 +47,30 @@
 
 
 ;; TODO: handle drest, and props/objects
-(define (arr-matches? arr args)
+(define (arrow-matches? arr args)
   (match arr
-    [(arr: domain
-           (Values: (list (Result: v
-                                   (PropSet: (TrueProp:) (TrueProp:))
-                                   (Empty:)) ...))
-           rest #f (list (Keyword: _ _ #f) ...))
+    [(Arrow: domain
+             (and rst (not (? RestDots?)))
+             (list (Keyword: _ _ #f) ...)
+             (Values: (list (Result: v
+                                     (PropSet: (TrueProp:) (TrueProp:))
+                                     (Empty:))
+                            ...)))
      (cond
-       [(< (length domain) (length args)) rest]
+       [(< (length domain) (length args)) rst]
        [(= (length domain) (length args)) #t]
        [else #f])]
     [_ #f]))
 
 (define (has-props? arr)
   (match arr
-    [(arr: _ (Values: (list (Result: v
+    [(Arrow: _
+             _
+             (list (Keyword: _ _ #f) ...)
+             (Values: (list (Result: v
                                      (PropSet: (TrueProp:) (TrueProp:))
-                                     (Empty:)) ...))
-           _ _ (list (Keyword: _ _ #f) ...)) #f]
+                                     (Empty:)) ...)))
+     #f]
     [else #t]))
 
 
@@ -75,31 +80,31 @@
      (let* ([f-ty (tc-expr/t #'f)]
             [args* (syntax->list #'args)])
        (define (matching-arities arrs)
-         (for/list ([arr (in-list arrs)] #:when (arr-matches? arr args*)) arr))
+         (for/list ([arr (in-list arrs)] #:when (arrow-matches? arr args*)) arr))
        (define (has-drest/props? arrs)
          (for/or ([arr (in-list arrs)])
-           (or (has-props? arr) (arr-drest arr))))
+           (or (has-props? arr)
+               (RestDots? (Arrow-rst arr)))))
 
        (define arg-tys
          (match f-ty
-           [(Function: (? has-drest/props?))
+           [(Fun: (? has-drest/props?))
             (map single-value args*)]
-           [(Function:
-              (app matching-arities
-                (list (arr: doms _ rests _ _) ..1)))
+           [(Fun: (app matching-arities
+                       (list (Arrow: doms rsts _ _) ..1)))
             ;; if for a particular argument, all of the domain types
-            ;; agree for each arr type in the case->, then we use
-            ;; that type to check against
+            ;; agree for each arrow type in the case->, then we use
+            ;; that type to check the argument expression against
             (for/list ([arg-stx (in-list args*)]
                        [arg-idx (in-naturals)])
               (define dom-ty (list-ref/default (car doms)
                                                arg-idx
-                                               (car rests)))
+                                               (car rsts)))
               (cond
                 [(for/and ([dom (in-list doms)]
-                           [rest (in-list rests)])
+                           [rst (in-list rsts)])
                    (equal? dom-ty
-                           (list-ref/default dom arg-idx rest)))
+                           (list-ref/default dom arg-idx rst)))
                  (tc-expr/check arg-stx (ret dom-ty))]
                 [else (single-value arg-stx)]))]
            [_ (map single-value args*)]))
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 5625aaa3..4601a8fd 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
@@ -20,9 +20,12 @@
   ;; call-with-values
   (pattern (call-with-values prod con)
     (match (tc/funapp #'prod #'() (tc-expr/t #'prod) null #f)
-      [(tc-results: ts fs os)
-       (tc/funapp #'con #'(prod) (tc-expr/t #'con) (map ret ts fs os) expected)]
-      [(tc-results: ts fs os drest dbound)
+      [(tc-results: tcrs #f)
+       (tc/funapp #'con #'(prod) (tc-expr/t #'con)
+                  (for/list ([tcr (in-list tcrs)])
+                    (-tc-results (list tcr) #f))
+                  expected)]
+      [(tc-results: _ (? RestDots?))
        (tc-error/expr "`call-with-values` with ... is not supported")]
       [(tc-any-results: _)
        (tc/app-regular this-syntax expected)]))
@@ -33,26 +36,16 @@
      [(or #f (tc-any-results: _)) (single-value #'arg)]
      [(tc-result1: tp)
       (single-value #'arg expected)]
-     [(tc-results: ts)
-      (single-value #'arg)] ;Type check the argument, to find other errors
-     ;; match polydots case and error
-     [(tc-results: ts _ _ dty dbound)
-      (single-value #'arg)]))
+      ;; Type check the argument, to find other errors
+     [_ (single-value #'arg)]))
   ;; handle `values' specially
   (pattern (values . args)
     (match expected
-      [(tc-results: ets efs eos)
-       (match-let ([(list (tc-result1: ts fs os) ...)
-                    (for/list
-                      ([arg (in-syntax #'args)]
-                       [et (in-sequences (in-list ets) (in-cycle (in-value #f)))]
-                       [ef (in-sequences (in-list efs) (in-cycle (in-value #f)))]
-                       [eo (in-sequences (in-list eos) (in-cycle (in-value #f)))])
-                      (if et
-                          (single-value arg (ret et ef eo))
-                          (single-value arg)))])
-         (ret ts fs os))]
-      [_ (match-let ([(list (tc-result1: ts fs os) ...)
-                      (for/list ([arg (in-syntax #'args)])
-                        (single-value arg))])
-           (ret ts fs os))])))
+      [(or (tc-results: tcrs #f)
+           (bind tcrs '()))
+       (-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)])))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt b/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt
index 1fd4e72c..7b81aff6 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt
@@ -45,8 +45,9 @@
   (define (failure)
     (match f-ty
       [(tc-result1:
-         (and t (AnyPoly-names: _ _ (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1)))))
-       (domain-mismatches f args t doms rests drests rngs arg-tres full-tail-ty #f
+         (and t (AnyPoly-names: _ _
+                                (Fun: (list (Arrow: doms  rests (list (Keyword: _ _ #f) ...) rngs) ..1)))))
+       (domain-mismatches f args t doms rests rngs arg-tres full-tail-ty #f
                           #:msg-thunk (lambda (dom)
                                         (string-append
                                          "Bad arguments to function in `apply':\n"
@@ -54,31 +55,36 @@
 
   (match f-ty
     ;; apply of a simple function or polymorphic function
-    [(tc-result1: (AnyPoly: vars dotted-vars (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1))))
+    [(tc-result1:
+      (AnyPoly: vars dotted-vars (Fun: (list arrows ..1))))
+     #:when (not (for*/or ([a (in-list arrows)]
+                           [kws (in-value (Arrow-kws a))])
+                   (ormap Keyword-required? kws)))
      (or
-       (for/or ([domain (in-list doms)]
-                [range (in-list rngs)]
-                [rest (in-list rests)]
-                [drest (in-list drests)])
-         ;; Takes a possible substitution and comuptes the substituted range type if it is not #f
-         (define (finish substitution)
-           (and substitution (do-ret (subst-all substitution range))))
+      (for/or ([arrow (in-list arrows)])
+        (match arrow
+          [(Arrow: domain rst _ rng)
+           ;; Takes a possible substitution and comuptes
+           ;; the substituted range type if it is not #f
+           (define (finish substitution)
+             (and substitution (do-ret (subst-all substitution rng))))
 
-         (finish
-           (infer vars dotted-vars
-                  (list (-Tuple* arg-tys full-tail-ty))
-                  (list (-Tuple* domain
-                                 (cond
-                                   ;; the actual work, when we have a * function
-                                   [rest (make-Listof rest)]
-                                   ;; ... function
-                                   [drest (make-ListDots (car drest) (cdr drest))]
-                                   ;; the function has no rest argument,
-                                   ;; but provides all the necessary fixed arguments
-                                   [else -Null])))
-                  range)))
+           (finish
+            (infer vars dotted-vars
+                   (list (-Tuple* arg-tys full-tail-ty))
+                   (list (-Tuple* domain
+                                  (match rst
+                                    ;; the actual work, when we have a * function
+                                    [(? Type?) (make-Listof rst)]
+                                    ;; ... function
+                                    [(RestDots: dty dbound)
+                                     (make-ListDots dty dbound)]
+                                    ;; the function has no rest argument,
+                                    ;; but provides all the necessary fixed arguments
+                                    [_ -Null])))
+                   rng))]))
        (failure))]
-    [(tc-result1: (AnyPoly: _ _ (Function: '())))
+    [(tc-result1: (AnyPoly: _ _ (Fun: '())))
      (tc-error/expr "Function has no cases")]
     [(tc-result1: f-ty)
      (tc-error/expr "Type of argument to apply is not a function type: \n~a" f-ty)]))
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 e6e0dea9..4cbdf17b 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
@@ -216,7 +216,7 @@
       [(begin0 e . es)
        (begin0
          (tc-expr/check #'e expected)
-         (tc-body/check #'es (tc-any-results -tt)))]
+         (tc-body/check #'es (-tc-any-results -tt)))]
       ;; if
       [(if tst thn els) (tc/if-twoarm #'tst #'thn #'els expected)]
       ;; lambda
@@ -247,14 +247,12 @@
       [(~and (let-values ([(f) fun]) . body) kw:kw-lambda^)
        #:when expected
        (match expected
-         [(tc-result1: (and f (or (Function: _)
-                                  (Poly: _ (Function: _)))))
+         [(tc-result1: (and f (or (? Fun?) (Poly-unsafe: _ (? Fun?)))))
           (define actual-kws (attribute kw.value))
           (check-kw-arity actual-kws f)
           (tc-expr/check/type #'fun (kw-convert f actual-kws #:split #t))
           (ret f -true-propset)]
-         [(or (tc-results: _) (tc-any-results: _))
-          (tc-expr/check form #f)])]
+         [_ (tc-expr/check form #f)])]
       ;; opt function def
       [(~and (let-values ([(f) fun]) . body) opt:opt-lambda^)
        #:when expected
@@ -349,7 +347,7 @@
 ;; Body must be a non empty sequence of expressions to typecheck.
 ;; The final one will be checked against expected.
 (define (tc-body/check body expected)
-  (define any-res (tc-any-results #f))
+  (define any-res (-tc-any-results #f))
   (define exps (syntax->list body))
   (let loop ([exps exps])
     (match exps
@@ -359,10 +357,11 @@
        (define props
          (match results
            [(tc-any-results: p) (list p)]
-           [(tc-results: _ (list (PropSet: p+ p-) ...) _)
-            (map -or p+ p-)]
-           [(tc-results: _ (list (PropSet: p+ p-) ...) _ _ _)
-            (map -or p+ p-)]))
+           [(tc-results: tcrs _)
+            (map (match-lambda
+                   [(tc-result: _ (PropSet: p+ p-) _)
+                    (-or p+ p-)])
+                 tcrs)]))
        (with-lexical-env+props
          props
          #:expected any-res
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-expression.rkt b/typed-racket-lib/typed-racket/typecheck/tc-expression.rkt
index 62b3f9ac..5a3f1f5a 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-expression.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-expression.rkt
@@ -54,15 +54,15 @@
     (if row? do-row-inst do-normal-inst))
   (define (error-case number)
     (tc-error/expr
-      "Cannot instantiate expression that produces ~a values"
-      number))
+     "Cannot instantiate expression that produces ~a values"
+     number))
   (match tc-res
-    [(tc-results: tys fs os)
-     (match tys
-      [(list ty)
-       (ret (list (inst-type ty inst)) fs os)]
-      [_ (error-case (if (null? tys) 0 "multiple"))])]
-    [_ (error-case "multiple")]))
+    [(tc-results: (list (tc-result: t ps o)) #f)
+     (ret (inst-type t inst) ps o)]
+    [_ (error-case (if (and (tc-results? tc-res)
+                            (null? (tc-results-ts tc-res)))
+                       0
+                       "multiple"))]))
 
 
 ;; do-normal-inst : Type Syntax -> Type
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
index ceed66e3..1e5f36c2 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
@@ -48,11 +48,13 @@
                       #:expected expected)))]))
 
 (define (subst-dom-objs argtys argobjs rng)
-  (subst-rep rng (for/list ([o (in-list argobjs)]
-                            [t (in-list argtys)]
-                            [idx (in-naturals)]
-                            #:when (not (Empty? o)))
-                   (list (cons 0 idx) o t))))
+  (instantiate-obj+simplify
+   rng
+   (for/list ([o (in-list argobjs)]
+              [t (in-list argtys)]
+              [idx (in-naturals)]
+              #:when (not (Empty? o)))
+     (list* idx o t))))
 
 (define (tc/funapp f-stx args-stx f-type args-res expected)
   (match-define (list (tc-result1: argtys (PropSet: argps+ argps-) argobjs) ...) args-res)
@@ -60,25 +62,29 @@
     (match f-type
       ;; we special-case this (no case-lambda) for improved error messages
       ;; tc/funapp1 currently cannot handle drest arities
-      [(Function: (list (and a (arr: _ _ _ #f _))))
-       (tc/funapp1 f-stx args-stx a args-res expected)]
-      [(Function: arrs)
-       ;; check there are no drests
-       #:when (not (ormap arr-drest arrs))
+      [(Fun: (list arrow))
+       #:when (not (RestDots? (Arrow-rst arrow)))
+       (tc/funapp1 f-stx args-stx arrow args-res expected)]
+      [(Fun: arrows)
+       ;; check there are no RestDots
+       #:when (not (for/or ([a (in-list arrows)])
+                     (RestDots? (Arrow-rst a))))
        (cond
          ;; find the first function where the argument types match
-         [(for/or ([a (in-list arrs)])
-            (match a [(arr: dom _ rest _ _) (and (subtypes/varargs argtys dom rest) a)]))
+         [(ormap (match-lambda
+                   [(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))]
          [else
           ;; if nothing matched, error
-          (match arrs
-            [(list (arr: doms rngs rests drests _) ...)
+          (match arrows
+            [(list (Arrow: doms rsts _ rngs) ...)
              (domain-mismatches
-              f-stx args-stx f-type doms rests drests rngs args-res #f #f
+              f-stx args-stx f-type doms rsts rngs args-res #f #f
               #:expected expected
               #:msg-thunk (lambda (dom)
                             (string-append
@@ -86,68 +92,71 @@
                              dom)))])])]
       ;; any kind of dotted polymorphic function without mandatory keyword args
       [(PolyDots: (list fixed-vars ... dotted-var)
-                  (Function: arrs))
+                  (Fun: arrows))
        ;; check there are no mandatory kw args
-       #:when (not (for*/or ([a (in-list arrs)]
-                             [kws (in-value (arr-kws a))])
+       #:when (not (for*/or ([a (in-list arrows)]
+                             [kws (in-value (Arrow-kws a))])
                      (ormap Keyword-required? kws)))
        (for/first-valid-inference
-           #:in-arrs [a (in-list arrs)]
-         #:arr-match (arr: dom rng rest drest _)
+           #:in-arrs [a (in-list arrows)]
+         #:arr-match (Arrow: dom rst _ rng)
          #:function-syntax f-stx
          #:args-syntax args-stx
          #:infer-when
          ;; only try inference if the argument lengths are appropriate
-         (cond [rest (<= (length dom) (length argtys))]
-               [drest (and (<= (length dom) (length argtys))
-                           (eq? dotted-var (cdr drest)))]
-               [else (= (length dom) (length argtys))])
+         (match rst
+           [(? Type?) (<= (length dom) (length argtys))]
+           [(RestDots: _ dbound) (and (<= (length dom) (length argtys))
+                                      (eq? dotted-var dbound))]
+           [_ (= (length dom) (length argtys))])
          ;; Only try to infer the free vars of the rng (which includes the vars
          ;; in props/objects).
          #:maybe-inferred-substitution
          (let ([rng (subst-dom-objs argtys argobjs rng)])
-           (extend-tvars fixed-vars
-                         (cond
-                           [drest
-                            (infer/dots
-                             fixed-vars dotted-var argtys dom (car drest) rng (fv rng)
-                             #:expected (and expected (tc-results->values expected))
-                             #:objs argobjs)]
-                           [rest
-                            (infer/vararg fixed-vars (list dotted-var) argtys dom rest rng
-                                          (and expected (tc-results->values expected))
-                                          #:objs argobjs)]
-                           ;; no rest or drest
-                           [else (infer fixed-vars
-                                        (list dotted-var)
-                                        argtys
-                                        dom
-                                        rng
-                                        (and expected (tc-results->values expected))
-                                        #:objs argobjs)])))
+           (extend-tvars
+            fixed-vars
+            (match rst
+              [(? Type?)
+               (infer/vararg
+                fixed-vars (list dotted-var) argtys dom rst rng
+                (and expected (tc-results->values expected))
+                #:objs argobjs)]
+              [(RestDots: dty _)
+               (infer/dots
+                fixed-vars dotted-var argtys dom dty rng (fv rng)
+                #:expected (and expected (tc-results->values expected))
+                #:objs argobjs)]
+              [_ (infer fixed-vars
+                        (list dotted-var)
+                        argtys
+                        dom
+                        rng
+                        (and expected (tc-results->values expected))
+                        #:objs argobjs)])))
          #:function-type f-type
          #:args-results args-res
          #:expected expected)]
       ;; regular polymorphic functions without dotted rest, 
       ;; we do not choose any instantiations with mandatory keyword arguments
-      [(Poly: vars (Function: arrs))
-       ;; check there are no drests
-       #:when (not (ormap arr-drest arrs))
+      [(Poly: vars (Fun: arrows))
+       ;; check there are no RestDots
+       #:when (not (for/or ([a (in-list arrows)])
+                     (RestDots? (Arrow-rst a))))
        (for/first-valid-inference
-           #:in-arrs [a (in-list arrs)]
-         #:arr-match (arr: dom rng rest _ kws)
+           #:in-arrs [a (in-list arrows)]
+         #:arr-match (Arrow: dom rst kws rng)
          #:function-syntax f-stx
          #:args-syntax args-stx
          ;; only try inference if the argument lengths are appropriate
          ;; and there's no mandatory kw
          #:infer-when
-         (and (not (ormap Keyword-required? kws)) ((if rest <= =) (length dom) (length argtys)))
+         (and (not (ormap Keyword-required? kws)) ((if rst <= =) (length dom) (length argtys)))
          ;; Only try to infer the free vars of the rng (which includes the vars
          ;; in props/objects).
          #:maybe-inferred-substitution
          (let ([rng (subst-dom-objs argtys argobjs rng)])
            (extend-tvars vars
-                         (infer/vararg vars null argtys dom rest rng
+                         (infer/vararg vars null argtys dom rst rng
                                        (and expected (tc-results->values expected))
                                        #:objs argobjs)))
          #:function-type f-type
@@ -156,7 +165,11 @@
       ;; Row polymorphism. For now we do really dumb inference that only works
       ;; in very restricted cases, but is probably enough for most cases in
       ;; the Racket codebase. Eventually this should be extended.
-      [(PolyRow: vars constraints (and f-ty (Function/arrs: doms _ _ #f _)))
+      [(PolyRow: vars constraints (and f-ty (Fun: arrows)))
+       ;; check there are no RestDots
+       #:when (not (for/or ([a (in-list arrows)])
+                     (RestDots? (Arrow-rst a))))
+       
        (define (fail)
          (poly-fail f-stx args-stx f-type args-res
                     #:name (and (identifier? f-stx) f-stx)
@@ -166,9 +179,10 @@
        ;; only infer if there is only one argument type that has the relevant
        ;; row type variable in its free variables in all cases
        (define row-var-idxs
-         (for/list ([dom (in-list doms)])
+         (for*/list ([a (in-list arrows)]
+                     [dom (in-value (Arrow-dom a))])
            (define num-occurs
-             (for/list ([dom-type dom]
+             (for/list ([dom-type (in-list dom)]
                         [idx (in-naturals)]
                         #:when (member row-var (fv dom-type)))
                idx))
@@ -189,7 +203,7 @@
                          args-res expected)]
              [else (fail)])]
       ;; procedural structs
-      [(Struct: _ _ _ (? Function? proc-ty) _ _)
+      [(Struct: _ _ _ (? Fun? proc-ty) _ _)
        (tc/funapp f-stx #`(#,(syntax/loc f-stx dummy) . #,args-stx) proc-ty
                   (cons (ret f-type) args-res) expected)]
       ;; parameters are functions too
@@ -212,14 +226,14 @@
       [(? resolvable?)
        (tc/funapp f-stx args-stx (resolve-once f-type) args-res expected)]
       ;; a union of functions can be applied if we can apply all of the elements
-      [(Union: (? Bottom?) ts) #:when (andmap Function? ts)
+      [(Union: (? Bottom?) ts) #:when (andmap Fun? ts)
        (merge-tc-results
         (for/list ([fty (in-list ts)])
           (tc/funapp f-stx args-stx fty args-res expected)))]
       ;; bottom or error type is a perfectly good fcn type
       [(or (Bottom:) (Error:)) (ret f-type)]
       ;; otherwise fail
-      [(Poly: ns (Function: arrs))
+      [(Poly: ns (? Fun?))
        (tc-error/expr
         (string-append "Cannot infer type instantiation for type ~a. Please add "
                        "more type annotations")
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 1a7d1037..953d5b8b 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
@@ -41,17 +41,16 @@
            #:attr mapping (make-immutable-free-id-table)
            #:attr flag-mapping (make-immutable-free-id-table)))
 
-(define (expected-str tys-len rest-ty drest arg-len rest)
+(define (expected-str tys-len rst arg-len rest-id)
   (format "Expected function with ~a argument~a~a, but got function with ~a argument~a~a"
           tys-len
           (if (= tys-len 1) "" "s")
-          (if (or rest-ty
-                  drest)
+          (if rst
               " and a rest arg"
               "")
           arg-len
           (if (= arg-len 1) "" "s")
-          (if rest " and a rest arg" "")))
+          (if rest-id " and a rest arg" "")))
 
 ;; tc-lambda-body: Typechecks the body with the given args and names and returns the resulting arr?.
 ;; arg-names: The identifiers of the positional args
@@ -63,47 +62,46 @@
 (define/cond-contract
   (tc-lambda-body arg-names arg-types #:rest [raw-rest #f] #:expected [expected #f] body)
   (->* ((listof identifier?) (listof Type?) syntax?)
-       (#:rest (or/c #f (list/c identifier? (or/c Type? (cons/c Type? symbol?))))
+       (#:rest (or/c #f (list/c identifier? (or/c Type? RestDots?)))
         #:expected (or/c #f tc-results/c))
-       arr?)
-  (define-values (rest-id rest)
+       Arrow?)
+  (define-values (rest-id rst)
     (if raw-rest
         (values (first raw-rest) (second raw-rest))
         (values #f #f)))
 
   (define rest-types
-    (cond
-      [(not rest) (list)]
-      [(cons? rest) (list (make-ListDots (car rest) (cdr rest)))]
-      [else (list (-lst rest))]))
+    (match rst
+      [(? Type?) (list (-lst rst))]
+      [(RestDots: dty dbound)
+       (list (make-ListDots dty dbound))]
+      [#f (list)]))
   (define rest-names
     (if rest-id (list rest-id) null))
 
-  (make-arr*
+  (-Arrow
    arg-types
    (abstract-results
     (with-extended-lexical-env
-      [#:identifiers (append rest-names arg-names)
-       #:types (append rest-types arg-types)]
+        [#:identifiers (append rest-names arg-names)
+         #:types (append rest-types arg-types)]
       (tc-body/check body expected))
     arg-names #:rest-id rest-id)
-   #:rest (and (Type? rest) rest)
-   #:drest (and (cons? rest) rest)))
+   #:rest rst))
 
 ;; check-clause: Checks that a lambda clause has arguments and body matching the expected type
 ;; arg-list: The identifiers of the positional args in the lambda form
 ;; rest-id: The identifier of the rest arg, or #f for no rest arg
 ;; body: The body of the lambda to typecheck.
 ;; arg-tys: The expected positional argument types.
-;; rest-ty: The expected base type of the rest arg (not poly dotted case)
-;; drest: The expected base type of the rest arg and its bound (poly dotted case)
+;; rst: #f, expected rest arg Type, or expected RestDots
 ;; ret-ty: The expected type of the body of the lambda.
-(define/cond-contract (check-clause arg-list rest-id body arg-tys rest-ty drest ret-ty)
+(define/cond-contract (check-clause arg-list rest-id body arg-tys rst ret-ty)
   ((listof identifier?)
-   (or/c #f identifier?) syntax? (listof Type?) (or/c #f Type?)
-   (or/c #f (cons/c Type? symbol?)) tc-results/c
+   (or/c #f identifier?) syntax? (listof Type?) (or/c #f Type? RestDots?)
+   tc-results/c
    . -> .
-   arr?)
+   Arrow?)
   (let* ([arg-len (length arg-list)]
          [tys-len (length arg-tys)]
          [arg-types
@@ -112,9 +110,12 @@
               (cond
                 [(= arg-len tys-len) arg-tys]
                 [(< arg-len tys-len) (take arg-tys arg-len)]
-                [(> arg-len tys-len) (append arg-tys
-                                             (map (lambda _ (or rest-ty (Un)))
-                                                  (drop arg-list tys-len)))]))])
+                [(> arg-len tys-len)
+                 (append arg-tys
+                         (map (if (Type? rst)
+                                  (λ _ rst)
+                                  (λ _ -Bottom))
+                              (drop arg-list tys-len)))]))])
 
     ;; Check that the number of formal arguments is valid for the expected type.
     ;; Thus it must be able to accept the number of arguments that the expected
@@ -123,19 +124,20 @@
     ;; This allows a form like (lambda args body) to have the type (-> Symbol
     ;; Number) with out a rest arg.
     (when (or (and (< arg-len tys-len) (not rest-id))
-              (and (> arg-len tys-len) (not (or rest-ty drest))))
-      (tc-error/delayed (expected-str tys-len rest-ty drest arg-len rest-id)))
+              (and (> arg-len tys-len) (not rst)))
+      (tc-error/delayed (expected-str tys-len rst arg-len rest-id)))
     (define rest-type
       (cond
         [(not rest-id) #f]
-        [drest drest]
+        [(RestDots? rst) rst]
         [(dotted? rest-id)
-         => (λ (b) (cons (extend-tvars (list b) (get-type rest-id #:default Univ)) b))]
+         => (λ (b) (make-RestDots (extend-tvars (list b) (get-type rest-id #:default Univ))
+                                  b))]
         [else
          (define base-rest-type
            (cond
              [(type-annotation rest-id) (get-type rest-id #:default Univ)]
-             [rest-ty rest-ty]
+             [(Type? rst) rst]
              [else Univ]))
          (define extra-types
            (if (<= arg-len tys-len)
@@ -152,8 +154,8 @@
 ;; drest-ty and drest-bound are both false or not false
 ;; tc/lambda-clause/check: formals syntax listof[Type?] tc-result
 ;;                         option[Type?] option[(cons Type? symbol)] -> arr?
-(define (tc/lambda-clause/check formals body arg-tys ret-ty rest-ty drest)
-  (check-clause (formals-positional formals) (formals-rest formals) body arg-tys rest-ty drest ret-ty))
+(define (tc/lambda-clause/check formals body arg-tys ret-ty rst)
+  (check-clause (formals-positional formals) (formals-rest formals) body arg-tys rst ret-ty))
 
 ;; typecheck a single opt-lambda clause with argument list and body
 ;; tc/opt-lambda-clause: listof[identifier] syntax -> listof[arr?]
@@ -188,12 +190,12 @@
     (tc-lambda-body arg-list arg-types body)))
 
 ;; restrict-to-arity : arr? nat -> (or/c #f arr?)
-;; either produces a new arity which is a subtype of arr with arity n,
+;; either produces a new arrow which is a subtype of arr with arity n,
 ;; or #f is that is not possible
 (define (restrict-to-arity arr n)
   (match arr
     ;; currently does not handle rest arguments
-    [(arr: args ret #f #f '())
+    [(Arrow: args #f '() _)
      #:when (= n (length args))
      arr]
     [_ #f]))
@@ -228,12 +230,13 @@
          ;; Lambda with poly dotted rest argument
          [(and rest-id (dotted? rest-id))
           =>
-          (lambda (bound)
+          (λ (bound)
             (unless (bound-index? bound)
               (if (bound-tvar? bound)
                   (tc-error "Bound on ... type (~a) is not an appropriate type variable" bound)
                   (tc-error/stx rest-id "Bound on ... type (~a) was not in scope" bound)))
-            (cons (extend-tvars (list bound) (get-type rest-id #:default Univ)) bound))]
+            (make-RestDots (extend-tvars (list bound) (get-type rest-id #:default Univ))
+                           bound))]
          ;; Lambda with regular rest argument
          [rest-id
           (get-type rest-id #:default Univ)]
@@ -246,7 +249,7 @@
             ;; but we can't return anything but a (listof arr?) here 
             ;; FIXME: misses optimization opportunities in this code
             (match (tc-expr eta-expanded?)
-              [(tc-result1: (Function: arrs))
+              [(tc-result1: (Fun: arrs))
                (define possibles (for*/list ([arr (in-list arrs)]
                                              [restricted (in-value (restrict-to-arity arr (length arg-list)))]
                                              #:when restricted)
@@ -330,7 +333,10 @@
       [(tc-result1: t)
        (define resolved (resolve t))
        (match resolved
-         [(Function/arrs: _ _ _ _ '()) resolved]
+         [(Fun: arrows)
+          #:when (for/and ([arr (in-list arrows)])
+                   (null? (Arrow-kws arr)))
+          resolved]
          [_ #f])]
       [_ #f]))
 
@@ -342,13 +348,18 @@
   (define (find-matching-arrs formal-arity arities-seen)
     (match-define (list formal-positionals formal-rest) formal-arity)
     (match expected-type
-      [(Function/arrs: argss rets rests drests '() #:arrs fs)
-       (for/list ([a (in-list argss)] [f (in-list fs)] [r (in-list rests)] [dr (in-list drests)]
-                  #:unless (arities-seen-seen-before? arities-seen (list (length a) (or r dr)))
-                  #:when (if formal-rest
-                             (or r (>= (length a) formal-positionals))
-                             ((if (or r dr) <= =) (length a) formal-positionals)))
-         f)]
+      [(Fun: arrows)
+       #:when (for/and ([arr (in-list arrows)])
+                (null? (Arrow-kws arr)))
+       (for*/list ([a (in-list arrows)]
+                   [dom (in-value (Arrow-dom a))]
+                   [rst (in-value (Arrow-rst a))]
+                   #:unless (arities-seen-seen-before? arities-seen (list (length dom) rst))
+                   #:when (cond
+                            [formal-rest
+                             (or (Type? rst) (>= (length dom) formal-positionals))]
+                            [else ((if rst <= =) (length dom) formal-positionals)]))
+         a)]
       [_ #f]))
 
 
@@ -377,24 +388,26 @@
         (andmap (λ (f-b-arr) (empty? (third f-b-arr))) used-formals+bodies+arrs)
         ;; If the empty function is expected, then don't error out
         (match expected-type
-          [(Function: (list)) #f]
+          [(Fun: (list)) #f]
           [_ #t]))
       ;; TODO improve error message.
-      (tc-error/expr #:return (list (make-arr* null (Un) #:rest Univ))
+      (tc-error/expr #:return (list (-Arrow null -Bottom #:rest Univ))
                      "Expected a function of type ~a, but got a function with the wrong arity"
                      expected-type)
       (apply append
              (for/list ([fb* (in-list used-formals+bodies+arrs)])
                (match-define (list f* b* t*) fb*)
-               (match t*
-                 [#f (tc/lambda-clause f* b*)]
-                 [(list (arr: argss rets rests drests '()) ...)
-                  (for/list ([args (in-list argss)] [ret (in-list rets)] [rest (in-list rests)] [drest (in-list drests)])
-                    (tc/lambda-clause/check
-                     f* b* args (values->tc-results ret (formals->objects f*)) rest drest))])))))
+               (cond
+                 [(not t*) (tc/lambda-clause f* b*)]
+                 [else
+                  (for/list ([arrow (in-list t*)])
+                    (match arrow
+                      [(Arrow: dom rst '() rng)
+                       (tc/lambda-clause/check
+                        f* b* dom (values->tc-results rng (formals->objects f*)) rst)]))])))))
 
 (define (tc/mono-lambda/type formals bodies expected)
-  (make-Function
+  (make-Fun
     (tc/mono-lambda
       (for/list ([f (in-syntax formals)] [b (in-syntax bodies)])
          (list (make-formals f) b))
@@ -547,10 +560,9 @@
   (define formals (syntax->list formals*))
   (define ft (t:->* args (tc-results->values return)))
   (define names (cons name formals))
-  (define objs (map (λ (_) -empty-obj) names))
   (with-extended-lexical-env
     [#:identifiers (cons name formals)
      #:types (cons ft args)]
     (values
-     (replace-names names objs (ret ft))
-     (replace-names names objs (tc-body/check body return)))))
+     (erase-identifiers (ret ft) names)
+     (erase-identifiers (tc-body/check body return) names))))
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 f9d584d3..88236879 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
@@ -118,8 +118,7 @@
     [#:identifiers idents
      #:types types
      #:aliased-objects aliased-objs]
-    (erase-names
-     ids-to-erase
+    (erase-identifiers
      (with-lexical-env+props
        props
        #:expected expected
@@ -130,7 +129,8 @@
        ;; before checking the body
        (pre-body-thunk)
        ;; typecheck the body
-       (tc-body/check body expected)))))
+       (tc-body/check body expected))
+     ids-to-erase)))
 
 (define (tc-expr/maybe-expected/t e names)
   (syntax-parse names
@@ -208,7 +208,7 @@
      ordered-clauses
      (λ ()
        ;; types the user gave.
-       (define given-rhs-types (map (λ (l) (map tc-result (map get-type l))) remaining-names))
+       (define given-rhs-types (map (λ (l) (map -tc-result (map get-type l))) remaining-names))
        (check-let-body
         remaining-names
         given-rhs-types
@@ -300,9 +300,9 @@
            (with-extended-lexical-env
              [#:identifiers names
               #:types ts]
-             (replace-names names
-                            os
-                            (loop (cdr clauses))))])))
+             (substitute-names (loop (cdr clauses))
+                               names
+                               os))])))
 
 ;; this is so match can provide us with a syntax property to
 ;; say that this binding is only called in tail position
@@ -317,6 +317,7 @@
      (tc-expr/check e expected)]
     [_ (tc-expr e)]))
 
+
 (define (tc/let-values namess exprs body [expected #f])
   (let* (;; a list of each name clause
          [namess (stx-map syntax->list namess)]
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt b/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
index 36d487cc..8e441c5a 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
@@ -2,7 +2,7 @@
 
 (require "../utils/utils.rkt"
          racket/match racket/list
-         (except-in (types abbrev utils prop-ops tc-result)
+         (except-in (types abbrev utils prop-ops)
                     -> ->* one-of/c)
          (rep type-rep prop-rep object-rep values-rep rep-utils)
          (typecheck tc-subst)
@@ -18,24 +18,28 @@
 (define/cond-contract (abstract-results results arg-names #:rest-id [rest-id #f])
   ((tc-results/c (listof identifier?)) (#:rest-id (or/c #f identifier?))
    . ->* . SomeValues?)
-  (define positional-arg-objects
-    (for/list ([n (in-range (length arg-names))])
-      (make-Path null (cons 0 n))))
-  (define-values (names objects)
-    (if rest-id
-        (values (cons rest-id arg-names)
-                (cons -empty-obj positional-arg-objects))
-        (values arg-names positional-arg-objects)))
-  (tc-results->values (replace-names names objects results)))
+  (define abstracted (abstract-obj results arg-names))
+  (tc-results->values
+   (if rest-id
+       (erase-identifiers abstracted (list rest-id))
+       abstracted)))
 
 (define (tc-results->values tc)
   (match (fix-results tc)
     [(tc-any-results: f)
      (-AnyValues f)]
-    [(tc-results: ts fs os)
-     (make-Values (map -result ts fs os))]
-    [(tc-results: ts fs os dty dbound)
-     (make-ValuesDots (map -result ts fs os) dty dbound)]))
+    [(tc-results: tcrs #f)
+     (make-Values
+      (map (match-lambda
+             [(tc-result: t ps o) (-result t ps o)])
+           tcrs))]
+    [(tc-results: tcrs (RestDots: dty dbound))
+     (make-ValuesDots
+      (map (match-lambda
+             [(tc-result: t ps o) (-result t ps o)])
+           tcrs)
+      dty
+      dbound)]))
 
 (define (flatten-props ps)
   (let loop ([ps ps])
@@ -59,16 +63,16 @@
           [(cons p rst)
            (match p
              [(TrueProp:) (partition! rst)]
-             [(TypeProp: obj (Refine: t p))
+             [(TypeProp: obj (Refine: t raw-p))
               (partition! (list (-is-type obj t)
-                                (instantiate-rep/obj p obj t)))
+                                (instantiate-obj raw-p obj)))
               (partition! rst)]
              [(? TypeProp? p)
               (set! atoms (cons p atoms))
               (partition! rst)]
-             [(NotTypeProp: obj (Refine: t p))
+             [(NotTypeProp: obj (Refine: t raw-p))
               (partition! (list (-or (-not-type obj t)
-                                     (negate-prop (instantiate-rep/obj p obj t)))))
+                                     (negate-prop (instantiate-obj raw-p obj)))))
               (when atoms (partition! rst))]
              [(? NotTypeProp? p)
               (set! atoms (cons p atoms))
@@ -128,48 +132,48 @@
 
 (define (unconditional-prop res)
   (match res
-    [(tc-any-results: pset) pset]
-    [(tc-results (list (tc-result: _ (PropSet: p+ p-) _) ...) _)
-     (apply -and (map -or p+ p-))]))
+    [(tc-any-results: p) p]
+    [(tc-results: tcrs _)
+     (apply
+      -and
+      (map (match-lambda
+             [(tc-result: _ (PropSet: p+ p-) _)
+              (-or p+ p-)])
+           tcrs))]))
 
 (define (merge-tc-results results)
   (define/match (merge-tc-result r1 r2)
     [((tc-result: t1 (PropSet: p1+ p1-) o1)
       (tc-result: t2 (PropSet: p2+ p2-) o2))
-     (tc-result
-       (Un t1 t2)
-       (-PS (-or p1+ p2+) (-or p1- p2-))
-       (if (equal? o1 o2) o1 -empty-obj))])
+     (-tc-result
+      (Un t1 t2)
+      (-PS (-or p1+ p2+) (-or p1- p2-))
+      (if (equal? o1 o2) o1 -empty-obj))])
 
   (define/match (same-dty? r1 r2)
     [(#f #f) #t]
-    [((cons t1 dbound) (cons t2 dbound)) #t]
+    [((RestDots: t1 dbound) (RestDots: t2 dbound)) #t]
     [(_ _) #f])
   (define/match (merge-dty r1 r2)
     [(#f #f) #f]
-    [((cons t1 dbound) (cons t2 dbound))
-     (cons (Un t1 t2) dbound)])
-
-  (define/match (number-of-values res)
-    [((tc-results rs #f))
-     (length rs)]
-    [((tc-results rs (cons _ dbound)))
-     (format "~a and ... ~a" (length rs) dbound)])
+    [((RestDots: t1 dbound) (RestDots: t2 dbound))
+     (make-RestDots (Un t1 t2) dbound)])
 
 
   (define/match (merge-two-results res1 res2)
     [((tc-result1: (== -Bottom)) res2) res2]
     [(res1 (tc-result1: (== -Bottom))) res1]
     [((tc-any-results: f1) res2)
-     (tc-any-results (-or f1 (unconditional-prop res2)))]
+     (-tc-any-results (-or f1 (unconditional-prop res2)))]
     [(res1 (tc-any-results: f2))
-     (tc-any-results (-or (unconditional-prop res1) f2))]
-    [((tc-results results1 dty1) (tc-results results2 dty2))
+     (-tc-any-results (-or (unconditional-prop res1) f2))]
+    [((tc-results: results1 dty1)
+      (tc-results: results2 dty2))
      ;; if we have the same number of values in both cases
      (cond
        [(and (= (length results1) (length results2))
              (same-dty? dty1 dty2))
-        (tc-results (map merge-tc-result results1 results2)
+        (-tc-results (map merge-tc-result results1 results2)
                     (merge-dty dty1 dty2))]
        ;; otherwise, error
        [else
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
index 21976e72..693a9d16 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
@@ -5,211 +5,115 @@
 
 (require "../utils/utils.rkt"
          (utils tc-utils)
-         racket/match racket/list
+         racket/match
          (contract-req)
-         (except-in (types abbrev utils prop-ops path-type subtract overlap)
+         (env lexical-env)
+         (except-in (types abbrev utils prop-ops subtype
+                           path-type subtract overlap)
                     -> ->* one-of/c)
          (only-in (infer infer) intersect restrict)
-         (types subtype)
          (rep core-rep type-rep object-rep
               prop-rep rep-utils values-rep))
 
+(provide instantiate-obj+simplify)
+
 (provide/cond-contract
- [restrict-values (-> SomeValues? (listof Type?) SomeValues?)]
  [values->tc-results (->* (SomeValues? (listof OptObject?))
                           ((listof Type?))
                           full-tc-results/c)]
- [replace-names (-> (listof identifier?)
-                    (listof OptObject?)
-                    tc-results/c
-                    tc-results/c)]
- [erase-names (-> (listof identifier?)
-                  tc-results/c
-                  tc-results/c)])
-
-(provide subst-rep
-         instantiate-rep/obj)
-
-
-(define (instantiate-rep/obj rep obj [t Univ])
-  (subst-rep rep (list (list (cons 0 0) obj t))))
+ [erase-identifiers (-> tc-results/c
+                        (listof identifier?)
+                        tc-results/c)])
 
 
 ;; Substitutes the given objects into the values and turns it into a
 ;; tc-result.  This matches up to the substitutions in the T-App rule
 ;; from the ICFP paper.
-(define (values->tc-results v os [ts '()])
-  (define targets
-    (for/list ([o (in-list os)]
-               [arg (in-naturals)]
-               [t (in-list/rest ts Univ)])
-      (list (cons 0 arg) o t)))
-  (define res
-    (match v
-      [(AnyValues: p)
-       (tc-any-results p)]
-      [(Results: t ps o)
-       (ret t ps o)]
-      [(Results: t ps o dty dbound)
-       (ret t ps o dty dbound)]
-      [_ (int-err "invalid res in values->tc-results: ~a" res)]))
+;; NOTE! 'os' should contain no unbound relative addresses (i.e. "free" 
+;;       De Bruijn indices) as those indices will NOT be updated if they
+;;        are substituted under binders.
+(define (values->tc-results v objs [types '()])
+  (define res->tc-res
+    (match-lambda
+      [(Result: t ps o) (-tc-result t ps o)]))
   
-  (subst-tc-results res targets))
-
-;; Restrict the objects in v refering to the current functions
-;; arguments to be of the types ts. Uses an identity substitution (yuck)
-;; since substitution does this same restriction.
-(define (restrict-values v ts)
-  (define targets
-    (for/list ([t (in-list ts)]
-               [arg (in-naturals)])
-      (define nm (cons 0 arg))
-      (list nm (-id-path nm) t)))
-  (subst-rep v targets))
-
-
-;; For each name replaces all uses of it in res with the
-;; corresponding object.  This is used so that names do not escape the
-;; scope of their definitions
-(define (replace-names names objects res)
-  (define targets
-    (for/list ([nm (in-list names)]
-               [o (in-list objects)])
-      (list nm o Univ)))
-  (subst-tc-results res targets))
-
-(define (erase-names names res)
-  (define targets
-    (for/list ([nm (in-list names)])
-      (list nm -empty-obj Univ)))
-  (subst-tc-results res targets))
-
-(define (subst-tc-results res targets)
-  (define (sr t ps o)
-    (subst-tc-result t ps o targets))
-  (define (sub x) (subst-rep x targets))
+  (define mapping (for/list ([o (in-list objs)]
+                             [t (in-list/rest types Univ)]
+                             [idx (in-naturals)])
+                    (list* idx o t)))
   
-  (match res
-    [(tc-any-results: p) (tc-any-results (sub p))]
-    [(tc-results: ts ps os)
-     (tc-results (map sr ts ps os) #f)]
-    [(tc-results: ts ps os dt db)
-     (tc-results (map sr ts ps os) (cons (sub dt) db))]
-    [_ (int-err "invalid res in subst-tc-results: ~a" res)]))
+  (match (instantiate-obj+simplify v mapping)
+    [(AnyValues: p)
+     (-tc-any-results p)]
+    [(Values: rs)
+     (-tc-results (map res->tc-res rs) #f)]
+    [(ValuesDots: rs dty dbound)
+     (-tc-results (map res->tc-res rs) (make-RestDots dty dbound))]))
 
-;; Substitution of objects into a tc-result This is a combination of
-;; the other substitutions, plus a restriction of the returned type to
-;; the arguments type if the returned object corresponds to an
-;; argument.
-(define (subst-tc-result r-t r-ps r-o targets)
-  (define type*
-    (match r-o
-      [(Path: flds nm)
-       (cond
-         [(assoc nm targets name-ref=?) =>
-          (match-lambda
-            [(list _ _ t)
-             (or (path-type flds t) Univ)])]
-         [else Univ])]
-      [_ Univ]))
+(define (erase-identifiers res names)
+  (substitute-names res names (for/list ([_ (in-list names)])
+                                -empty-obj)))
 
-  (tc-result
-   (intersect (subst-rep r-t targets)
-              type*)
-   (subst-rep r-ps targets)
-   (subst-rep r-o targets)))
-
-
-;; inc-lvls
-;; This function increments the 'lvl' field in all of the targets
-;; and objects of substitution (see 'inc-lvl' above)
-(define (inc-lvls targets)
-  (for/list ([tgt (in-list targets)])
-    (match tgt
-      [(list nm1 (Path: flds nm2) ty)
-       (list (inc-lvl nm1) (make-Path flds (inc-lvl nm2)) ty)]
-      [(cons nm1 rst)
-       (cons (inc-lvl nm1) rst)])))
-
-;; Simple substitution of objects into a Rep
-;; This is basically 'rep[x ↦ o]'.
-;; If that was the only substitution we were doing,
-;; and the type of 'x' was 'τ', then 'targets'
-;; would equal (list (list x o τ)) (i.e. it's the list of
-;; identifiers being substituted out, the optional object replacing
-;; them, and their type).
-(define/cond-contract (subst-rep rep targets)
-  (-> any/c (listof (list/c name-ref/c OptObject? Type?))
-      any/c)
-  (define (subst/inc rep)
-    (subst-rep rep (inc-lvls targets)))
-  ;; substitution loop
-  (let subst ([rep rep])
+(define (instantiate-obj+simplify rep mapping)
+  ;; lookup: if idx has a mapping,
+  ;; then returns (cons/c OptObject? Type?),
+  ;; else returns #f
+  (define (lookup idx) (match (assv idx mapping)
+                         [(cons _ entry) entry]
+                         [_ #f]))
+  (let subst/lvl ([rep rep] [lvl 0])
+    (define (subst rep) (subst/lvl rep lvl))
     (match rep
       ;; Functions
       ;; increment the level of the substituted object
-      [(arr: dom rng rest drest kws)
-       (make-arr (map subst dom)
-                 (subst/inc rng)
-                 (and rest (subst rest))
-                 (and drest (cons (subst (car drest)) (cdr drest)))
-                 (map subst kws))]
+      [(Arrow: dom rst kws rng)
+       (make-Arrow (map subst dom)
+                   (and rst (subst rst))
+                   (map subst kws)
+                   (subst/lvl rng (add1 lvl)))]
       [(Intersection: ts raw-prop)
        (-refine (make-Intersection (map subst ts))
-                (subst/inc raw-prop))]
-      [(Path: flds nm)
-       (let ([flds (map subst flds)])
-         (cond
-           [(assoc nm targets name-ref=?)
-            =>
-            (λ (l) (match (second l)
-                     [(Empty:) -empty-obj]
-                     [(Path: flds* nm*)
-                      (make-Path (append flds flds*) nm*)]
-                     [(? LExp? l) #:when (null? flds) l]
-                     [_ -empty-obj]))]
-           [else (make-Path flds nm)]))]
+                (subst/lvl raw-prop (add1 lvl)))]
+      [(Path: flds (cons (== lvl) (app lookup (list o _))))
+       (make-Path (map subst flds) o)]
       ;; restrict with the type for results and props
-      [(TypeProp: (and obj (Path: flds nm)) obj-ty)
-       (let ([flds (map subst flds)])
-         (cond
-           [(assoc nm targets name-ref=?) =>
-            (match-lambda
-              [(list _ inner-obj inner-obj-ty)
-               (define inner-obj-ty-at-flds (or (path-type flds inner-obj-ty) Univ))
-               (define new-obj-ty (intersect obj-ty inner-obj-ty-at-flds obj))
-               (match inner-obj
-                 [_ #:when (Bottom? new-obj-ty) -ff]
-                 [_ #:when (subtype inner-obj-ty-at-flds obj-ty) -tt]
-                 [(Empty:) -tt]
-                 [(Path: flds* nm*)
-                  (define resulting-obj (make-Path (append flds flds*) nm*))
-                  (-is-type resulting-obj new-obj-ty)]
-                 [(? LExp? l) (if (null? flds)
-                                  (-is-type l new-obj-ty)
-                                  -ff)])])]
-           [else (-is-type (make-Path flds nm) (subst obj-ty))]))]
-      [(NotTypeProp: (and obj (Path: flds nm)) neg-obj-ty)
-       (let ([flds (map subst flds)])
-         (cond
-           [(assoc nm targets name-ref=?)
-            =>
-            (match-lambda
-              [(list _ inner-obj inner-obj-ty)
-               (define inner-obj-ty-at-flds (or (path-type flds inner-obj-ty) Univ))
-               (define new-obj-ty (subtract inner-obj-ty-at-flds neg-obj-ty obj))
-               (define new-neg-obj-ty (restrict neg-obj-ty inner-obj-ty-at-flds obj))
-               (match inner-obj
-                 [_ #:when (Bottom? new-obj-ty) -ff]
-                 [_ #:when (Bottom? new-neg-obj-ty) -tt]
-                 [(Empty:) -tt]
-                 [(Path: flds* nm*)
-                  (define resulting-obj (make-Path (append flds flds*) nm*))
-                  (-not-type resulting-obj new-neg-obj-ty)]
-                 [(? LExp? l) (if (null? flds)
-                                  (-not-type l new-neg-obj-ty)
-                                  -ff)])])]
-           [else
-            (-not-type (make-Path flds nm) (subst neg-obj-ty))]))]
+      [(TypeProp: (Path: flds (cons (== lvl) (app lookup (? pair? entry))))
+                  prop-ty)
+       (define o (make-Path (map subst flds) (car entry)))
+       (define o-ty (or (path-type flds (cdr entry)) Univ))
+       (define new-prop-ty (intersect prop-ty o-ty o))
+       (cond
+         [(Bottom? new-prop-ty) -ff]
+         [(subtype o-ty prop-ty) -tt]
+         [(Empty? o) -tt]
+         [else (-is-type o new-prop-ty)])]
+      [(NotTypeProp: (Path: flds (cons (== lvl) (app lookup (? pair? entry))))
+                     prop-ty)
+       (define o (make-Path (map subst flds) (car entry)))
+       (define o-ty (or (path-type flds (cdr entry)) Univ))
+       (define new-o-ty (subtract o-ty prop-ty o))
+       (define new-prop-ty (restrict prop-ty o-ty o))
+       (cond
+         [(or (Bottom? new-o-ty)
+              (Univ? new-prop-ty))
+          -ff]
+         [(Empty? o) -tt]
+         [else (-not-type o new-prop-ty)])]
+      [(tc-result: orig-t
+                   orig-ps
+                   (Path: flds (cons (== lvl) (app lookup (? pair? entry)))))
+       (define o (make-Path (map subst flds) (car entry)))
+       (define t (intersect orig-t (or (path-type flds (cdr entry)) Univ)))
+       (define ps (subst orig-ps))
+       (-tc-result t ps o)]
+      [(Result: orig-t
+                orig-ps
+                (Path: flds (cons (== lvl) (app lookup (? pair? entry)))))
+       (define o (make-Path (map subst flds) (car entry)))
+       (define t (intersect orig-t (or (path-type flds (cdr entry)) Univ)))
+       (define ps (subst orig-ps))
+       (make-Result t ps o)]
       ;; else default fold over subfields
       [_ (Rep-fmap rep subst)])))
+
+
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt b/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt
index 95d095df..45089567 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt
@@ -90,7 +90,8 @@
       ;; FIXME - this sucks and should die
       [t:type-refinement
        (match (lookup-id-type/lexical #'t.predicate)
-              [(and t (Function: (list (arr: (list dom) (Values: (list (Result: rng _ _))) #f #f '()))))
+              [(and t (Fun: (list (Arrow: (list dom) #f '()
+                                          (Values: (list (Result: rng _ _)))))))
                (let ([new-t (make-pred-ty (list dom)
                                           rng
                                           (make-Refinement dom #'t.predicate))])
@@ -236,7 +237,7 @@
 ;; typecheck the expressions of a module-top-level form
 ;; no side-effects
 ;; syntax? -> (or/c 'no-type tc-results/c)
-(define (tc-toplevel/pass2 form [expected (tc-any-results -tt)])
+(define (tc-toplevel/pass2 form [expected (-tc-any-results -tt)])
   
   (do-time (format "pass2 ~a line ~a"
                    (if #t
@@ -358,15 +359,15 @@
   ;; Register signatures in the signature environment
   ;; but defer type parsing to allow mutually recursive refernces
   ;; between signatures and type aliases
-  (for ([sig-form signature-defs])
+  (for ([sig-form (in-list signature-defs)])
     (parse-and-register-signature! sig-form))
 
   (define-values (type-alias-names type-alias-map)
     (get-type-alias-info type-aliases))
 
   ;; Add the struct names to the type table, but not with a type
-  (let ((names (map name-of-struct struct-defs))
-        (type-vars (map type-vars-of-struct struct-defs)))
+  (let ([names (map name-of-struct struct-defs)]
+        [type-vars (map type-vars-of-struct struct-defs)])
     (for ([name (in-list names)]
           [tvars (in-list type-vars)])
       (register-resolved-type-alias
diff --git a/typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt b/typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt
index 9d8842cb..ef714ae1 100644
--- a/typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt
@@ -153,7 +153,7 @@
                           [did-I-suggest-:print-type-already? " ..."]
                           [else (set! did-I-suggest-:print-type-already? #t)
                                 :print-type-message]))]
-           [(tc-results: t)
+           [(tc-results: (list (tc-result: t) ...) #f)
             (define tcs (map cleanup-type t))
             (define tgs (map generalize tcs))
             (define tgs-val (make-Values (map -result tgs)))
diff --git a/typed-racket-lib/typed-racket/types/abbrev.rkt b/typed-racket-lib/typed-racket/types/abbrev.rkt
index 9a207d0f..3d8bdd3f 100644
--- a/typed-racket-lib/typed-racket/types/abbrev.rkt
+++ b/typed-racket-lib/typed-racket/types/abbrev.rkt
@@ -22,7 +22,7 @@
          (for-syntax racket/base syntax/parse))
 
 (provide (all-defined-out)
-         (except-out (all-from-out "base-abbrev.rkt" "match-expanders.rkt") make-arr))
+         (all-from-out "base-abbrev.rkt" "match-expanders.rkt"))
 
 ;; Convenient constructors
 (define -App make-App)
@@ -151,10 +151,10 @@
   (make-Struct name parent flds proc poly pred))
 
 ;; Function type constructors
-(define/decl top-func (make-Function (list)))
+(define/decl top-func (make-Fun (list)))
 
 (define (asym-pred dom rng prop)
-  (make-Function (list (make-arr* (list dom) rng #:props prop))))
+  (make-Fun (list (-Arrow (list dom) rng #:props prop))))
 
 (define/cond-contract make-pred-ty
   (c:case-> (c:-> Type? Type?)
@@ -173,8 +173,9 @@
 
 (define (opt-fn args opt-args result #:rest [rest #f] #:kws [kws null])
   (apply cl->* (for/list ([i (in-range (add1 (length opt-args)))])
-                 (make-Function (list (make-arr* (append args (take opt-args i)) result
-                                                 #:rest rest #:kws kws))))))
+                 (make-Fun (list (-Arrow (append args (take opt-args i))
+                                         result
+                                         #:rest rest #:kws kws))))))
 
 (define-syntax-rule (->opt args ... [opt ...] res)
   (opt-fn (list args ...) (list opt ...) res))
@@ -247,4 +248,4 @@
     [(_ x:id t p)
      (syntax/loc stx
        (let ([x (genid (syntax->datum #'x))])
-         (-refine t (abstract-names p (list x)))))]))
+         (-refine t (abstract-obj p (list x)))))]))
diff --git a/typed-racket-lib/typed-racket/types/base-abbrev.rkt b/typed-racket-lib/typed-racket/types/base-abbrev.rkt
index aa379cf6..137bdee4 100644
--- a/typed-racket-lib/typed-racket/types/base-abbrev.rkt
+++ b/typed-racket-lib/typed-racket/types/base-abbrev.rkt
@@ -102,20 +102,23 @@
                                -Weak-HashTableTop))
 
 ;; Function types
-(define/cond-contract (make-arr* dom rng
-                                 #:rest [rest #f] #:drest [drest #f] #:kws [kws null]
-                                 #:props [props -tt-propset] #:object [obj -empty-obj])
+(define/cond-contract (-Arrow dom rng
+                              #:rest [rst #f]
+                              #:kws [kws null]
+                              #:props [props -tt-propset]
+                              #:object [obj -empty-obj])
   (c:->* ((c:listof Type?) (c:or/c SomeValues? Type?))
-         (#:rest (c:or/c #f Type?)
-          #:drest (c:or/c #f (c:cons/c Type? symbol?))
+         (#:rest (c:or/c #f Type? RestDots?)
           #:kws (c:listof Keyword?)
           #:props PropSet?
           #:object OptObject?)
-         arr?)
-  (make-arr dom (if (Type? rng)
-                    (make-Values (list (-result rng props obj)))
-                    rng)
-            rest drest (sort #:key Keyword-kw kws keyword<?)))
+         Arrow?)
+  (make-Arrow dom
+              rst
+              (sort kws Keyword<?)
+              (if (Type? rng)
+                  (make-Values (list (-result rng props obj)))
+                  rng)))
 
 (define-syntax (->* stx)
   (define-syntax-class c
@@ -123,22 +126,22 @@
   (syntax-parse stx
     [(_ dom rng)
      (syntax/loc stx
-       (make-Function (list (make-arr* dom rng))))]
+       (make-Fun (list (-Arrow dom rng))))]
     [(_ dom rst rng)
      (syntax/loc stx
-       (make-Function (list (make-arr* dom rng #:rest rst))))]
+       (make-Fun (list (-Arrow dom rng #:rest rst))))]
     [(_ dom rng :c props)
      (syntax/loc stx
-       (make-Function (list (make-arr* dom rng #:props props))))]
+       (make-Fun (list (-Arrow dom rng #:props props))))]
     [(_ dom rng _:c props _:c object)
      (syntax/loc stx
-       (make-Function (list (make-arr* dom rng #:props props #:object object))))]
+       (make-Fun (list (-Arrow dom rng #:props props #:object object))))]
     [(_ dom rst rng _:c props)
      (syntax/loc stx
-       (make-Function (list (make-arr* dom rng #:rest rst #:props props))))]
+       (make-Fun (list (-Arrow dom rng #:rest rst #:props props))))]
     [(_ dom rst rng _:c props : object)
      (syntax/loc stx
-       (make-Function (list (make-arr* dom rng #:rest rst #:props props #:object object))))]))
+       (make-Fun (list (-Arrow dom rng #:rest rst #:props props #:object object))))]))
 
 (define-syntax (-> stx)
   (define-syntax-class c
@@ -159,30 +162,34 @@
     [(_ dom rng) (syntax/loc stx (->* dom rng))]
     [(_ dom (dty dbound) rng)
      (syntax/loc stx
-       (make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound)))))]
+       (make-Fun
+        (list (-Arrow dom rng #:rest (make-RestDots dty 'dbound)))))]
     [(_ dom rng (~datum :) props)
      (syntax/loc stx
        (->* dom rng (~datum :) props))]
     [(_ dom (dty dbound) rng (~datum :) props)
      (syntax/loc stx
-       (make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound) #:props props))))]))
+       (make-Fun
+        (list (-Arrow dom rng
+                      #:rest (make-RestDots dty 'dbound)
+                      #:props props))))]))
 
 (define (simple-> doms rng)
   (->* doms rng))
 
 (define (->acc dom rng path #:var [var (cons 0 0)])
   (define obj (-acc-path path (-id-path var)))
-  (make-Function
-   (list (make-arr* dom rng
-                    #:props (-PS (-not-type obj (-val #f))
-                                 (-is-type obj (-val #f)))
-                    #:object obj))))
+  (make-Fun
+   (list (-Arrow dom rng
+                 #:props (-PS (-not-type obj (-val #f))
+                              (-is-type obj (-val #f)))
+                 #:object obj))))
 
 (define (cl->* . args)
   (define (funty-arities f)
     (match f
-      [(Function: as) as]))
-  (make-Function (apply append (map funty-arities args))))
+      [(Fun: as) as]))
+  (make-Fun (apply append (map funty-arities args))))
 
 (define-syntax (cl-> stx)
   (syntax-parse stx
@@ -194,13 +201,12 @@
   (syntax-parse stx
     [(_ ty:expr ... (~seq k:keyword kty:expr opt:boolean) ... rng)
      (syntax/loc stx
-       (make-Function
+       (make-Fun
         (list
-         (make-arr* (list ty ...)
-                    rng
-                    #:kws (sort #:key (match-lambda [(Keyword: kw _ _) kw])
-                                (list (make-Keyword 'k kty opt) ...)
-                                keyword<?)))))]))
+         (-Arrow (list ty ...)
+                 rng
+                 #:kws (sort (list (make-Keyword 'k kty opt) ...)
+                             Keyword<?)))))]))
 
 (define-syntax (->optkey stx)
   (syntax-parse stx
@@ -209,16 +215,15 @@
        (with-syntax ([((extra ...) ...)
                       (for/list ([i (in-range (add1 (length l)))])
                         (take l i))]
-                     [(rsts ...) (for/list ([i (in-range (add1 (length l)))]) #'rst)])
+                     [(rst ...) (for/list ([i (in-range (add1 (length l)))]) #'rst)])
          (syntax/loc stx
-           (make-Function
+           (make-Fun
             (list
-             (make-arr* (list ty ... extra ...)
-                        rng
-                        #:rest rsts
-                        #:kws (sort #:key (match-lambda [(Keyword: kw _ _) kw])
-                                    (list (make-Keyword 'k kty opt) ...)
-                                    keyword<?))
+             (-Arrow (list ty ... extra ...)
+                     rng
+                     #:rest rst
+                     #:kws (sort (list (make-Keyword 'k kty opt) ...)
+                                 Keyword<?))
              ...)))))]
     [(_ ty:expr ... [oty:expr ...] (~seq k:keyword kty:expr opt:boolean) ... rng)
      (let ([l (syntax->list #'(oty ...))])
@@ -226,18 +231,16 @@
                       (for/list ([i (in-range (add1 (length l)))])
                         (take l i))])
          (syntax/loc stx
-           (make-Function
+           (make-Fun
             (list
-             (make-arr* (list ty ... extra ...)
+             (-Arrow (list ty ... extra ...)
                         rng
-                        #:rest #f
-                        #:kws (sort #:key (match-lambda [(Keyword: kw _ _) kw])
-                                    (list (make-Keyword 'k kty opt) ...)
-                                    keyword<?))
+                        #:kws (sort (list (make-Keyword 'k kty opt) ...)
+                                    Keyword<?))
              ...)))))]))
 
 (define (make-arr-dots dom rng dty dbound)
-  (make-arr* dom rng #:drest (cons dty dbound)))
+  (-Arrow dom rng #:rest (make-RestDots dty dbound)))
 
 ;; Convenient syntax for polymorphic types
 (define-syntax -poly
diff --git a/typed-racket-lib/typed-racket/types/kw-types.rkt b/typed-racket-lib/typed-racket/types/kw-types.rkt
index 80874092..ef043b0c 100644
--- a/typed-racket-lib/typed-racket/types/kw-types.rkt
+++ b/typed-racket-lib/typed-racket/types/kw-types.rkt
@@ -1,24 +1,20 @@
 #lang racket/base
 
-(require "abbrev.rkt"
-         "../rep/core-rep.rkt"
-         "../rep/type-rep.rkt"
-         "../rep/values-rep.rkt"
-         "../utils/tc-utils.rkt"
-         "../base-env/annotate-classes.rkt"
-         "tc-result.rkt"
+(require "../utils/utils.rkt"
+         (utils tc-utils)
+         (types abbrev tc-result)
+         (rep core-rep type-rep values-rep)
+         (base-env annotate-classes)
          racket/list racket/set racket/match
          racket/format racket/string
-         racket/dict
          syntax/parse)
 
 ;; convert : [Listof Keyword] [Listof Type] [Listof Type] [Option Type]
 ;;           [Option Type] [Option (Pair Type symbol)] boolean -> Type
-(define (convert kw-ts plain-ts opt-ts rng rest drest split?)
-  (when drest
-    (int-err "drest passed to kw-convert"))
+(define (convert kw-ts plain-ts opt-ts rng rst split?)
+  (when (RestDots? rst) (int-err "RestDots passed to kw-convert"))
   ;; the kw function protocol passes rest args as an explicit list
-  (define rest-type (if rest (list (-lst rest)) empty))
+  (define rst-type (if rst (list (-lst rst)) empty))
 
   ;; the kw protocol puts the arguments in keyword-sorted order in the
   ;; function header, so we need to sort the types to match
@@ -26,7 +22,7 @@
     (sort kw-ts (λ (kw1 kw2) (keyword<? (Keyword-kw kw1)
                                        (Keyword-kw kw2)))))
 
-  (make-Function
+  (make-Fun
     (cond
       [(not split?)
        (define ts 
@@ -39,8 +35,8 @@
            plain-ts
            (for/list ([t (in-list opt-ts)]) (-opt t))
            (for/list ([t (in-list opt-ts)]) -Boolean)
-           rest-type)))
-       (list (make-arr* ts rng #:rest rest #:drest drest))]
+           rst-type)))
+       (list (-Arrow ts rng #:rest rst))]
       [else
        ;; The keyword argument types including boolean flags for
        ;; optional keyword arguments
@@ -59,9 +55,8 @@
        ;; Add boolean arguments for the optional type flaggs.
        (define opt-flags (make-list (length opt-ts) -Boolean))
 
-       (list (make-arr* (append kw-args plain-ts opt-ts opt-flags rest-type)
-                        rng
-                        #:drest drest))])))
+       (list (-Arrow (append kw-args plain-ts opt-ts opt-flags rst-type)
+                     rng))])))
 
 ;; This is used to fix the props of keyword types.
 ;; TODO: This should also explore deeper into the actual types and remove props in there as well.
@@ -70,54 +65,43 @@
 (define (erase-props/Values values)
   (match values
     [(AnyValues: _) ManyUniv]
-    [(Results: ts fs os)
-     (-values ts)]
-    [(Results: ts fs os dty dbound)
-     (-values-dots ts dty dbound)]))
+    [(Values: rs)
+     (make-Values
+      (map (match-lambda
+             [(Result: t _ _) (-result t)])
+           rs))]
+    [(ValuesDots: rs dty dbound)
+     (make-ValuesDots (make-Values
+                       (map (match-lambda
+                              [(Result: t _ _) (-result t)])
+                            rs))
+                      dty
+                      dbound)]))
 
 
 (define (prefix-of a b)
-  (define (rest-equal? a b)
-    (match* (a b)
-      [(a a) #t]
-      [(#f _) #f]
-      [(_ #f) #f]
-      [(_ _) #f]))
-  (define (drest-equal? a b)
-    (match* (a b)
-      [((list t b) (list t b)) #t]
-      [(#f #f) #t]
-      [(_ _) #f]))
   (match* (a b)
-    [((arr: args result rest drest kws)
-      (arr: args* result* rest* drest* kws*))
-     (and (< (length args) (length args*))
-          (rest-equal? rest rest*)
-          (drest-equal? drest drest*)
-          (equal? result result*)
-          (equal? kws kws*)
-          (for/and ([p (in-list args)]
-                    [p* (in-list args*)])
-            (equal? p p*)))]))
-
-(define (arity-length a)
-  (match a
-    [(arr: args _ _ _ _) (length args)]))
-
+    [((Arrow: args1 rst kws rng)
+      (Arrow: args2 rst kws rng))
+     (and (< (length args1) (length args2))
+          (for/and ([t1 (in-list args1)]
+                    [t2 (in-list args2)])
+            (equal? t1 t2)))]
+    [(_ _) #f]))
 
 (define (arg-diff a1 a2)
-  (match a2
-    [(arr: args _ _ _ _) (drop args (arity-length a1))]))
+  (drop (Arrow-dom a2)
+        (length (Arrow-dom a1))))
 
 (define (find-prefixes l)
-  (define l* (sort l (λ (arr1 arr2) (< (arity-length arr1)
-                                       (arity-length arr2)))))
+  (define l* (sort l (λ (a1 a2) (< (length (Arrow-dom a1))
+                                   (length (Arrow-dom a2))))))
   (for/fold ([d '()]) ([e (in-list l*)])
-    (define prefix (for/or ([p (in-dict-keys d)])
+    (define prefix (for/or ([(p _) (in-assoc d)])
                      (and (prefix-of p e) p)))
     (if prefix
-        (dict-set d prefix (arg-diff prefix e))
-        (dict-set d e null))))
+        (assoc-set d prefix (arg-diff prefix e))
+        (assoc-set d e null))))
 
 ;; handle-extra-or-missing-kws : (Listof Keyword) LambdaKeywords
 ;;                               -> (Listof Keyword)
@@ -147,13 +131,13 @@
     ;; use for/list and remove duplicates afterwards instead of
     ;; set and set->list to retain determinism
     (remove-duplicates
-     (for/list ([(k v) (in-dict table)])
+     (for/list ([(k v) (in-assoc table)])
        (match k
-         [(arr: mand rng rest drest kws)
+         [(Arrow: mand rst kws rng)
           (define kws* (if actual-kws
                            (handle-extra-or-missing-kws kws actual-kws)
                            kws))
-          (convert kws* mand v rng rest drest split?)]))))
+          (convert kws* mand v rng rst split?)]))))
   (apply cl->* fns))
 
 ;; kw-convert : Type (Option LambdaKeywords) [Boolean] -> Type
@@ -161,7 +145,7 @@
 ;; function protocol
 (define (kw-convert ft actual-kws #:split [split? #f])
   (match ft
-    [(Function: arrs)
+    [(Fun: arrs)
      (inner-kw-convert arrs actual-kws split?)]
     [(Poly-names: names f)
      (make-Poly names (kw-convert f actual-kws #:split split?))]
@@ -199,9 +183,9 @@
   (define non-kw-argc (+ raw-non-kw-argc opt-non-kw-argc))
   (define mand-non-kw-argc (- non-kw-argc (* 2 opt-non-kw-argc)))
   (match ft
-    [(Function: arrs)
+    [(Fun: arrs)
      (cond [(= (length arrs) 1) ; no optional args (either kw or not)
-            (match-define (arr: doms rng _ _ _) (car arrs))
+            (match-define (Arrow: doms _ _ rng) (car arrs))
             (define kw-length
               (- (length doms) (+ non-kw-argc (if rest? 1 0))))
             (define-values (kw-args other-args) (split-at doms kw-length))
@@ -211,17 +195,17 @@
                 (make-Keyword kw kw-type #t)))
             (define rest-type
               (and rest? (last other-args)))
-            (make-Function
-             (list (make-arr* (take other-args non-kw-argc)
-                              (erase-props/Values rng)
-                              #:kws actual-kws
-                              #:rest rest-type)))]
+            (make-Fun
+             (list (-Arrow (take other-args non-kw-argc)
+                           (erase-props/Values rng)
+                           #:kws actual-kws
+                           #:rest rest-type)))]
            [(and (even? (length arrs)) ; had optional args
                  (>= (length arrs) 2))
             ;; assumption: only one arr is needed, since the types for
             ;; the actual domain are the same (the difference is in the
             ;; second type for the optional keyword protocol)
-            (match-define (arr: doms rng _ _ _) (car arrs))
+            (match-define (Arrow: doms _ _ rng) (car arrs))
             (define kw-length
               (- (length doms) (+ non-kw-argc (if rest? 1 0))))
             (define kw-args (take doms kw-length))
@@ -232,12 +216,12 @@
             (define rest-type
               (and rest? (last opt-and-rest-args)))
             (define opt-types (take opt-and-rest-args opt-non-kw-argc))
-            (make-Function
+            (make-Fun
              (for/list ([to-take (in-range (add1 (length opt-types)))])
-               (make-arr* (append mand-args (take opt-types to-take))
-                          (erase-props/Values rng)
-                          #:kws actual-kws
-                          #:rest rest-type)))]
+               (-Arrow (append mand-args (take opt-types to-take))
+                       (erase-props/Values rng)
+                       #:kws actual-kws
+                       #:rest rest-type)))]
            [else (int-err "unsupported arrs in keyword function type")])]
     [_ (int-err "unsupported keyword function type")]))
 
@@ -250,9 +234,9 @@
   (match-define (lambda-kws actual-mands actual-opts) kw-prop)
   (define arrs
     (match f-type
-      [(AnyPoly-names: _ _ (Function: arrs)) arrs]))
-  (for/and ([arr (in-list arrs)])
-    (match-define (arr: _ _ _ _ kws) arr)
+      [(AnyPoly-names: _ _ (Fun: arrs)) arrs]))
+  (for*/and ([arr (in-list arrs)]
+             [kws (in-value (Arrow-kws arr))])
     (define-values (mand-kw-types opt-kw-types) (partition-kws kws))
     (define mand-kws (map Keyword-kw mand-kw-types))
     (define opt-kws (map Keyword-kw opt-kw-types))
@@ -304,7 +288,7 @@
 
 (define ((opt-convert-arr required-pos optional-pos) arr)
   (match arr
-    [(arr: args result #f #f '())
+    [(Arrow: args #f '() result)
      (define num-args (length args))
      (and (>= num-args required-pos)
           (<= num-args (+ required-pos optional-pos))
@@ -313,24 +297,21 @@
                  [missing-opt-args (- (+ required-pos optional-pos) num-args)]
                  [present-flags (map (λ (t) (-val #t)) opt-args)]
                  [missing-args (make-list missing-opt-args (-val #f))])
-            (make-arr (append required-args
-                              opt-args
-                              missing-args
-                              present-flags
-                              missing-args)
-                      result
-                      #f
-                      #f
-                      '())))]
-    [(arr: args result _ _ _) #f]))
+            (-Arrow (append required-args
+                            opt-args
+                            missing-args
+                            present-flags
+                            missing-args)
+                    result)))]
+    [_ #f]))
 
 (define (opt-convert ft required-pos optional-pos)
   (let loop ([ft ft])
     (match ft
-      [(Function: arrs)
+      [(Fun: arrs)
        (let ([arrs (map (opt-convert-arr required-pos optional-pos) arrs)])
          (and (andmap values arrs)
-              (make-Function arrs)))]
+              (make-Fun arrs)))]
       [(Poly-names: names f)
        (match (loop f)
          [#f #f]
@@ -367,19 +348,19 @@
   (define argc (+ raw-argc opt-argc))
   (define mand-argc (- argc (* 2 opt-argc)))
   (match ft
-    [(Function: arrs)
+    [(Fun: arrs)
      (cond [(and (even? (length arrs)) (>= (length arrs) 2))
-            (match-define (arr: doms rng _ _ _) (car arrs))
+            (match-define (Arrow: doms _ _ rng) (car arrs))
             (define-values (mand-args opt-and-rest-args)
               (split-at doms mand-argc))
             (define rest-type
               (and rest? (last opt-and-rest-args)))
             (define opt-types (take opt-and-rest-args opt-argc))
-            (make-Function
+            (make-Fun
              (for/list ([to-take (in-range (add1 (length opt-types)))])
-               (make-arr* (append mand-args (take opt-types to-take))
-                          rng
-                          #:rest rest-type)))]
+               (-Arrow (append mand-args (take opt-types to-take))
+                       rng
+                       #:rest rest-type)))]
            [else (int-err "unsupported arrs in keyword function type")])]
     [_ (int-err "unsupported keyword function type")]))
 
diff --git a/typed-racket-lib/typed-racket/types/match-expanders.rkt b/typed-racket-lib/typed-racket/types/match-expanders.rkt
index 326fe58c..a0d2c294 100644
--- a/typed-racket-lib/typed-racket/types/match-expanders.rkt
+++ b/typed-racket-lib/typed-racket/types/match-expanders.rkt
@@ -8,7 +8,7 @@
          (types resolve base-abbrev)
          (for-syntax racket/base syntax/parse))
 
-(provide Listof: List: MListof: AnyPoly: AnyPoly-names: Function/arrs:
+(provide Listof: List: MListof: AnyPoly: AnyPoly-names:
          SimpleListof: SimpleMListof:
          PredicateProp:
          Val-able:
@@ -75,7 +75,7 @@
       [(Mu-unsafe:
         (Union: (== -Null)
                 (list (pair-matcher elem-t (B: 0)))))
-       (define elem-t* (instantiate-raw-type t elem-t))
+       (define elem-t* (instantiate-type elem-t t))
        (cond
          [simple? (and (equal? elem-t elem-t*) elem-t)]
          [else elem-t*])]
@@ -161,11 +161,6 @@
       [(_ vars dotted-vars body)
        #'(app unpoly-names vars dotted-vars body)])))
 
-(define-match-expander Function/arrs:
-  (lambda (stx)
-    (syntax-parse stx
-      [(_ doms rngs rests drests kws (~optional (~seq #:arrs arrs) #:defaults ([arrs #'_])))
-       #'(Function: (and arrs (list (arr: doms rngs rests drests kws) (... ...))))])))
 
 ;; A match expander for matching the prop on a predicate. This assumes a standard
 ;; predicate type of the shape (-> Any Any : SomeType)
@@ -173,4 +168,7 @@
   (λ (stx)
     (syntax-parse stx
       [(_ ps)
-       #'(Function: (list (arr: (list _) (Values: (list (Result: _ ps _))) _ _ _)))])))
+       #'(Fun: (list (Arrow: (list _)
+                             _
+                             _
+                             (Values: (list (Result: _ ps _))))))])))
diff --git a/typed-racket-lib/typed-racket/types/overlap.rkt b/typed-racket-lib/typed-racket/types/overlap.rkt
index eb16c3a5..637f0701 100644
--- a/typed-racket-lib/typed-racket/types/overlap.rkt
+++ b/typed-racket-lib/typed-racket/types/overlap.rkt
@@ -125,7 +125,7 @@
      (Val-able: (? simple-datum? v2)))
     (equal? v1 v2)]
    [((Val-able: (? simple-datum?))
-     (or (? Struct?) (? StructTop?) (? Function?)))
+     (or (? Struct?) (? StructTop?) (? Fun?)))
     #:no-order
     #f]
    [((Val-able: (not (? hash?)))
diff --git a/typed-racket-lib/typed-racket/types/path-type.rkt b/typed-racket-lib/typed-racket/types/path-type.rkt
index 40cbfdb5..c5259dae 100644
--- a/typed-racket-lib/typed-racket/types/path-type.rkt
+++ b/typed-racket-lib/typed-racket/types/path-type.rkt
@@ -77,7 +77,7 @@
       [((Distinction: _ _ t) _) (path-type path t resolved)]
 
       ;; for private fields in classes
-      [((Function: (list (arr: doms (Values: (list (Result: rng _ _))) _ _ _)))
+      [((Fun: (list (Arrow: doms _ _ (Values: (list (Result: rng _ _))))))
         (cons (FieldPE:) rst))
        (path-type rst rng (hash))]
 
diff --git a/typed-racket-lib/typed-racket/types/printer.rkt b/typed-racket-lib/typed-racket/types/printer.rkt
index 1779604a..49a8c254 100644
--- a/typed-racket-lib/typed-racket/types/printer.rkt
+++ b/typed-racket-lib/typed-racket/types/printer.rkt
@@ -267,7 +267,7 @@
 ;; Convert an arr (see type-rep.rkt) to its printable form
 (define (arr->sexp arr)
   (match arr
-    [(arr: dom rng rest drest kws)
+    [(Arrow: dom rest kws rng)
      (append
       (list '->)
       (map type->sexp dom)
@@ -281,8 +281,11 @@
            (if req?
                (format "~a ~a" k (type->sexp t))
                (format "[~a ~a]" k (type->sexp t)))]))
-      (if rest  `(,(type->sexp rest) *)                       null)
-      (if drest `(,(type->sexp (car drest)) ... ,(cdr drest)) null)
+      (match rest
+        [(? Type?) `(,(type->sexp rest) *)]
+        [(RestDots: dty dbound)
+         `(,(type->sexp dty) ... ,dbound)]
+        [_ null])
       (match rng
         [(AnyValues: (? TrueProp?)) '(AnyValues)]
         [(AnyValues: p) `(AnyValues : ,(prop->sexp p))]
@@ -334,8 +337,8 @@
   ;; see type-contract.rkt, which does something similar and this code
   ;; was stolen from/inspired by/etc.
   (match* ((first arrs) (last arrs))
-    [((arr: first-dom rng rst _ kws)
-      (arr: last-dom _ _ _ _))
+    [((Arrow: first-dom rst kws rng)
+      (Arrow: last-dom _ _ _))
      (define-values (mand-kws opt-kws) (partition-kws kws))
      (define opt-doms (drop last-dom (length first-dom)))
      `(->*
@@ -383,8 +386,8 @@
 ;; Convert a case-> type to an s-expression
 (define (case-lambda->sexp type)
   (match type
-    [(Function: arities)
-     (match arities
+    [(Fun: arrows)
+     (match arrows
        [(list) '(case->)]
        [(list a) (arr->sexp a)]
        [(and arrs (list a b ...))
@@ -549,11 +552,11 @@
      `#(,(string->symbol (format "struct:~a" (syntax-e nm)))
         ,(map t->s t)
         ,@(if proc (list (t->s proc)) null))]
-    [(Function: arities)
+    [(? Fun?)
      (parameterize ([current-print-type-fuel
                      (sub1 (current-print-type-fuel))])
        (case-lambda->sexp type))]
-    [(arr: _ _ _ _ _) `(arr ,(arr->sexp type))]
+    [(? Arrow?) `(Arrow ,(arr->sexp type))]
     [(Vector: e) `(Vectorof ,(t->s e))]
     [(HeterogeneousVector: e) `(Vector ,@(map t->s e))]
     [(Box: e) `(Boxof ,(t->s e))]
diff --git a/typed-racket-lib/typed-racket/types/prop-ops.rkt b/typed-racket-lib/typed-racket/types/prop-ops.rkt
index a3cc52af..54660af3 100644
--- a/typed-racket-lib/typed-racket/types/prop-ops.rkt
+++ b/typed-racket-lib/typed-racket/types/prop-ops.rkt
@@ -18,7 +18,7 @@
   [atomic-complement? (c:-> Prop? Prop? boolean?)]
   [atomic-contradiction? (c:-> Prop? Prop? boolean?)]
   [contradiction? (c:-> Prop? Prop? boolean?)]
-  [add-unconditional-prop-all-args (c:-> Function? Type? Function?)]
+  [add-unconditional-prop-all-args (c:-> Fun? Type? Fun?)]
   [add-unconditional-prop (c:-> tc-results/c Prop? tc-results/c)]
   [erase-props (c:-> tc-results/c tc-results/c)]
   [reduce-propset/type (c:-> PropSet? Type? PropSet?)]
@@ -42,27 +42,27 @@
 ;; return type in the proposition (i.e. if it
 ;; can't be False, then the else prop should be -ff)
 (define (reduce-tc-results/subsumption res)
-  (define (update-ps t ps obj)
-    (cond
-      [(Bottom? t) (tc-result t -ff-propset -empty-obj)]
-      [else
-       (define p+ (if ps (PropSet-thn ps) -tt))
-       (define p- (if ps (PropSet-els ps) -tt))
-       (define o (if obj obj -empty-obj))
+  (define (update-ps tcr)
+    (match tcr
+      [(tc-result: t ps obj)
        (cond
-         [(or (equal? -False t)
-              (FalseProp? p+))
-          (tc-result (intersect t -False) (-PS -ff p-) o)]
-         [(not (overlap? t -False))
-          (tc-result t (-PS p+ -ff) o)]
-         [(FalseProp? p-) (tc-result (subtract t -False) (-PS p+ -ff) o)]
-         [else (tc-result t (-PS p+ p-) o)])]))
+         [(Bottom? t) (-tc-result t -ff-propset -empty-obj)]
+         [else
+          (define p+ (if ps (PropSet-thn ps) -tt))
+          (define p- (if ps (PropSet-els ps) -tt))
+          (define o (if obj obj -empty-obj))
+          (cond
+            [(or (equal? -False t)
+                 (FalseProp? p+))
+             (-tc-result (intersect t -False) (-PS -ff p-) o)]
+            [(not (overlap? t -False))
+             (-tc-result t (-PS p+ -ff) o)]
+            [(FalseProp? p-) (-tc-result (subtract t -False) (-PS p+ -ff) o)]
+            [else (-tc-result t (-PS p+ p-) o)])])]))
   (match res
     [(tc-any-results: _) res]
-    [(tc-results: ts pss os)
-     (tc-results (map update-ps ts pss os) #f)]
-    [(tc-results: ts pss os dt db)
-     (tc-results (map update-ps ts pss os) (cons dt db))]))
+    [(tc-results: tcrs db)
+     (-tc-results (map update-ps tcrs) db)]))
 
 
 ;; atomic-contradiction?: Prop? Prop? -> boolean?
@@ -395,53 +395,40 @@
 ;; Ands the given proposition to the props in the tc-results.
 ;; Useful to express properties of the form: if this expressions returns at all, we learn this
 (define/match (add-unconditional-prop results prop)
-  [((tc-any-results: p) prop) (tc-any-results (-and prop p))]
-  [((tc-results: ts (list (PropSet: ps+ ps-) ...) os) prop)
-   (ret ts
-        (for/list ([p+ (in-list ps+)]
-                   [p- (in-list ps-)])
-          (-PS (-and prop p+) (-and prop p-)))
-        os)]
-  [((tc-results: ts (list (PropSet: ps+ ps-) ...) os dty dbound) prop)
-   (ret ts
-        (for/list ([p+ (in-list ps+)] [p- (in-list ps-)])
-          (-PS (-and prop p+) (-and prop p-)))
-        os
-        dty
-        dbound)])
+  [((tc-any-results: p) prop) (-tc-any-results (-and prop p))]
+  [((tc-results: tcrs db) prop)
+   (-tc-results
+    (map (match-lambda
+           [(tc-result: t (PropSet: p+ p-) o)
+            (-tc-result t (-PS (-and prop p+) (-and prop p-)) o)])
+         tcrs)
+    db)])
 
 
 ;; ands the given type prop to both sides of the given arr for each argument
 ;; useful to express properties of the form: if this function returns at all,
 ;; we learn this about its arguments (like fx primitives, or car/cdr, etc.)
 (define/match (add-unconditional-prop-all-args arr type)
-  [((Function: (list (arr: dom rng rest drest kws))) type)
+  [((Fun: (list (Arrow: dom rest kws rng))) type)
    (match rng
-     [(Values: (list (Result: tp (PropSet: -true-prop -false-prop) op)))
+     [(Values: (list (Result: tp (PropSet: p+ p-) op)))
       (let ([new-props (apply -and (build-list (length dom)
                                                (lambda (i)
                                                  (-is-type i type))))])
-        (make-Function
-         (list (make-arr
-                dom
-                (make-Values
-                 (list (-result tp
-                                (-PS (-and -true-prop new-props)
-                                     (-and -false-prop new-props))
-                                op)))
-                rest drest kws))))])])
+        (make-Fun
+         (list (make-Arrow dom rest kws
+                           (make-Values
+                            (list (-result tp
+                                           (-PS (-and p+ new-props)
+                                                (-and p- new-props))
+                                           op)))))))])])
 
 ;; tc-results/c -> tc-results/c
 (define/match (erase-props tc)
-  [((tc-any-results: _)) (tc-any-results #f)]
-  [((tc-results: ts _ _))
-   (define empties (make-list (length ts) #f))
-   (ret ts
-        empties
-        empties)]
-  [((tc-results: ts _ _ dty dbound))
-   (define empties (make-list (length ts) #f))
-   (ret ts
-        empties
-        empties
-        dty dbound)])
+  [((tc-any-results: _)) (-tc-any-results #f)]
+  [((tc-results: tcrs dbound))
+   (-tc-results
+    (map (match-lambda
+           [(tc-result: t) (-tc-result t #f #f)])
+         tcrs)
+    dbound)])
diff --git a/typed-racket-lib/typed-racket/types/substitute.rkt b/typed-racket-lib/typed-racket/types/substitute.rkt
index d8d06de1..f9aaaeb3 100644
--- a/typed-racket-lib/typed-racket/types/substitute.rkt
+++ b/typed-racket-lib/typed-racket/types/substitute.rkt
@@ -44,40 +44,14 @@
   (let sub ([target target])
     (match target
       [(F: name) (hash-ref subst name target)]
-      [(arr: dom rng rest drest kws)
-       (cond
-         [(and (pair? drest)
-               (ormap (λ (name) (and (equal? name (cdr drest))
-                                     (not (bound-tvar? name))
-                                     name))
-                      names))
-          =>
-          (λ (name)
-            (int-err "substitute used on ... variable ~a in type ~a" name target))]
-         [else
-          (make-arr (map sub dom)
-                    (sub rng)
-                    (and rest (sub rest))
-                    (and drest (cons (sub (car drest)) (cdr drest)))
-                    (map sub kws))])]
-      [(ValuesDots: types dty dbound)
-       (cond
-         [(for/or ([name (in-list names)])
-            (and (equal? dbound name)
-                 (not (bound-tvar? name))))
-          =>
-          (λ (name)
-            (int-err "substitute used on ... variable ~a in type ~a" name target))]
-         [else (make-ValuesDots (map sub types) (sub dty) dbound)])]
-      [(ListDots: dty dbound)
-       (cond
-         [(for/or ([name (in-list names)])
-            (and (equal? dbound name)
-                 (not (bound-tvar? name))))
-          =>
-          (λ (name)
-            (int-err "substitute used on ... variable ~a in type ~a" name target))]
-         [else (make-ListDots (sub dty) dbound)])]
+      [(or (RestDots: _     dbound)
+           (ListDots: _     dbound)
+           (ValuesDots: _ _ dbound))
+       #:when (and (memq dbound names)
+                   (not (bound-tvar? dbound)))
+       (int-err "substitute used on ... variable ~a in type ~a"
+                dbound
+                target)]
       [_ (Rep-fmap target sub)])))
 
 
@@ -117,26 +91,18 @@
                  (for/list ([img (in-list images)])
                    (-result (substitute img name expanded))))))])]
          [else (make-ValuesDots (map sub types) (sub dty) dbound)])]
-      [(arr: dom rng rest drest kws)
-       (cond
-         [(and (pair? drest)
-               (eq? name (cdr drest)))
-          (make-arr (append
-                     (map sub dom)
-                     ;; We need to recur first, just to expand out any dotted usages of this.
-                     (let ([expanded (sub (car drest))])
-                       (map (λ (img) (substitute img name expanded))
-                            images)))
-                    (sub rng)
-                    rimage
-                    #f
-                    (map sub kws))]
-         [else
-          (make-arr (map sub dom)
-                    (sub rng)
-                    (and rest (sub rest))
-                    (and drest (cons (sub (car drest)) (cdr drest)))
-                    (map sub kws))])]
+      [(Arrow: dom (RestDots: dty dbound) kws rng)
+       #:when (eq? name dbound)
+       (make-Arrow
+        (append
+         (map sub dom)
+         ;; We need to recur first, just to expand out any dotted usages of this.
+         (let ([expanded (sub dty)])
+           (map (λ (img) (substitute img name expanded))
+                images)))
+        rimage
+        (map sub kws)
+        (sub rng))]
       [_ (Rep-fmap target sub)])))
 
 ;; implements curly brace substitution from the formalism, with the addition
@@ -145,38 +111,27 @@
 (define (substitute-dotted pre-image image image-bound name target)
   (let sub ([target target])
     (match target
+      [(F: name*) #:when (eq? name* name) image]
       [(ValuesDots: types dty dbound)
-       (let ([extra-types (cond
-                            [(eq? name dbound) pre-image]
-                            [else null])])
-         (make-ValuesDots (append (map sub types) (map -result extra-types))
-                          (sub dty)
-                          (cond
-                            [(eq? name dbound) image-bound]
-                            [else dbound])))]
+       #:when (eq? name dbound)
+       (make-ValuesDots (append (map sub types)
+                                (map -result pre-image))
+                        (sub dty)
+                        image-bound)]
       [(ListDots: dty dbound)
        (-Tuple*
         (if (eq? name dbound) pre-image null)
         (make-ListDots (sub dty)
                        (if (eq? name dbound) image-bound dbound)))]
-      [(F: name*)
-       (cond [(eq? name* name) image]
-             [else target])]
-      [(arr: dom rng rest drest kws)
-       (let ([extra-types (cond
-                            [(and drest (eq? name (cdr drest)))
-                             pre-image]
-                            [else null])])
-         (make-arr (append (map sub dom) extra-types)
-                   (sub rng)
-                   (and rest (sub rest))
-                   (and drest
-                        (cons (substitute image (cdr drest) (sub (car drest)))
-                              (cond
-                                [(eq? name (cdr drest))
-                                 image-bound]
-                                [else (cdr drest)])))
-                   (map sub kws)))]
+      [(Arrow: dom (RestDots: dty dbound) kws rng)
+       #:when (eq? name dbound)
+       (make-Arrow
+        (append (map sub dom) pre-image)
+        (make-RestDots
+         (substitute image dbound (sub dty))
+         image-bound)
+        (map sub kws)
+        (sub rng))]
       [_ (Rep-fmap target sub)])))
 
 ;; substitute many variables
diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt
index 93da56f6..44863596 100644
--- a/typed-racket-lib/typed-racket/types/subtype.rkt
+++ b/typed-racket-lib/typed-racket/types/subtype.rkt
@@ -8,7 +8,9 @@
               free-variance rep-switch)
          (utils tc-utils)
          (only-in (env type-env-structs)
-                  with-lexical-env with-naively-extended-lexical-env lexical-env)
+                  with-lexical-env
+                  with-naively-extended-lexical-env
+                  lexical-env)
          (types utils resolve match-expanders current-seen
                 numeric-tower substitute prefab signatures)
          (for-syntax racket/base syntax/parse racket/sequence)
@@ -19,7 +21,7 @@
 
 (lazy-require
  ("../infer/infer.rkt" (infer))
- ("../typecheck/tc-subst.rkt" (restrict-values instantiate-rep/obj))
+ ("../typecheck/tc-subst.rkt" (instantiate-obj+simplify))
  ("../typecheck/tc-envops.rkt" (env+ implies-in-env?)))
 
 
@@ -35,19 +37,22 @@
  [unrelated-structs (-> Struct? Struct? boolean?)])
 
 
-;;************************************************************
-;; Public Interface to Subtyping
-;;************************************************************
-
 ;; When subtype is called w/ no object, we
 ;; us a temporary object to name the arguments.
 ;; This parameter gives us plenty of fresh, temporary names
 ;; to use and this way we don't have to be constantly allocating
 ;; fresh identifiers.
+(define temp-ids
+  (make-parameter (make-id-seq)))
 (define temp-objs
   (make-parameter (make-obj-seq)))
 
+;;************************************************************
+;; Public Interface to Subtyping
+;;************************************************************
+
 ;; is t1 a subtype of t2?
+;; if obj, then we're assuming obj is the subject
 ;; type type -> boolean
 (define (subtype t1 t2 [obj #f])
   (and (subtype* (seen) t1 t2 obj) #t))
@@ -100,11 +105,6 @@
          (λ (A*) (subvals* A* (cdr vs1) (cdr vs2)))]
         [else #f]))
 
-;; check if s is a supertype of any element of ts
-(define (supertype-of-one/arr A s ts)
-  (for/or ([t (in-list ts)])
-    (arr-subtype*/no-fail A t s)))
-
 (define-syntax (let*/and stx)
   (syntax-parse stx
     [(_ () . e) (syntax/loc stx (let () . e))]
@@ -175,68 +175,50 @@
        [(_ _) #f]))))
 
 
-;; combine-arrs
-;;
-;; Checks if this function is defined by an uneccessary case->
-;; matching the following pattern:
-;; τ0 -> σ ∧ τ1 -> σ ∧ τn -> σ ...
-;; and if so, returns the combined function type:
-;; (∪ τ0 τ1 ... τn)-> σ
-;; amk: would it be better to simplify function types ahead of time
-;; for cases like this where there is a preferable normal form?
-(define/cond-contract (combine-arrs arrs)
-  (-> (listof arr?) (or/c #f arr?))
-  (match arrs
-    [(list (and a1 (arr: dom1 rng1 #f #f '())) (arr: dom rng #f #f '()) ...)
-     (cond
-       [(null? dom) (make-arr dom1 rng1 #f #f '())]
-       [(not (apply = 1 (length dom1) (map length dom))) #f]
-       [(not (for/and ([rng2 (in-list rng)]) (equal? rng1 rng2)))
-        #f]
-       [else (make-arr (apply map Un (cons dom1 dom)) rng1 #f #f '())])]
-    [_ #f]))
+;; used when checking if (Arrow ... rst1 ...)
+;; is a subtype of (Arrow2 ... rst2 ...)
+(define (rest-arg-subtype* A rst1 rst2)
+  (match* (rst1 rst2)
+    [(_ #f) A]
+    [(t t) A]
+    [((? Type? t1) (? Type? t2)) (subtype* A t2 t1)]
+    [((RestDots: t1 dbound)
+      (RestDots: t2 dbound))
+     (subtype* A t2 t1)]
+    [(_ _) #f]))
+
+
+(define-syntax-rule (with-fresh-ids len ids . body)
+  (let-values ([(ids seq) (for/fold ([ids '()]
+                                     [seq (temp-ids)])
+                                    ([_ (in-range len)])
+                            (define-values (id rst) (id-seq-next seq))
+                            (values (cons id ids) rst))])
+    (parameterize ([temp-ids seq])
+      . body)))
 
 ;; simple co/contra-variance for ->
-(define/cond-contract (arr-subtype*/no-fail A arr1 arr2)
-  (-> list? arr? arr? any/c)
+(define (arrow-subtype* A arr1 arr2)
   (match* (arr1 arr2)
-    ;; the really simple case
-    [((arr: dom1 rng1 #f #f '())
-      (arr: dom2 rng2 #f #f '()))
-     (subtype-seq A
-                  (subtypes* dom2 dom1)
-                  (subval* (restrict-values rng1 dom2) rng2))]
-    [((arr: dom1 rng1 #f #f kws1)
-      (arr: dom2 rng2 #f #f kws2))
-     (subtype-seq A
-                  (subtypes* dom2 dom1)
-                  (kw-subtypes* kws1 kws2)
-                  (subval* (restrict-values rng1 dom2) rng2))]
-    [((arr: dom1 rng1 rest1 #f kws1)
-      (arr: dom2 rng2 #f    #f kws2))
-     (subtype-seq A
-                  (subtypes*/varargs dom2 dom1 rest1)
-                  (kw-subtypes* kws1 kws2)
-                  (subval* (restrict-values rng1 dom2) rng2))]
-    [((arr: dom1 rng1 #f    #f kws1)
-      (arr: dom2 rng2 rest2 #f kws2))
-     #f]
-    [((arr: dom1 rng1 rest1 #f kws1)
-      (arr: dom2 rng2 rest2 #f kws2))
-     (subtype-seq A
-                  (subtypes*/varargs dom2 dom1 rest1)
-                  (subtype* rest2 rest1)
-                  (kw-subtypes* kws1 kws2)
-                  (subval* (restrict-values rng1 dom2) rng2))]
-    ;; handle ... varargs when the bounds are the same
-    [((arr: dom1 rng1 #f (cons drest1 dbound) kws1)
-      (arr: dom2 rng2 #f (cons drest2 dbound) kws2))
-     (subtype-seq A
-                  (subtype* drest2 drest1)
-                  (subtypes* dom2 dom1)
-                  (kw-subtypes* kws1 kws2)
-                  (subval* (restrict-values rng1 dom2) rng2))]
-    [(_ _) #f]))
+    [((Arrow: dom1 rst1 kws1 rng1)
+      (Arrow: dom2 rst2 kws2 rng2))
+     (define A* (subtype-seq A
+                             (rest-arg-subtype* rst1 rst2)
+                             (subtypes*/varargs dom2 dom1 rst1)
+                             (kw-subtypes* kws1 kws2)))
+     (cond
+       [(not A*) #f]
+       [else
+        (define arity (max (length dom1) (length dom2)))
+        (with-fresh-ids arity ids
+          (define mapping
+            (for/list ([idx (in-range arity)]
+                       [id (in-list ids)]
+                       [t (in-list/rest dom2 (or rst2 Univ))])
+              (list* idx id t)))
+          (subval* A*
+                   (instantiate-obj+simplify rng1 mapping)
+                   (instantiate-obj rng2 ids)))])]))
 
 
 ;;************************************************************
@@ -269,10 +251,13 @@
       [(and (null? dom) (null? argtys)) A]
       [(null? argtys) #f]
       [(and (null? dom) rst)
-       (cond [(subtype* A (car argtys) rst) => (λ (A) (loop-varargs dom (cdr argtys) A))]
-             [else #f])]
+       (cond
+         [(subtype* A (car argtys) rst)
+          => (λ (A) (loop-varargs dom (cdr argtys) A))]
+         [else #f])]
       [(null? dom) #f]
-      [(subtype* A (car argtys) (car dom)) => (λ (A) (loop-varargs (cdr dom) (cdr argtys) A))]
+      [(subtype* A (car argtys) (car dom))
+       => (λ (A) (loop-varargs (cdr dom) (cdr argtys) A))]
       [else #f])))
 
 
@@ -374,8 +359,8 @@
                (subtype* t2 t1)))
 
 (define-syntax-rule (with-fresh-obj obj . body)
-  (let-values ([(obj os) (obj-seq-next (temp-objs))])
-    (parameterize ([temp-objs os])
+  (let-values ([(obj seq) (obj-seq-next (temp-objs))])
+    (parameterize ([temp-objs seq])
       . body)))
 
 ;; the algorithm for recursive types transcribed directly from TAPL, pg 305
@@ -407,7 +392,7 @@
           (and A
                (or (TrueProp? raw-prop)
                    (let* ([obj (if (Object? obj) obj (-id-path (genid)))]
-                          [prop (instantiate-rep/obj raw-prop obj t1)])
+                          [prop (instantiate-obj raw-prop obj)])
                      (implies-in-env? (lexical-env)
                                       (-is-type obj t1)
                                       prop)))
@@ -444,6 +429,26 @@
      (subtype* A t1 b2 obj)]
     [(_ _) #f]))
 
+
+
+
+;; is this a sequence of arrows of the form
+;; τ0 -> σ ∧ τ1 -> σ ∧ τn -> σ ...
+;; if so, return
+;; (∪ τ0 τ1 ... τn) -> σ
+;; else return #f
+(define/cond-contract (collapsable-arrows? arrows)
+  (-> (listof Arrow?) (or/c Arrow? #f))
+  (match arrows
+    [(cons (Arrow: (list dom1) #f '() rng) remaining)
+     (match remaining
+       [(list (Arrow: (list dom2) #f '() (== rng))
+              (Arrow: (list doms) #f '() (== rng)) ...)
+        (-Arrow (list (apply Un dom1 dom2 doms)) rng)]
+       [_ #f])]
+    [_ #f]))
+
+
 ;; these data structures are allocated once and
 ;; used below in 'subtype-switch'
 (define seq->elem-table
@@ -625,26 +630,20 @@
      ;; tvars are equal if they are the same variable
      [(F: var2) (eq? var1 var2)]
      [_ (continue<: A t1 t2 obj)])]
-  [(case: Function (Function: arrs1))
-   (match t2
-     ;; special-case for case-lambda/union with only one argument              
-     [(Function: (list arr2))
-      (cond [(null? arrs1) #f]
-            [else
-             (define comb (combine-arrs arrs1))
-             (or (and comb (arr-subtype*/no-fail A comb arr2))
-                 (supertype-of-one/arr A arr2 arrs1))])]
-     ;; case-lambda
-     [(Function: arrs2)
-      (if (null? arrs1) #f
-          (let loop-arities ([A A]
-                             [arrs2 arrs2])
-            (cond
-              [(null? arrs2) A]
-              [(supertype-of-one/arr A (car arrs2) arrs1)
-               => (λ (A) (loop-arities A (cdr arrs2)))]
-              [else #f])))]
-     [_ (continue<: A t1 t2 obj)])]
+  [(case: Fun (Fun: arrows1))
+   (match* (t2 arrows1)
+     [((Fun: (list arrow2)) (app collapsable-arrows? (? Arrow? arrow1)))
+      ;; special case when lhs can be collapsed into simpler arrow
+      (arrow-subtype* A arrow1 arrow2)]
+     [((Fun: arrows2) _)
+      (cond
+        [(null? arrows1) #f]
+        [else (for/fold ([A A])
+                        ([a2 (in-list arrows2)]
+                         #:break (not A))
+                (for/or ([a1 (in-list arrows1)])
+                  (arrow-subtype* A a1 a2)))])]
+     [(_ _) (continue<: A t1 t2 obj)])]
   [(case: Future (Future: elem1))
    (match t2
      [(Future: elem2) (subtype* A elem1 elem2)]
@@ -720,7 +719,7 @@
      [(Refine: t1* raw-prop)
       (cond
         [(Object? obj)
-         (define prop (instantiate-rep/obj raw-prop obj t1*))
+         (define prop (instantiate-obj raw-prop obj))
          (define env (env+ (lexical-env) (list prop)))
          (cond
            [(not env) A]
@@ -728,7 +727,7 @@
                    (subtype* A t1* t2 obj))])]
         [else
          (with-fresh-obj obj
-           (define prop (instantiate-rep/obj raw-prop obj t1*))
+           (define prop (instantiate-obj raw-prop obj))
            ;; since this is a fresh object, we will do a simpler environment extension
            (with-naively-extended-lexical-env [#:props (list prop)]
              (subtype* A t1* t2 obj)))])]
@@ -1008,7 +1007,7 @@
                     (and (subtype* A t1 t2*)
                          (implies-in-env? (lexical-env)
                                           (-is-type obj t1)
-                                          (instantiate-rep/obj p* obj t1)))))
+                                          (instantiate-obj p* obj)))))
       A]
      [_ (continue<: A t1 t2 obj)])]
   [(case: Vector (Vector: elem1))
diff --git a/typed-racket-lib/typed-racket/types/tc-result.rkt b/typed-racket-lib/typed-racket/types/tc-result.rkt
index 76b0239a..6b8bed5c 100644
--- a/typed-racket-lib/typed-racket/types/tc-result.rkt
+++ b/typed-racket-lib/typed-racket/types/tc-result.rkt
@@ -1,7 +1,8 @@
 #lang racket/base
 
 (require "../utils/utils.rkt"
-         (rep core-rep type-rep prop-rep values-rep)
+         (rep rep-utils core-rep type-rep prop-rep
+              values-rep free-variance)
          (utils tc-utils)
          (types base-abbrev)
          racket/match
@@ -9,13 +10,41 @@
 
 ;; this structure represents the result of typechecking an expression
 ;; fields are #f only when the direct result of parsing or annotations
-(define-struct/cond-contract tc-result
-  ([t Type?] [pset (c:or/c PropSet? #f)] [o (c:or/c OptObject? #f)])
-  #:transparent)
-(define-struct/cond-contract tc-results
-  ([ts (c:listof tc-result?)] [drest (c:or/c (c:cons/c Type? symbol?) #f)])
-  #:transparent)
-(define-struct/cond-contract tc-any-results ([f (c:or/c Prop? #f)]) #:transparent)
+(def-rep tc-result ([t Type?]
+                    [pset (c:or/c PropSet? #f)]
+                    [o (c:or/c OptObject? #f)])
+  #:no-provide
+  [#:frees (f)
+   (combine-frees (list (f t)
+                        (if pset (f pset) empty-free-vars)
+                        (if o (f o) empty-free-vars)))]
+  [#:fmap (f)
+   (make-tc-result (f t)
+                   (and pset (f pset))
+                   (and o (f o)))]
+  [#:for-each (f)
+   (f t)
+   (when pset (f pset))
+   (when o (f o))])
+
+(def-rep tc-results ([tcrs (c:listof tc-result?)]
+                     [drst (c:or/c #f RestDots?)])
+  #:no-provide
+  [#:frees (f)
+   (combine-frees (cons (if drst (f drst) empty-free-vars)
+                        (map f tcrs)))]
+  [#:fmap (f)
+   (make-tc-results (map f tcrs)
+                    (and drst (f drst)))]
+  [#:for-each (f)
+   (for-each f tcrs)
+   (when drst (f drst))])
+
+(def-rep tc-any-results ([p (c:or/c Prop? #f)])
+  #:no-provide
+  [#:frees (f) (if p (f p) empty-free-vars)]
+  [#:fmap (f) (make-tc-any-results (and p (f p)))]
+  [#:for-each (f) (when p (f p))])
 
 (define (tc-results/c v)
   (or (tc-results? v)
@@ -23,81 +52,48 @@
 
 (define (tc-results1/c v)
   (and (tc-results? v)
-       (= (length (tc-results-ts v)) 1)))
+       (= (length (tc-results-tcrs v)) 1)))
 
 ;; Contract to check that values are tc-results/c and do not contain #f propset or obj
 ;; Used to contract the return values of typechecking functions.
 (define (full-tc-results/c r)
   (match r
     [(tc-any-results: p) (and p #t)]
-    [(tc-results: _ ps os)
-     (and (andmap (λ (x) x) ps)
+    [(tc-results: (list (tc-result: _ pss os) ...) _)
+     (and (andmap (λ (x) x) pss)
           (andmap (λ (x) x) os)
           #t)]
-    [(tc-results: _ ps os _ _)
-     (and (andmap (λ (x) x) ps)
-          (andmap (λ (x) x) os)
-          #t)]
-    [else #f]))
+    [_ #f]))
 
 
-(define-match-expander tc-result:
+(define-match-expander tc-result:*
   (syntax-rules ()
    [(_ tp fp op) (tc-result tp fp op)]
    [(_ tp) (tc-result tp _ _)]))
 
-;; expand-tc-results: (Listof tc-result) -> (Values (Listof Type) (Listof PropSet) (Listof Object))
-(define (expand-tc-results results)
-  (values (map tc-result-t results) (map tc-result-pset results) (map tc-result-o results)))
-
-(define-match-expander tc-results:
-  (syntax-rules ()
-   [(_ tp)
-    (tc-results (app expand-tc-results tp _ _) #f)]
-   [(_ tp fp op)
-    (tc-results (app expand-tc-results tp fp op) #f)]
-   [(_ tp fp op dty dbound)
-    (tc-results (app expand-tc-results tp fp op) (cons dty dbound))]))
-
-(define-match-expander tc-any-results:
-  (syntax-rules ()
-   [(_ f)
-    (tc-any-results f)]))
-
 
 (define-match-expander tc-result1:
   (syntax-rules ()
-   [(_ tp) (tc-results: (list tp))]
-   [(_ tp fp op) (tc-results: (list tp) (list fp) (list op))]))
+   [(_ t) (tc-results: (list (tc-result: t _ _)) #f)]
+   [(_ t ps o) (tc-results: (list (tc-result: t ps o)) #f)]))
 
 (define (tc-results-ts* tc)
   (match tc
-    [(tc-results: t) t]))
+    [(tc-results: (list (tc-result: ts _ _) ...) _) ts]))
 
 (define-match-expander Result1:
   (syntax-rules ()
    [(_ tp) (Results: (list tp))]
    [(_ tp fp op) (Results: (list tp) (list fp) (list op))]))
 
-;; expand-Results: (Listof Rresult) -> (Values (Listof Type) (Listof PropSet) (Listof Object))
-(define (expand-Results results)
-  (values (map Result-t results) (map Result-ps results) (map Result-o results)))
-
-
-(define-match-expander Results:
-  (syntax-rules ()
-   [(_ tp) (Values: (app expand-Results tp _ _))]
-   [(_ tp fp op) (Values: (app expand-Results tp fp op))]
-   [(_ tp fp op dty dbound) (ValuesDots: (app expand-Results tp fp op) dty dbound)]))
-
 ;; make-tc-result*: Type? PropSet/c Object? -> tc-result?
 ;; Smart constructor for a tc-result.
 (define (-tc-result type [prop -tt-propset] [object -empty-obj])
   (cond
     [(or (equal? type -Bottom) (equal? prop -ff-propset))
-     (tc-result -Bottom -ff-propset object)]
+     (make-tc-result -Bottom -ff-propset object)]
     [else
-     (tc-result type prop object)]))
+     (make-tc-result type prop object)]))
 
 
 ;; convenience function for returning the result of typechecking an expression
@@ -130,7 +126,7 @@
                  (if (and (list? t) (list? pset) (list? o))
                      (map -tc-result t pset o)
                      (list (-tc-result t pset o)))
-                 (cons dty dbound))]))
+                 (make-RestDots dty dbound))]))
 
 
 ;; fix-props:
@@ -150,19 +146,28 @@
 ;; Turns #f Prop or Obj into the Empty/Trivial
 (define (fix-results r)
   (match r
-    [(tc-any-results: f) (tc-any-results (fix-props f -tt))]
-    [(tc-results: ts ps os)
-     (ret ts (map fix-props ps) (map fix-object os))]
-    [(tc-results: ts ps os dty dbound)
-     (ret ts (map fix-props ps) (map fix-object os) dty dbound)]))
+    [(tc-any-results: p) (make-tc-any-results (fix-props p -tt))]
+    [(tc-results: ts drst)
+     (make-tc-results
+      (map (match-lambda
+             [(tc-result: t ps o)
+              (make-tc-result t (fix-props ps) (fix-object o))])
+           ts)
+      drst)]))
 
 (define (fix-results/bottom r)
   (match r
-    [(tc-any-results: f) (tc-any-results (fix-props f -ff))]
-    [(tc-results: ts ps os)
-     (ret ts (for/list ([p ps]) (fix-props p -ff-propset)) (map fix-object os))]
-    [(tc-results: ts ps os dty dbound)
-     (ret ts (for/list ([p ps]) (fix-props p -ff-propset)) (map fix-object os) dty dbound)]))
+    [(tc-any-results: p) (make-tc-any-results (fix-props p -ff))]
+    [(tc-results: (list (tc-result: ts ps os) ...) #f)
+     (ret ts
+          (for/list ([p (in-list ps)]) (fix-props p -ff-propset))
+          (map fix-object os))]
+    [(tc-results: (list (tc-result: ts ps os) ...) (RestDots: dty dbound))
+     (ret ts
+          (for/list ([p (in-list ps)]) (fix-props p -ff-propset))
+          (map fix-object os)
+          dty
+          dbound)]))
 
 (provide/cond-contract
  [ret
@@ -179,15 +184,20 @@
 
 (define tc-result-equal? equal?)
 
-(provide tc-result: tc-results: tc-any-results: tc-result1: Result1: Results:
-         tc-results)
+(provide tc-any-results: tc-result1: Result1: tc-results:
+         (rename-out [tc-result:* tc-result:]))
 (provide/cond-contract
- [rename -tc-result tc-result
-   (c:case->
-     (Type? . c:-> . tc-result?)
-     (Type? PropSet? OptObject? . c:-> . tc-result?))]
- [tc-any-results ((c:or/c Prop? #f) . c:-> . tc-any-results?)]
+ [-tc-result
+  (c:case->
+   (Type? . c:-> . tc-result?)
+   (Type? PropSet? OptObject? . c:-> . tc-result?))]
  [tc-result-t (tc-result? . c:-> . Type?)]
+ [rename make-tc-results -tc-results
+         (c:-> (c:listof tc-result?)
+               (c:or/c #f RestDots?)
+               tc-results?)]
+ [rename make-tc-any-results -tc-any-results
+         (c:-> (c:or/c #f Prop?) tc-any-results?)]
  [rename tc-results-ts* tc-results-ts (tc-results? . c:-> . (c:listof Type?))]
  [tc-result-equal? (tc-result? tc-result? . c:-> . boolean?)]
  [tc-result? (c:any/c . c:-> . boolean?)]
diff --git a/typed-racket-lib/typed-racket/types/type-table.rkt b/typed-racket-lib/typed-racket/types/type-table.rkt
index a117cf92..4e9c87a6 100644
--- a/typed-racket-lib/typed-racket/types/type-table.rkt
+++ b/typed-racket-lib/typed-racket/types/type-table.rkt
@@ -105,8 +105,8 @@
               ;; of the + function)
               (printer-thunk type-names
                 (pretty-format-rep (cleanup-type type))))]
-        [(or (tc-results: types)
-             (tc-results: types _ _ _ _)) ; FIXME, account for dty/dbound
+        [(tc-results: (list (tc-result: types _ _)...) _)
+         ;; FIXME, account for dty/dbound
          (printer-thunk type-names
            (apply string-append
                   (for/list ([(type index) (in-indexed (in-list types))])
diff --git a/typed-racket-lib/typed-racket/types/update.rkt b/typed-racket-lib/typed-racket/types/update.rkt
index a7acefaf..1b3567a1 100644
--- a/typed-racket-lib/typed-racket/types/update.rkt
+++ b/typed-racket-lib/typed-racket/types/update.rkt
@@ -66,10 +66,9 @@
          ;; is an object type that doesn't mention private fields. Thus we use the
          ;; FieldPE path element as a marker to refine the result of the accessor
          ;; function.
-         [((Function: (list (arr: doms (Values: (list (Result: rng _ _))) _ _ _)))
+         [((Fun: (list (Arrow: doms _ _ (Values: (list (Result: rng _ _))))))
            (FieldPE:))
-          (make-Function
-           (list (make-arr* doms (update rng rst))))]
+          (make-Fun (list (-Arrow doms (update rng rst))))]
          
          [((Union: _ ts) _)
           ;; Note: if there is a path element, then all Base types are
diff --git a/typed-racket-lib/typed-racket/types/utils.rkt b/typed-racket-lib/typed-racket/types/utils.rkt
index dc789d11..702c8b1f 100644
--- a/typed-racket-lib/typed-racket/types/utils.rkt
+++ b/typed-racket-lib/typed-racket/types/utils.rkt
@@ -74,33 +74,32 @@
 ;; has-optional-args? : (Listof arr) -> Boolean
 ;; Check if the given arrs meet the necessary conditions to be printed
 ;; with a ->* constructor or for generating a ->* contract
-(define (has-optional-args? arrs)
- (and (> (length arrs) 1)
-      ;; No polydots
-      (for/and ([arr (in-list arrs)])
-        (match arr [(arr: _ _ _ drest _) (not drest)]))
-      ;; Keyword args, range and rest specs all the same.
-      (let* ([xs (map (match-lambda [(arr: _ rng rest-spec _ kws)
-                                (list rng rest-spec kws)])
-                      arrs)]
-             [first-x (first xs)])
-        (for/and ([x (in-list (rest xs))])
-          (equal? x first-x)))
-      ;; Positionals are monotonically increasing by at most one.
-      (let-values ([(_ ok?)
-                    (for/fold ([positionals (arr-dom (first arrs))]
-                               [ok-so-far?  #t])
-                              ([arr (in-list (rest arrs))])
-                      (match arr
-                        [(arr: dom _ _ _ _)
-                         (define ldom         (length dom))
-                         (define lpositionals (length positionals))
-                         (values dom
-                                 (and ok-so-far?
-                                      (or (= ldom lpositionals)
-                                          (= ldom (add1 lpositionals)))
-                                      (equal? positionals (take dom lpositionals))))]))])
-        ok?)))
+(define (has-optional-args? arrows)
+  (and (> (length arrows) 1)
+       ;; No polydots
+       (not (ormap (λ (a) (RestDots? (Arrow-rst a))) arrows))
+       ;; Keyword args, range and rest specs all the same.
+       (match-let ([(cons (Arrow: _ rst1 kws1 rng1) as) arrows])
+         (for/and ([a (in-list as)])
+           (match a
+             [(Arrow: _ rst2 kws2 rng2)
+              (and (equal? rst1 rst2)
+                   (equal? kws1 kws2)
+                   (equal? rng1 rng2))])))
+       ;; Positionals are monotonically increasing by at most one.
+       (let-values ([(_ ok?)
+                     (for/fold ([positionals (Arrow-dom (first arrows))]
+                                [ok?  #t])
+                               ([arr (in-list (rest arrows))]
+                                #:break (not ok?))
+                       (define dom (Arrow-dom arr))
+                       (define ldom (length dom))
+                       (define lpositionals (length positionals))
+                       (values dom
+                               (and (or (= ldom lpositionals)
+                                        (= ldom (add1 lpositionals)))
+                                    (equal? positionals (take dom lpositionals)))))])
+         ok?)))
 
 (provide/cond-contract
  [instantiate-poly ((or/c Poly? PolyDots? PolyRow?) (listof Rep?)
@@ -111,6 +110,6 @@
  [fi (Rep? . -> . (listof symbol?))]
  [fv/list ((listof Rep?) . -> . (set/c symbol?))]
  [current-poly-struct (parameter/c (or/c #f poly?))]
- [has-optional-args? (-> (listof arr?) any)]
+ [has-optional-args? (-> (listof Arrow?) any)]
  )
 
diff --git a/typed-racket-lib/typed-racket/utils/utils.rkt b/typed-racket-lib/typed-racket/utils/utils.rkt
index 801f9f6a..79da7668 100644
--- a/typed-racket-lib/typed-racket/utils/utils.rkt
+++ b/typed-racket-lib/typed-racket/utils/utils.rkt
@@ -35,7 +35,11 @@ at least theoretically.
  gen-pretty-id
  local-tr-identifier?
  mark-id-as-normalized
- normalized-id?)
+ normalized-id?
+ assoc-ref
+ assoc-set
+ assoc-remove
+ in-assoc)
 
 (define optimize? (make-parameter #t))
 (define with-linear-integer-arithmetic? (make-parameter #f))
@@ -354,18 +358,18 @@ at least theoretically.
        #'[(val)
           (:do-in
            ;; ([(outer-id ...) outer-expr] ...)
-           ([(list) list-exp]
-            [(rest) rest-exp])
+           ([(l) list-exp]
+            [(r) rest-exp])
            ;; outer-check
            #t
            ;; ([loop-id loop-expr] ...)
-           ([pos list])
+           ([pos l])
            ;; pos-guard
            #t
            ;; ([(inner-id ...) inner-expr] ...)
            ([(val pos) (if (pair? pos)
                            (values (car pos) (cdr pos))
-                           (values rest '()))])
+                           (values r '()))])
            ;; pre-guard
            #t
            ;; post-guard
@@ -405,4 +409,66 @@ at least theoretically.
      (if (eqv? 0 idx)
          (car xs)
          (list-ref/default (cdr xs) (sub1 idx) default))]
-    [else default]))
\ No newline at end of file
+    [else default]))
+
+(define assoc-ref
+  (let ([no-arg (gensym)])
+    (λ (d key [default no-arg])
+      (cond
+        [(assoc key d) => cdr]
+        [(eq? default no-arg)
+         (raise-mismatch-error 'assoc-ref
+                               (format "no value for key: ~e in: " key)
+                               d)]
+        [(procedure? default) (default)]
+        [else default]))))
+
+(define (assoc-set d key val)
+  (let loop ([xd d])
+    (cond
+      [(null? xd) (list (cons key val))]
+      [else
+       (let ([a (car xd)])
+         (if (equal? (car a) key)
+             (cons (cons key val) (cdr xd))
+             (cons a (loop (cdr xd)))))])))
+
+(define (assoc-remove d key)
+  (let loop ([xd d])
+    (cond
+      [(null? xd) null]
+      [else
+       (let ([a (car xd)])
+         (if (equal? (car a) key)
+             (cdr xd)
+             (cons a (loop (cdr xd)))))])))
+
+(define (in-assoc-proc l)
+  (in-parallel (map car l) (map cdr l)))
+
+(define-sequence-syntax in-assoc
+  (λ () #'in-list/rest-proc)
+  (λ (stx)
+    (syntax-case stx ()
+      [[(key val) (_ assoc-exp)]
+       #'[(val)
+          (:do-in
+           ;; ([(outer-id ...) outer-expr] ...)
+           ([(l) assoc-exp])
+           ;; outer-check
+           #t
+           ;; ([loop-id loop-expr] ...)
+           ([pos l])
+           ;; pos-guard
+           #t
+           ;; ([(inner-id ...) inner-expr] ...)
+           ([(key val pos) (if (pair? pos)
+                               (values (caar pos) (cdar pos) (cdr pos))
+                               (values #f #f #f))])
+           ;; pre-guard
+           pos
+           ;; post-guard
+           #t
+           ;; (loop-arg ...)
+           (pos))]]
+      [blah (raise-syntax-error 'in-assoc "invalid usage" #'blah)])))
\ No newline at end of file
diff --git a/typed-racket-more/typed/rackunit/type-env-ext.rkt b/typed-racket-more/typed/rackunit/type-env-ext.rkt
index 5434639c..32b6409b 100644
--- a/typed-racket-more/typed/rackunit/type-env-ext.rkt
+++ b/typed-racket-more/typed/rackunit/type-env-ext.rkt
@@ -6,8 +6,8 @@
           racket/base syntax/parse
           (utils tc-utils)
           (env init-envs)
-          (except-in (rep prop-rep object-rep type-rep) make-arr)
-          (rename-in (types abbrev) [make-arr* make-arr])))
+          (rep prop-rep object-rep type-rep)
+          (types abbrev)))
 
 (define-for-syntax unit-env
   (make-env
diff --git a/typed-racket-test/fail/pr13448.rkt b/typed-racket-test/fail/pr13448.rkt
deleted file mode 100644
index d3ebfd02..00000000
--- a/typed-racket-test/fail/pr13448.rkt
+++ /dev/null
@@ -1,7 +0,0 @@
-#lang typed/racket
-(: foo
-   (case-> 
-     (Number -> Number)
-     (Number String -> Number)
-     (Number String String * -> Number)))
-(define (foo x (s1 "") . s) x)
diff --git a/typed-racket-test/unit-tests/check-below-tests.rkt b/typed-racket-test/unit-tests/check-below-tests.rkt
index c0b249bd..5ecba033 100644
--- a/typed-racket-test/unit-tests/check-below-tests.rkt
+++ b/typed-racket-test/unit-tests/check-below-tests.rkt
@@ -27,14 +27,11 @@
 
 (define (check-result result)
   (match result
-    [(tc-results: ts fs os)
-     (for-each check-prop fs)
-     (for-each check-object os) ]
-    [(tc-results: ts fs os dty bound)
-     (for-each check-prop fs)
+    [(tc-results: (list (tc-result: _ ps os) ...) _)
+     (for-each check-prop ps)
      (for-each check-object os)]
-    [(tc-any-results: f)
-     (check-prop f)]
+    [(tc-any-results: p)
+     (check-prop p)]
     [(? Type?)
      (void)]))
 
@@ -121,23 +118,23 @@
       (ret (list -Symbol) (list -tt-propset) (list -empty-obj))
       (ret (list Univ) (list -true-propset) (list (make-Path empty #'x))))
 
-    (test-below (ret -Bottom) (tc-any-results #f) #:result (tc-any-results -ff))
-    (test-below (ret Univ) (tc-any-results -tt) #:result (tc-any-results -tt))
-    (test-below (tc-any-results -ff) (tc-any-results #f) #:result (tc-any-results -ff))
+    (test-below (ret -Bottom) (-tc-any-results #f) #:result (-tc-any-results -ff))
+    (test-below (ret Univ) (-tc-any-results -tt) #:result (-tc-any-results -tt))
+    (test-below (-tc-any-results -ff) (-tc-any-results #f) #:result (-tc-any-results -ff))
     (test-below
       (ret (list -Symbol -String) (list -true-propset -ff-propset))
-      (tc-any-results #f)
-      #:result (tc-any-results -ff))
-    (test-below (ret -Symbol -ff-propset) (tc-any-results #f) #:result (tc-any-results -ff))
+      (-tc-any-results #f)
+      #:result (-tc-any-results -ff))
+    (test-below (ret -Symbol -ff-propset) (-tc-any-results #f) #:result (-tc-any-results -ff))
 
-    (test-below (ret -Symbol -true-propset -empty-obj) (tc-any-results #f)
-      #:result (tc-any-results -tt))
-    (test-below (ret (list -Symbol -String)) (tc-any-results #f)
-      #:result (tc-any-results -tt))
+    (test-below (ret -Symbol -true-propset -empty-obj) (-tc-any-results #f)
+      #:result (-tc-any-results -tt))
+    (test-below (ret (list -Symbol -String)) (-tc-any-results #f)
+      #:result (-tc-any-results -tt))
     (test-below
       (ret (list -Symbol -String) (list -true-propset -false-propset) (list -empty-obj -empty-obj))
-      (tc-any-results #f)
-      #:result (tc-any-results -tt))
+      (-tc-any-results #f)
+      #:result (-tc-any-results -tt))
 
 
     (test-below #:fail
@@ -146,7 +143,7 @@
       #:result (ret (list -Symbol -Symbol) (list -tt-propset -tt-propset) (list -empty-obj -empty-obj)))
 
     (test-below #:fail
-      (tc-any-results -tt)
+      (-tc-any-results -tt)
       (ret -Symbol))
 
 
@@ -164,7 +161,7 @@
       #:result (ret -Symbol -tt-propset -empty-obj Univ 'B))
 
     (test-below #:fail
-      (tc-any-results -tt)
+      (-tc-any-results -tt)
       (ret -Symbol #f -empty-obj Univ 'B)
       #:result (ret (list -Symbol) (list -tt-propset) (list -empty-obj) Univ 'B))
 
@@ -173,8 +170,8 @@
       (ret (list -Symbol -Symbol) (list -tt-propset -tt-propset)  (list -empty-obj -empty-obj) Univ 'B))
 
     (test-below (ret -Symbol -true-propset -empty-obj Univ 'B)
-                (tc-any-results #f)
-                #:result (tc-any-results -tt))
+                (-tc-any-results #f)
+                #:result (-tc-any-results -tt))
 
     (test-below
       (ret -Symbol)
diff --git a/typed-racket-test/unit-tests/contract-tests.rkt b/typed-racket-test/unit-tests/contract-tests.rkt
index 5328f0fe..72078105 100644
--- a/typed-racket-test/unit-tests/contract-tests.rkt
+++ b/typed-racket-test/unit-tests/contract-tests.rkt
@@ -136,9 +136,9 @@
    (t (-set Univ)) 
    (t (make-pred-ty -Symbol))
    (t (->key -Symbol #:key -Boolean #t Univ))
-   (t (make-Function
-       (list (make-arr* (list Univ) -Boolean #:kws (list (make-Keyword '#:key Univ #t))
-                        #:props (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol))))))
+   (t (make-Fun
+       (list (-Arrow (list Univ) -Boolean #:kws (list (make-Keyword '#:key Univ #t))
+                     #:props (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol))))))
    (t (-struct #'struct-name1 #f (list (make-fld -Symbol #'acc #f))))
    ;; Adapted from PR 13815
    (t (-poly (a) (-> a a)))
@@ -184,20 +184,20 @@
 
    ;; Github Issue #50
    (t (cl->* (-> -String -Bottom) (-> -String -Symbol -Bottom)))
-   (t (make-Function
-       (list (make-arr* (list -String) -Boolean
-                        #:kws (list (make-Keyword '#:key Univ #t))
-                        #:props (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol)))
-             (make-arr* (list -String Univ) -Boolean
-                        #:kws (list (make-Keyword '#:key Univ #t))
-                        #:props (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol))))))
+   (t (make-Fun
+       (list (-Arrow (list -String) -Boolean
+                     #:kws (list (make-Keyword '#:key Univ #t))
+                     #:props (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol)))
+             (-Arrow (list -String Univ) -Boolean
+                     #:kws (list (make-Keyword '#:key Univ #t))
+                     #:props (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol))))))
    (t/fail (cl->* (-> -String ManyUniv) (-> -String Univ ManyUniv))
            "unknown return values")
 
    (t/fail
-    (make-Function
-     (list (make-arr* (list) -Boolean #:kws (list (make-Keyword '#:key Univ #f)))
-           (make-arr* (list Univ) -Boolean #:kws (list (make-Keyword '#:key2 Univ #f)))))
+    (make-Fun
+     (list (-Arrow (list) -Boolean #:kws (list (make-Keyword '#:key Univ #f)))
+           (-Arrow (list Univ) -Boolean #:kws (list (make-Keyword '#:key2 Univ #f)))))
     "case function type with optional keyword arguments")
    (t/fail (-> (make-pred-ty -Symbol)-Symbol)
            "function type with props or objects")
@@ -215,10 +215,10 @@
            "required a chaperone contract but generated an impersonator contract")
 
    (t/fail
-    (make-Function
+    (make-Fun
      (list
-      (make-arr* (list) -Boolean #:kws (list (make-Keyword '#:key Univ #t)))
-      (make-arr* (list Univ Univ) -Boolean #:kws (list (make-Keyword '#:key2 Univ #t)))))
+      (-Arrow (list) -Boolean #:kws (list (make-Keyword '#:key Univ #t)))
+      (-Arrow (list Univ Univ) -Boolean #:kws (list (make-Keyword '#:key2 Univ #t)))))
     "case function type with optional keyword arguments")
    (t/fail (-vec (-struct #'struct-name3 #f (list (make-fld (-seq -Symbol) #'acc #f)) #f #t))
            "required a chaperone contract but generated an impersonator contract")
diff --git a/typed-racket-test/unit-tests/keyword-expansion-test.rkt b/typed-racket-test/unit-tests/keyword-expansion-test.rkt
index b5a8ce68..7a073437 100644
--- a/typed-racket-test/unit-tests/keyword-expansion-test.rkt
+++ b/typed-racket-test/unit-tests/keyword-expansion-test.rkt
@@ -16,7 +16,7 @@
 
 (define (extract-arrs t)
   (match t
-    [(Function: arrs) (apply set arrs)]
+    [(Fun: arrs) (apply set arrs)]
     [t t]))
 
 (define-syntax-rule (t-opt ((req-arg ...) (opt-arg ...)) expected)
diff --git a/typed-racket-test/unit-tests/metafunction-tests.rkt b/typed-racket-test/unit-tests/metafunction-tests.rkt
index b7c0d89e..4dde69da 100644
--- a/typed-racket-test/unit-tests/metafunction-tests.rkt
+++ b/typed-racket-test/unit-tests/metafunction-tests.rkt
@@ -163,7 +163,7 @@
       (check-equal?
         (values->tc-results (make-AnyValues (-is-type '(0 . 0) -String))
                             (list (make-Path null #'x)) (list Univ))
-        (tc-any-results (-is-type #'x -String)))
+        (-tc-any-results (-is-type #'x -String)))
 
 
       (check-equal?
@@ -193,29 +193,30 @@
                   (make-TypeProp (make-Path (list -car) #'x) -NonPosInt))))
     )
 
-    (test-suite "replace-names"
+    (test-suite "term substitution"
       (check-equal?
-        (replace-names (list #'x) (list (make-Path null '(0 . 0)))
-                       (ret Univ -tt-propset (make-Path null #'x)))
+        (abstract-obj (ret Univ -tt-propset (make-Path null #'x))
+                      (list #'x))
         (ret Univ -tt-propset (make-Path null '(0 . 0))))
       (check-equal?
-        (replace-names (list #'x) (list (make-Path null '(0 . 0)))
-                       (ret (-> Univ Univ : -tt-propset : (make-Path null #'x))))
+        (abstract-obj (ret (-> Univ Univ : -tt-propset : (make-Path null #'x)))
+                      (list #'x))
         (ret (-> Univ Univ : -tt-propset : (make-Path null '(1 . 0)))))
       (check-equal?
-        (replace-names (list #'x) (list (make-Path null '(0 . 0)))
-                       (ret (-refine/fresh y -Int (-leq (-lexp y) (-lexp #'x)))
-                            -tt-propset
-                            (make-Path null #'x)))
+       (abstract-obj (ret (-refine/fresh y -Int (-leq (-lexp y) (-lexp #'x)))
+                          -tt-propset
+                          (make-Path null #'x))
+                     (list #'x))
         (ret (-refine/fresh y -Int (-leq (-lexp y) (-lexp (make-Path null '(1 . 0)))))
              -tt-propset
              (make-Path null '(0 . 0))))
 
       (check-equal?
-       (replace-names (list #'x) (list -empty-obj)
-                      (ret (-refine/fresh y -Int (-leq (-lexp y) (-lexp #'x)))
-                           -tt-propset
-                           (make-Path null #'x)))
+       (erase-identifiers
+        (ret (-refine/fresh y -Int (-leq (-lexp y) (-lexp #'x)))
+             -tt-propset
+             (make-Path null #'x))
+        (list #'x))
        (ret -Int
             -tt-propset
             -empty-obj))
diff --git a/typed-racket-test/unit-tests/subst-tests.rkt b/typed-racket-test/unit-tests/subst-tests.rkt
index b1dc1e90..9a79f20c 100644
--- a/typed-racket-test/unit-tests/subst-tests.rkt
+++ b/typed-racket-test/unit-tests/subst-tests.rkt
@@ -30,8 +30,8 @@
     (s -Number a (-pair -String (-v a)) (-pair -String -Number))
     (s* (-Symbol -String) #f a (make-ListDots (-v a) 'a) (-lst* -Symbol -String))
     (s* (-Symbol -String) Univ a (make-ListDots (-v a) 'a) (-lst* -Symbol -String #:tail (-lst Univ)))
-    (s... (-Number -Boolean) a (make-Function (list (make-arr-dots null -Number (-v a) 'a))) (-Number -Boolean . -> . -Number))
-    (s... (-Number -Boolean) a (make-Function (list (make-arr-dots (list -String) -Number (-v a) 'a))) (-String -Number -Boolean . -> . -Number))
-    (s... (-Number -Boolean) a (make-Function (list (make-arr-dots (list -String) -Number (-v b) 'a))) (-String (-v b) (-v b) . -> . -Number))
-    (s... (-Number -Boolean) a (make-Function (list (make-arr-dots (list -String) -Number (-v b) 'b)))
-          (make-Function (list (make-arr-dots (list -String) -Number (-v b) 'b))))))
+    (s... (-Number -Boolean) a (make-Fun (list (make-arr-dots null -Number (-v a) 'a))) (-Number -Boolean . -> . -Number))
+    (s... (-Number -Boolean) a (make-Fun (list (make-arr-dots (list -String) -Number (-v a) 'a))) (-String -Number -Boolean . -> . -Number))
+    (s... (-Number -Boolean) a (make-Fun (list (make-arr-dots (list -String) -Number (-v b) 'a))) (-String (-v b) (-v b) . -> . -Number))
+    (s... (-Number -Boolean) a (make-Fun (list (make-arr-dots (list -String) -Number (-v b) 'b)))
+          (make-Fun (list (make-arr-dots (list -String) -Number (-v b) 'b))))))
diff --git a/typed-racket-test/unit-tests/typecheck-tests.rkt b/typed-racket-test/unit-tests/typecheck-tests.rkt
index ac063f2d..50c92fa7 100644
--- a/typed-racket-test/unit-tests/typecheck-tests.rkt
+++ b/typed-racket-test/unit-tests/typecheck-tests.rkt
@@ -552,7 +552,7 @@
         [tc-e/t #(2 3 #t) (make-HeterogeneousVector (list -Integer -Integer -Boolean))]
         [tc-e (vector 2 "3" #t) (make-HeterogeneousVector (list -Integer -String -Boolean))]
         [tc-e (vector) (make-HeterogeneousVector (list))]
-        [tc-e (vector) #:ret (tc-any-results -tt) #:expected (tc-any-results #f)]
+        [tc-e (vector) #:ret (-tc-any-results -tt) #:expected (-tc-any-results #f)]
         [tc-err (vector)
                 #:ret (tc-ret -Integer)
            #:expected (tc-ret -Integer)]
@@ -1163,11 +1163,11 @@
               (-lst* -One -String -Char)]
         ;; instantiating non-dotted terms
         [tc-e/t (inst (plambda: (a) ([x : a]) x) Integer)
-                (make-Function
-                 (list (make-arr* (list -Integer) -Integer
-                                  #:props (-PS (-not-type (cons 0 0) (-val #f))
-                                               (-is-type (cons 0 0) (-val #f)))
-                                  #:object (make-Path null (cons 0 0)))))]
+                (make-Fun
+                 (list (-Arrow (list -Integer) -Integer
+                               #:props (-PS (-not-type (cons 0 0) (-val #f))
+                                            (-is-type (cons 0 0) (-val #f)))
+                               #:object (make-Path null (cons 0 0)))))]
         [tc-e/t (inst (plambda: (a) [x : a *] (apply list x)) Integer)
                 ((list) -Integer . ->* . (-lst -Integer) : -true-propset)]