diff --git a/typed-racket-lib/typed-racket/infer/dmap.rkt b/typed-racket-lib/typed-racket/infer/dmap.rkt
index 21f9bdc5..81abecef 100644
--- a/typed-racket-lib/typed-racket/infer/dmap.rkt
+++ b/typed-racket-lib/typed-racket/infer/dmap.rkt
@@ -39,7 +39,7 @@
      #f
      (%1 make-dcon
       (for/list/fail ([c1 (in-list fixed1)]
-                      [c2 (in-sequence-forever fixed2 rest)])
+                      [c2 (in-list/rest fixed2 rest)])
         (c-meet c1 c2))
       #f)]
     ;; redo in the other order to call the previous case
@@ -52,7 +52,7 @@
                        (values fixed2 fixed1 rest2 rest1))])
        (% make-dcon
         (for/list/fail ([c1 (in-list longer)]
-                   [c2 (in-sequence-forever shorter srest)])
+                   [c2 (in-list/rest shorter srest)])
           (c-meet c1 c2))
         (c-meet lrest srest)))]
     [((struct dcon-dotted (fixed1 c1 bound1)) (struct dcon-dotted (fixed2 c2 bound2)))
diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index f8cd3940..82bcaef8 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -404,13 +404,16 @@
 ;; produces a cset which determines a substitution that makes S a subtype of T
 ;; implements the V |-_X S <: T => C judgment from Pierce+Turner, extended with
 ;; the index variables from the TOPLAS paper
-(define/cond-contract (cgen context S T)
-  (context? (or/c Values/c ValuesDots? AnyValues?) (or/c Values/c ValuesDots? AnyValues?)
-   . -> . (or/c #F cset?))
+(define/cond-contract (cgen context S T [obj #f])
+  (->* (context? (or/c Values/c ValuesDots? AnyValues?)
+                 (or/c Values/c ValuesDots? AnyValues?))
+       ((or/c #f OptObject?))
+       (or/c #F cset?))
   ;; useful quick loop
-  (define/cond-contract (cg S T)
-   (Type? Type? . -> . (or/c #f cset?))
-   (cgen context S T))
+  (define/cond-contract (cg S T [obj #f])
+   (->* (Type? Type?) ((or/c #f OptObject?))
+        (or/c #f cset?))
+   (cgen context S T obj))
   (define/cond-contract (cg/inv S T)
    (Type? Type? . -> . (or/c #f cset?))
    (cgen/inv context S T))
@@ -454,7 +457,8 @@
         ;; check each element
         [((Result: s pset-s o-s)
           (Result: t pset-t o-t))
-         (% cset-meet (cg s t)
+         (% cset-meet
+            (cg s t o-s)
             (cgen/prop-set context pset-s pset-t)
             (cgen/object context o-s o-t))]
 
@@ -465,8 +469,8 @@
          ;; Check for a substition that S is below (ret -Bottom).
          (define bottom-case
            (match S
-             [(Values: (list (Result: s f-s o-s)))
-              (cgen context s -Bottom)]
+             [(Values: (list (Result: s _ o-s)))
+              (cgen context s -Bottom o-s)]
              [else #f]))
          (define regular-case
            (cgen/seq context s-seq t-seq))
@@ -477,7 +481,7 @@
 
         ;; they're subtypes. easy.
         [(a b) #:when (cond
-                        [(Type? a) (subtype a b)]
+                        [(Type? a) (subtype a b obj)]
                         [(Result? a) (subresult a b)]
                         [else (subval a b)])
          empty]
@@ -488,7 +492,7 @@
 
         ;; refinements are erased to their bound
         [((Refinement: S _) T)
-         (cg S T)]
+         (cg S T obj)]
 
         ;; variables that are in X and should be constrained
         ;; all other variables are compatible only with themselves
@@ -513,29 +517,31 @@
 
         ;; recursive names should get resolved as they're seen
         [(s (? Name? t))
-         (cg s (resolve-once t))]
+         (let ([t (resolve-once t)])
+           (and t (cg s t obj)))]
         [((? Name? s) t)
-         (cg (resolve-once s) t)]
+         (let ([s (resolve-once s)])
+           (and s (cg s t obj)))]
 
         ;; constrain b1 to be below T, but don't mention the new vars
         [((Poly: v1 b1) T) (cgen (context-add context #:bounds v1) b1 T)]
 
         ;; Mu's just get unfolded
-        [((? Mu? s) t) (cg (unfold s) t)]
-        [(s (? Mu? t)) (cg s (unfold t))]
+        [((? Mu? s) t) (cg (unfold s) t obj)]
+        [(s (? Mu? t)) (cg s (unfold t) obj)]
 
         ;; find *an* element of elems which can be made a subtype of T
         [((Intersection: ts raw-prop) T)
          (cset-join
           (for*/list ([t (in-list ts)]
-                      [v (in-value (cg t T))]
+                      [v (in-value (cg t T obj))]
                       #:when v)
             v))]
         
         ;; constrain S to be below *each* element of elems, and then combine the constraints
         [(S (Intersection: ts raw-prop))
-         (define cs (for/list/fail ([ts (in-list ts)]) (cg S ts)))
-         (let ([obj (-id-path (genid))])
+         (define cs (for/list/fail ([ts (in-list ts)]) (cg S ts obj)))
+         (let ([obj (if (Object? obj) obj (-id-path (genid)))])
            (and cs
                 (implies-in-env? (lexical-env)
                                  (-is-type obj S)
@@ -544,10 +550,10 @@
         
         ;; constrain *each* element of es to be below T, and then combine the constraints
         [((BaseUnion-bases: es) T)
-         (define cs (for/list/fail ([e (in-list es)]) (cg e T)))
+         (define cs (for/list/fail ([e (in-list es)]) (cg e T obj)))
          (and cs (cset-meet* (cons empty cs)))]
         [((Union-all: es) T)
-         (define cs (for/list/fail ([e (in-list es)]) (cg e T)))
+         (define cs (for/list/fail ([e (in-list es)]) (cg e T obj)))
          (and cs (cset-meet* (cons empty cs)))]
 
         [(_ (Bottom:)) no-cset]
@@ -558,16 +564,16 @@
         [(S (Union-all: es))
          (cset-join
           (for*/list ([e (in-list es)]
-                      [v (in-value (cg S e))]
+                      [v (in-value (cg S e obj))]
                       #:when v)
             v))]
         
         ;; from define-new-subtype
         [((Distinction: nm1 id1 S) (app resolve (Distinction: nm2 id2 T)))
          #:when (and (equal? nm1 nm2) (equal? id1 id2))
-         (cg S T)]
+         (cg S T obj)]
         [((Distinction: _ _ S) T)
-         (cg S T)]
+         (cg S T obj)]
 
         ;; two structs with the same name
         ;; just check pairwise on the fields
@@ -596,17 +602,23 @@
         [((Name: n _ #t) (Name: n* _ #t))
          (if (free-identifier=? n n*)
              empty ;; just succeed now
-             (% cg (resolve-once S) (resolve-once T)))]
+             (let ([S (resolve-once S)]
+                   [T (resolve-once T)])
+               (and S T (cg S T obj))))]
         ;; pairs are pointwise
         [((Pair: a b) (Pair: a* b*))
-         (% cset-meet (cg a a*) (cg b b*))]
+         (% cset-meet
+            (cg a a* (-car-of obj))
+            (cg b b* (-cdr-of obj)))]
         ;; sequences are covariant
         [((Sequence: ts) (Sequence: ts*))
          (cgen/list context ts ts*)]
         [((Listof: t) (Sequence: (list t*)))
          (cg t t*)]
         [((Pair: t1 t2) (Sequence: (list t*)))
-         (% cset-meet (cg t1 t*) (cg t2 (-lst t*)))]
+         (% cset-meet
+            (cg t1 t* (-car-of obj))
+            (cg t2 (-lst t*) (-cdr-of obj)))]
         [((MListof: t) (Sequence: (list t*)))
          (cg t t*)]
         ;; To check that mutable pair is a sequence we check that the cdr is
@@ -659,9 +671,11 @@
 
         ;; resolve applications
         [((App: _ _) _)
-         (% cg (resolve-once S) T)]
+         (let ([S (resolve-once S)])
+           (and S (cg S T obj)))]
         [(_ (App: _ _))
-         (% cg S (resolve-once T))]
+         (let ([T (resolve-once T)])
+           (and T (cg S T obj)))]
 
         ;; If the struct names don't match, try the parent of S
         ;; Needs to be done after App and Mu in case T is actually the current struct
@@ -850,16 +864,21 @@
 ;; expected-cset : a cset representing the expected type, to meet early and
 ;;  keep the number of constraints in check. (empty by default)
 ;; produces a cset which determines a substitution that makes the Ss subtypes of the Ts
-(define/cond-contract (cgen/list context S T
+(define/cond-contract (cgen/list context S T [objs '()]
                                  #:expected-cset [expected-cset (empty-cset '() '())])
-  ((context? (listof Values/c) (listof Values/c)) (#:expected-cset cset?) . ->* . (or/c cset? #f))
+  (->* (context? (listof Values/c) (listof Values/c))
+       ((listof (or/c #f OptObject?))
+        #:expected-cset cset?)
+       (or/c cset? #f))
   (and (= (length S) (length T))
        (% cset-meet*
-          (for/list/fail ([s (in-list S)] [t (in-list T)])
+          (for/list/fail ([s (in-list S)]
+                          [t (in-list T)]
+                          [obj (in-list/rest objs #f)])
                          ;; We meet early to prune the csets to a reasonable size.
                          ;; This weakens the inference a bit, but sometimes avoids
                          ;; constraint explosion.
-            (% cset-meet (cgen context s t) expected-cset)))))
+            (% cset-meet (cgen context s t obj) expected-cset)))))
 
 
 
@@ -874,22 +893,26 @@
 ;; just return a boolean result
 (define infer
  (let ()
-   (define/cond-contract (infer X Y S T R [expected #f] #:multiple? [multiple-substitutions? #f])
+   (define/cond-contract (infer X Y S T R [expected #f]
+                                #:multiple? [multiple-substitutions? #f]
+                                #:objs [objs '()])
      (((listof symbol?) (listof symbol?) (listof Type?) (listof Type?)
        (or/c #f Values/c ValuesDots?))
       ((or/c #f Values/c AnyValues? ValuesDots?)
-       #:multiple? boolean?)
+       #:multiple? boolean?
+       #:objs (listof OptObject?))
       . ->* . (or/c boolean?
                     substitution/c
                     (cons/c substitution/c
                             (listof substitution/c))))
-     (define ctx (context null X Y ))
+     (define ctx (context null X Y))
      (define expected-cset
        (if expected
            (cgen ctx R expected)
            (empty-cset '() '())))
      (and expected-cset
-          (let* ([cs (cgen/list ctx S T #:expected-cset expected-cset)]
+          (let* ([cs (cgen/list ctx S T objs
+                                #:expected-cset expected-cset)]
                  [cs* (% cset-meet cs expected-cset)])
             (and cs* (cond
                        [R (substs-gen cs* X Y R multiple-substitutions?)]
@@ -898,17 +921,20 @@
   infer)) ;to export a variable binding and not syntax
 
 ;; like infer, but T-var is the vararg type:
-(define (infer/vararg X Y S T T-var R [expected #f])
+(define (infer/vararg X Y S T T-var R [expected #f]
+                      #:objs [objs '()])
   (define new-T (if T-var (list-extend S T T-var) T))
   (and ((length S) . >= . (length T))
-       (infer X Y S new-T R expected)))
+       (infer X Y S new-T R expected #:objs objs)))
 
 ;; like infer, but dotted-var is the bound on the ...
 ;; and T-dotted is the repeated type
-(define (infer/dots X dotted-var S T T-dotted R must-vars #:expected [expected #f])
+(define (infer/dots X dotted-var S T T-dotted R must-vars
+                    #:expected [expected #f]
+                    #:objs [objs (map (λ (_) #f) S)])
   (early-return
-   (define short-S (take S (length T)))
-   (define rest-S (drop S (length T)))
+   (define-values (short-S rest-S) (split-at S (length T)))
+   (define-values (short-objs rest-objs) (split-at objs (length T)))
    ;; Generate a new type corresponding to T-dotted for every extra arg.
    (define-values (new-vars new-Ts)
      (generate-dbound-prefix dotted-var T-dotted (length rest-S) #f))
@@ -922,8 +948,12 @@
    #:return-unless expected-cset #f
    (define cs (% move-vars-to-dmap
                  (% cset-meet
-                    (cgen/list ctx short-S (map subst T) #:expected-cset expected-cset)
-                    (cgen/list ctx rest-S new-Ts #:expected-cset expected-cset))
+                    (cgen/list ctx short-S (map subst T)
+                               short-objs
+                               #:expected-cset expected-cset)
+                    (cgen/list ctx rest-S new-Ts
+                               rest-objs
+                               #:expected-cset expected-cset))
                  dotted-var new-vars))
    #:return-unless cs #f
    (define m (cset-meet cs expected-cset))
diff --git a/typed-racket-lib/typed-racket/infer/intersect.rkt b/typed-racket-lib/typed-racket/infer/intersect.rkt
index 3900e8da..85d2318c 100644
--- a/typed-racket-lib/typed-racket/infer/intersect.rkt
+++ b/typed-racket-lib/typed-racket/infer/intersect.rkt
@@ -11,7 +11,7 @@
 (export intersect^)
 
 
-(define ((intersect-types additive?) t1 t2 #:obj [obj -empty-obj])
+(define ((intersect-types additive?) t1 t2 [obj -empty-obj])
   (cond
     ;; we dispatch w/ Error first, because it behaves in
     ;; strange ways (e.g. it is ⊤ and ⊥ w.r.t subtyping) and
@@ -32,8 +32,8 @@
          [(_ _) #:when (not (overlap? t1 t2)) -Bottom]
       
          ;; already a subtype
-         [(_ _) #:when (subtype t1 t2 #:obj obj) t1]
-         [(_ _) #:when (subtype t2 t1 #:obj obj) t2]
+         [(_ _) #:when (subtype t1 t2 obj) t1]
+         [(_ _) #:when (subtype t2 t1 obj) t2]
 
      
          ;; polymorphic intersect
diff --git a/typed-racket-lib/typed-racket/infer/signatures.rkt b/typed-racket-lib/typed-racket/infer/signatures.rkt
index 05472d05..cff94782 100644
--- a/typed-racket-lib/typed-racket/infer/signatures.rkt
+++ b/typed-racket-lib/typed-racket/infer/signatures.rkt
@@ -21,8 +21,8 @@
    [cond-contracted c-meet ((c? c?) (symbol?) . ->* . (or/c #f c?))]))
 
 (define-signature intersect^
-  ([cond-contracted intersect ((Type? Type?) (#:obj OptObject?) . ->* . Type?)]
-   [cond-contracted restrict  ((Type? Type?) (#:obj OptObject?) . ->* . Type?)]))
+  ([cond-contracted intersect ((Type? Type?) (OptObject?) . ->* . Type?)]
+   [cond-contracted restrict  ((Type? Type?) (OptObject?) . ->* . Type?)]))
 
 (define-signature infer^
   ([cond-contracted infer ((;; variables from the forall
@@ -38,7 +38,8 @@
                            ;; optional expected type
                            ((or/c #f Values/c AnyValues? ValuesDots?)
                             ;; optional multiple substitutions?
-                            #:multiple? boolean?)
+                            #:multiple? boolean?
+                            #:objs (listof OptObject?))
                            . ->* . any)]
    [cond-contracted infer/vararg ((;; variables from the forall
                                    (listof symbol?)
@@ -53,7 +54,9 @@
                                    ;; range
                                    (or/c #f Values/c ValuesDots?))
                                   ;; [optional] expected type
-                                  ((or/c #f Values/c AnyValues? ValuesDots?)) . ->* . any)]
+                                  ((or/c #f Values/c AnyValues? ValuesDots?)
+                                   #:objs (listof OptObject?))
+                                  . ->* . any)]
    [cond-contracted infer/dots (((listof symbol?)
                                  symbol?
                                  (listof Values/c)
@@ -61,4 +64,6 @@
                                  Values/c
                                  (or/c Values/c ValuesDots?)
                                  (listof symbol?))
-                                (#:expected (or/c #f Values/c AnyValues? ValuesDots?)) . ->* . any)]))
+                                (#:expected (or/c #f Values/c AnyValues? ValuesDots?)
+                                 #:objs (listof OptObject?))
+                                . ->* . any)]))
diff --git a/typed-racket-lib/typed-racket/rep/object-rep.rkt b/typed-racket-lib/typed-racket/rep/object-rep.rkt
index 243f32bf..4ea86f2d 100644
--- a/typed-racket-lib/typed-racket/rep/object-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/object-rep.rkt
@@ -31,6 +31,7 @@
          genobj
          make-obj-seq
          obj-seq-next
+         scale-obj
          (rename-out [make-LExp* make-LExp]
                      [make-LExp raw-make-LExp])
          (all-from-out "fme-utils.rkt"))
@@ -283,18 +284,20 @@
   (cond
     [(or (Empty? o1) (Empty? o2)) -empty-obj]
     [(and (LExp? o1) (constant-LExp? o1))
-     => (scale-obj o2)]
+     => (λ (n) (scale-obj n o2))]
     [(and (LExp? o2) (constant-LExp? o2))
-     => (scale-obj o1)]
+     => (λ (n) (scale-obj n o1))]
     [else -empty-obj]))
 
-(define ((scale-obj o) c)
-  (match o
-    [(? Path?) (-lexp (list c o))]
+(define/cond-contract (scale-obj n obj)
+  (-> exact-integer? OptObject? OptObject?)
+  (match obj
+    [(? Path?) (-lexp (list n obj))]
     [(LExp: const terms)
      ;; scaling doesn't modify which objects are in the LExp! =)
      ;; just constants & coefficients
-     (make-LExp* (* c const) (terms-scale terms c))]))
+     (make-LExp* (* n const) (terms-scale terms n))]
+    [(Empty:) -empty-obj]))
 
 
 
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 6e7930ab..2c0ba0ed 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -1558,11 +1558,21 @@
      (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)]))
diff --git a/typed-racket-lib/typed-racket/typecheck/check-below.rkt b/typed-racket-lib/typed-racket/typecheck/check-below.rkt
index c03ea77a..53a8a401 100644
--- a/typed-racket-lib/typed-racket/typecheck/check-below.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/check-below.rkt
@@ -86,10 +86,10 @@
        (type-mismatch p2 p1 "mismatch in proposition"))
      (tc-any-results (fix-props p2 p1))]
 
-    [((or (tc-results: _ (list (PropSet: fs+ fs-) ...) _)
-          (tc-results: _ (list (PropSet: fs+ fs-) ...) _ _ _))
+    [((or (tc-results: _ (list (PropSet: ps+ ps-) ...) _)
+          (tc-results: _ (list (PropSet: ps+ ps-) ...) _ _ _))
       (tc-any-results: p2))
-     (define merged-prop (apply -and (map -or fs+ fs-)))
+     (define merged-prop (apply -and (map -or ps+ ps-)))
      (unless (prop-better? merged-prop p2)
        (type-mismatch p2 merged-prop "mismatch in proposition"))
      (tc-any-results (fix-props p2 merged-prop))]
@@ -97,7 +97,7 @@
 
     [((tc-result1: t1 p1 o1) (tc-result1: t2 p2 o2))
      (cond
-       [(not (subtype t1 t2))
+       [(not (subtype t1 t2 o1))
         (expected-but-got t2 t1)]
        [(and (not (prop-set-better? p1 p2))
              (object-better? o1 o2))
@@ -124,48 +124,53 @@
 
     [((tc-results: t1 p1 o1 dty1 dbound)
       (tc-results: t2 (list (or #f (PropSet: (TrueProp:) (TrueProp:))) ...)
-                      (list (or #f (Empty:)) ...) dty2 dbound))
+                   (list (or #f (Empty:)) ...) dty2 dbound))
      (cond
        [(= (length t1) (length t2))
-        (unless (andmap subtype t1 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)])
+        (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)
+        (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)])
+        (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:)) ...)))
+                   (list (or #f (Empty:)) ...)))
      (unless (= (length t1) (length t2))
        (value-mismatch expected tr1))
-     (unless (for/and ([t (in-list t1)] [s (in-list t2)]) (subtype t s))
+     (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)]) (subtype t s))
+     (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)) (=> continue)
-     (if (= (length t1) (length t2))
-         (continue)
-         (value-mismatch expected tr1))
+    [((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?))
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 903f12de..0432d250 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
@@ -38,7 +38,7 @@
                                "expected at least" (length dom)
                                "given" (length t-a)
                                #:delayed? #t)])
-       (for ([dom-t (if rest (in-sequence-forever dom rest) (in-list dom))]
+       (for ([dom-t (if rest (in-list/rest dom rest) (in-list dom))]
              [a (in-syntax args-stx)]
              [arg-t (in-list t-a)])
          (parameterize ([current-orig-stx a]) (check-below arg-t dom-t))))
@@ -48,8 +48,8 @@
        (let-values
            ([(o-a t-a) (for/lists (os ts)
                          ([_ (in-range dom-count)]
-                          [oa (in-sequence-forever (in-list o-a) -empty-obj)]
-                          [ta (in-sequence-forever (in-list t-a) Univ)])
+                          [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
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
index f4ab20be..5669740e 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
@@ -88,7 +88,7 @@
   ;; vector-ref on het vectors
   (pattern (~and form ((~or vector-ref unsafe-vector-ref unsafe-vector*-ref) vec:expr index:expr))
     (match (single-value #'vec)
-      [(tc-result1: (and vec-t (app resolve (HeterogeneousVector: es))))
+      [(tc-result1: (and vec-t (app resolve (Is-a: (HeterogeneousVector: es)))))
        (tc/hetero-ref #'index es vec-t "vector")]
       [v-ty (tc/app-regular #'form expected)]))
   ;; unsafe struct-set! 
@@ -100,17 +100,17 @@
   ;; vector-set! on het vectors
   (pattern (~and form ((~or vector-set! unsafe-vector-set! unsafe-vector*-set!) v:expr index:expr val:expr))
     (match (single-value #'v)
-      [(tc-result1: (and vec-t (app resolve (HeterogeneousVector: es))))
+      [(tc-result1: (and vec-t (app resolve (Is-a: (HeterogeneousVector: es)))))
        (tc/hetero-set! #'index es #'val vec-t "vector")]
       [v-ty (tc/app-regular #'form expected)]))
   (pattern (~and form ((~or vector-immutable vector) args:expr ...))
     (match expected
-      [(tc-result1: (app resolve (Vector: t)))
+      [(tc-result1: (app resolve (Is-a: (Vector: t))))
        (ret (make-HeterogeneousVector 
               (for/list ([e (in-syntax #'(args ...))])
                 (tc-expr/check e (ret t))
                 t)))]
-      [(tc-result1: (app resolve (HeterogeneousVector: ts)))
+      [(tc-result1: (app resolve (Is-a: (HeterogeneousVector: ts))))
        (cond
          [(= (length ts) (syntax-length #'(args ...)))
           (ret
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 8f06abf7..09844f1c 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
@@ -86,16 +86,21 @@
             (map single-value args*)]
            [(Function:
               (app matching-arities
-                (list (arr: doms ranges rests drests _) ..1)))
-            (define matching-domains
-              (in-values-sequence
-                (apply in-parallel
-                  (for/list ((dom (in-list doms)) (rest (in-list rests)))
-                    (in-sequences (in-list dom) (in-cycle (in-value rest)))))))
-            (for/list ([a (in-list args*)] [types matching-domains])
-              (match-define (cons t ts) types)
-              (if (for/and ((t2 (in-list ts))) (equal? t t2))
-                  (tc-expr/check a (ret t))
-                  (single-value a)))]
+                (list (arr: doms _ rests _ _) ..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
+            (for/list ([arg-stx (in-list args*)]
+                       [arg-idx (in-naturals)])
+              (define dom-ty (list-ref/default (car doms)
+                                               arg-idx
+                                               (car rests)))
+              (cond
+                [(for/and ([dom (in-list doms)]
+                           [rest (in-list rests)])
+                   (equal? dom-ty
+                           (list-ref/default dom arg-idx rest)))
+                 (tc-expr/check arg-stx (ret dom-ty))]
+                [else (single-value arg-stx)]))]
            [_ (map single-value args*)]))
        (tc/funapp #'f #'args f-ty arg-tys expected))]))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
index 0d73b236..858cbecd 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
@@ -51,7 +51,7 @@
                      (loop ps negs (append new-props new) (env-set-id-type Γ x new-t))]))]
                [(TypeProp: obj pt)
                 (let ([t (lookup-obj-type/lexical obj Γ #:fail (λ (_) Univ))])
-                  (define new-t (intersect t pt #:obj obj))
+                  (define new-t (intersect t pt obj))
                   (cond
                     [(Bottom? new-t) #f]
                     [(equal? t new-t) (loop ps negs new Γ)]
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 7e54dfe8..588f7d7d 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
@@ -21,12 +21,14 @@
          racket/extflonum
          ;; Needed for current implementation of typechecking letrec-syntax+values
          (for-template (only-in racket/base list letrec-values
-                                + * < <= = >= >)
+                                + - * < <= = >= > add1 sub1 modulo
+                                min max vector-length random)
                        ;; see tc-app-contracts.rkt
                        racket/contract/private/provide)
 
          (for-label (only-in '#%paramz [parameterization-key pz:pk])
-                    (only-in racket/private/class-internal find-method/who)))
+                    (only-in racket/private/class-internal find-method/who))
+         (for-syntax racket/base racket/syntax))
 
 (import tc-if^ tc-lambda^ tc-app^ tc-let^ tc-send^ check-subforms^ tc-literal^
         check-class^ check-unit^ tc-expression^)
@@ -398,7 +400,7 @@
        [(HeterogeneousVector: ts)
         (make-HeterogeneousVector
          (for/list ([x (in-list xs)]
-                    [t (in-sequence-forever (in-list ts) #f)])
+                    [t (in-list/rest ts #f)])
            (cond-check-below (find-stx-type x t) t)))]
        [_ (make-HeterogeneousVector (for/list ([x (in-list xs)])
                                       (generalize (find-stx-type x #f))))])]
@@ -426,20 +428,32 @@
 ;; adds linear info for the following operations:
 ;; + * < <= = >= >
 ;; when the arguments are integers w/ objects
+;; a lot of the content in this function should eventually
+;; just be moved to the actual types of the respective
+;; racket identifiers, but in an effort to move progress forward
+;; and not break programs currently typechecking, this more
+;; explicit, hard-coded helper will do (i.e. some of these functions
+;; currently have extremely large types in TR -- modifying their
+;; type is not always trivial)
 (define (add-applicable-linear-info form result)
   ;; class to recognize expressions that typecheck at a subtype of -Int
   ;; and whose object is non-empty
-  (define-syntax-class int/obj
+  (define-syntax-class (t/obj type)
     #:attributes (obj)
     (pattern e:expr
              #:do [(define o
                      (match (type-of #'e)
                        [(tc-result1: t _ (? Object? o))
-                        #:when (subtype t -Int)
+                        #:when (subtype t type)
                         o]
                        [_ #f]))]
-             #:fail-unless o "not an integer with a non-empty object"
+             #:fail-unless o (format "not a ~a expr with a non-empty object" type)
              #:attr obj o))
+  (define-syntax (obj stx)
+    (syntax-case stx ()
+      [(_ e)
+       (with-syntax ([e* (format-id #'e "~a.obj" (syntax->datum #'e))])
+         (syntax/loc #'e (attribute e*)))]))
   ;; class to recognize int comparisons and associate their
   ;; internal TR prop constructors
   (define-syntax-class int-comparison
@@ -474,32 +488,90 @@
   ;; inspect the function appplication to see if it is a linear
   ;; integer compatible form we want to enrich with info when
   ;; #:with-linear-integer-arithmetic is specified by the user
-  (syntax-parse form
-    [(#%plain-app (~literal *) e1:int/obj e2:int/obj)
-     (match result
-       [(tc-result1: t ps _)
-        (define o1*o2 (-obj* (attribute e1.obj) (attribute e2.obj)))
+  (match result
+    [(tc-result1: ret-t ps _)
+     (syntax-parse form
+       ;; *
+       [(#%plain-app (~literal *) (~var e1 (t/obj -Int)) (~var es (t/obj -Int)) ...)
+        (define product-obj (apply -obj* (obj e1) (obj es)))
         (cond
-          [(Object? o1*o2)
-           (ret (-refine/fresh x t (-eq (-lexp x) o1*o2))
+          [(Object? product-obj)
+           (ret (-refine/fresh x ret-t (-eq (-lexp x) product-obj))
                 ps
-                o1*o2)]
+                product-obj)]
           [else result])]
-       [_ result])]
-    [(#%plain-app (~literal +) e:int/obj es:int/obj ...)
-     (match result
-       [(tc-result1: t ps _)
-        (define l (apply -lexp (attribute e.obj) (attribute es.obj)))
-        (ret (-refine/fresh x t (-eq (-lexp x) l))
+       ;; +
+       [(#%plain-app (~literal +) (~var e (t/obj -Int)) (~var es (t/obj -Int)) ...)
+        (define l (apply -lexp (obj e) (obj es)))
+        (ret (-refine/fresh x ret-t (-eq (-lexp x) l))
              ps
-             l)])]
-    [(#%plain-app comp:int-comparison
-                  e1:int/obj
-                  e2:int/obj
-                  es:int/obj ...)
-     (define p (apply -and (comparison-props (attribute comp.constructor)
-                                             (attribute e1.obj)
-                                             (attribute e2.obj)
-                                             (attribute es.obj))))
-     (add-p/not-p result p)]
+             l)]
+       ;; -
+       [(#%plain-app (~literal -) (~var e (t/obj -Int)) (~var es (t/obj -Int)) ...)
+        (define l (apply -lexp
+                         (obj e)
+                         (for/list ([o (in-list (obj es))])
+                           (scale-obj -1 o))))
+        (ret (-refine/fresh x ret-t (-eq (-lexp x) l))
+             ps
+             l)]
+       ;; add1
+       [(#%plain-app (~literal add1) (~var e (t/obj -Int)))
+        (define l (-lexp 1 (obj e)))
+        (ret (-refine/fresh x ret-t (-eq (-lexp x) l))
+             ps
+             l)]
+       ;; sub1
+       [(#%plain-app (~literal sub1) (~var e (t/obj -Int)))
+        (define l (-lexp -1 (obj e)))
+        (ret (-refine/fresh x ret-t (-eq (-lexp x) l))
+             ps
+             l)]
+       ;; modulo
+       [(#%plain-app (~literal modulo) (~var e1 (t/obj -Int)) (~var e2 (t/obj -Nat)))
+        (ret (-refine/fresh x ret-t (-lt (-lexp x) (obj e2)))
+             ps
+             -empty-obj)]
+       ;; max
+       [(#%plain-app (~literal max) (~var e1 (t/obj -Int)) (~var es (t/obj -Int)) ...)
+        (ret (-refine/fresh x ret-t
+                            (apply -and (let ([l (-lexp x)])
+                                          (for/list ([o (in-list (cons (obj e1) (obj es)))])
+                                            (-geq l o)))))
+             ps
+             -empty-obj)]
+       ;; min
+       [(#%plain-app (~literal min) (~var e1 (t/obj -Int)) (~var es (t/obj -Int)) ...)
+        (ret (-refine/fresh x ret-t
+                            (apply -and (let ([l (-lexp x)])
+                                          (for/list ([o (in-list (cons (obj e1) (obj es)))])
+                                            (-leq l o)))))
+             ps
+             -empty-obj)]
+       ;; random
+       [(#%plain-app (~literal random) (~var e1 (t/obj -Int)))
+        (ret (-refine/fresh x ret-t (-lt (-lexp x) (obj e1)))
+             ps
+             -empty-obj)]
+       [(#%plain-app (~literal random) (~var e1 (t/obj -Int)) (~var e2 (t/obj -Int)))
+        (ret (-refine/fresh x ret-t (-and (-leq (obj e1) (-lexp x))
+                                          (-lt (-lexp x) (obj e2))))
+             ps
+             -empty-obj)]
+       ;; vector-length
+       [(#%plain-app (~literal vector-length) (~var e1 (t/obj -VectorTop)))
+        (define l (-vec-len-of (obj e1)))
+        (ret (-refine/fresh x ret-t (-eq (-lexp x) l))
+             ps
+             l)]
+       [(#%plain-app comp:int-comparison
+                     (~var e1 (t/obj -Int))
+                     (~var e2 (t/obj -Int))
+                     (~var es (t/obj -Int)) ...)
+        (define p (apply -and (comparison-props (attribute comp.constructor)
+                                                (obj e1)
+                                                (obj e2)
+                                                (obj es))))
+        (add-p/not-p result p)]
+       [_ result])]
     [_ result]))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
index fbd56590..ceed66e3 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
@@ -111,13 +111,20 @@
                            [drest
                             (infer/dots
                              fixed-vars dotted-var argtys dom (car drest) rng (fv rng)
-                             #:expected (and expected (tc-results->values expected)))]
+                             #: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)))]
+                                          (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)))])))
+                           [else (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)]
@@ -141,7 +148,8 @@
          (let ([rng (subst-dom-objs argtys argobjs rng)])
            (extend-tvars vars
                          (infer/vararg vars null argtys dom rest rng
-                                       (and expected (tc-results->values expected)))))
+                                       (and expected (tc-results->values expected))
+                                       #:objs argobjs)))
          #:function-type f-type
          #:args-results args-res
          #:expected expected)]
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt b/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt
index 847cfb27..fe6c19d6 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt
@@ -31,7 +31,7 @@
     (pattern (~and i (~or :number :str :bytes :char))
              #:fail-unless expected #f
              #:fail-unless (let ([n (syntax-e #'i)])
-                             (subtype (-val n) expected #:obj (if (exact-integer? n) (-lexp n) -empty-obj))) #f))
+                             (subtype (-val n) expected (if (exact-integer? n) (-lexp n) -empty-obj))) #f))
   (syntax-parse v-stx
     [i:exp expected]
     [i:boolean (-val (syntax-e #'i))]
@@ -113,21 +113,26 @@
        [t 
         (-pair (tc-literal #'i) (tc-literal #'r))])]
     [(~var i (3d vector?))
-     (match (and expected (resolve (intersect expected -VectorTop)))
-       [(Vector: t)
-        (make-Vector
-          (check-below
-            (apply Un
-              (for/list ([l (in-vector (syntax-e #'i))])
-                (tc-literal l t)))
+     (define vec-val (syntax-e #'i))
+     (define vec-ty
+       (match (and expected (resolve (intersect expected -VectorTop)))
+         [(Is-a: (Vector: t))
+          (make-Vector
+           (check-below
+            (apply Un (for/list ([l (in-vector vec-val)])
+                        (tc-literal l t)))
             t))]
-       [(HeterogeneousVector: ts)
-        (make-HeterogeneousVector
-         (for/list ([l (in-vector (syntax-e #'i))]
-                    [t (in-sequence-forever (in-list ts) #f)])
-           (cond-check-below (tc-literal l t) t)))]
-       [_ (make-HeterogeneousVector (for/list ([l (in-vector (syntax-e #'i))])
-                                      (generalize (tc-literal l #f))))])]
+         [(Is-a: (HeterogeneousVector: ts))
+          (make-HeterogeneousVector
+           (for/list ([l (in-vector (syntax-e #'i))]
+                      [t (in-list/rest ts #f)])
+             (cond-check-below (tc-literal l t) t)))]
+         [_ (make-HeterogeneousVector (for/list ([l (in-vector (syntax-e #'i))])
+                                        (generalize (tc-literal l #f))))]))
+     (if (with-linear-integer-arithmetic?)
+         (-refine/fresh v vec-ty (-eq (-lexp (vector-length vec-val))
+                                      (-vec-len-of (-id-path v))))
+         vec-ty)]
     [(~var i (3d hash?))
      (match (and expected (resolve (intersect expected -HashtableTop)))
        [(Hashtable: k v)
@@ -149,7 +154,7 @@
 (define (tc-prefab struct-inst expected)
   (define expected-ts
     (match (and expected (resolve expected))
-      [(Prefab: _ ts) (in-sequence-forever (in-list ts) #f)]
+      [(Prefab: _ ts) (in-list/rest ts #f)]
       [_ (in-cycle (in-value #f))]))
   (define key (prefab-struct-key struct-inst))
   (define struct-vec (struct->vector struct-inst))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
index 55bf5c14..21976e72 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
@@ -38,11 +38,11 @@
 ;; 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 (map (λ (_) Univ) os)])
+(define (values->tc-results v os [ts '()])
   (define targets
     (for/list ([o (in-list os)]
                [arg (in-naturals)]
-               [t (in-list ts)])
+               [t (in-list/rest ts Univ)])
       (list (cons 0 arg) o t)))
   (define res
     (match v
@@ -177,7 +177,7 @@
             (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 obj))
+               (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]
@@ -197,8 +197,8 @@
             (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 obj))
-               (define new-neg-obj-ty (restrict neg-obj-ty inner-obj-ty-at-flds #:obj obj))
+               (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]
diff --git a/typed-racket-lib/typed-racket/types/match-expanders.rkt b/typed-racket-lib/typed-racket/types/match-expanders.rkt
index d6691c19..326fe58c 100644
--- a/typed-racket-lib/typed-racket/types/match-expanders.rkt
+++ b/typed-racket-lib/typed-racket/types/match-expanders.rkt
@@ -11,9 +11,27 @@
 (provide Listof: List: MListof: AnyPoly: AnyPoly-names: Function/arrs:
          SimpleListof: SimpleMListof:
          PredicateProp:
-         Val-able:)
+         Val-able:
+         Is-a:)
 
 
+;; matches types that are exactly the pattern,
+;; or that are an intersection type of some kind where
+;; exactly 1 of the types in the intersection is of the type
+(define-match-expander Is-a:
+  (lambda (stx)
+    (syntax-parse stx
+      [(_ pat)
+       (syntax/loc stx
+         (or pat
+             (Intersection: (or (list pat)
+                                (app (λ (ts) (filter (match-lambda
+                                                       [pat #t]
+                                                       [_ #f])
+                                                     ts))
+                                     (list pat)))
+                            _)))])))
+
 ;; some types used to be represented by a Value rep,
 ;; but are now represented by a Base rep. This function
 ;; helps us recover the singleton values for those types.
@@ -27,15 +45,14 @@
     [(== -One) (box-immutable 1)]
     [_ #f]))
 
+;; matches types that correspond to singleton values
 (define-match-expander Val-able:
   (lambda (stx)
     (syntax-parse stx
       [(_ pat)
        (syntax/loc stx
-         (or (Value: pat)
-             (app Base->val? (box pat))
-             (Intersection: (list (or (Value: pat)
-                                      (app Base->val? (box pat)))) _)))])))
+         (Is-a: (or (Value: pat)
+                    (app Base->val? (box pat)))))])))
 
 (define-match-expander Listof:
   (lambda (stx)
diff --git a/typed-racket-lib/typed-racket/types/prop-ops.rkt b/typed-racket-lib/typed-racket/types/prop-ops.rkt
index fe4ff29f..a3cc52af 100644
--- a/typed-racket-lib/typed-racket/types/prop-ops.rkt
+++ b/typed-racket-lib/typed-racket/types/prop-ops.rkt
@@ -67,16 +67,15 @@
 
 ;; atomic-contradiction?: Prop? Prop? -> boolean?
 ;; Returns true if the AND of the two props is equivalent to FalseProp
-(define (atomic-contradiction? p1 p2)
-  (match* (p1 p2)
-    [((TypeProp: o1 t1) (NotTypeProp: o2 t2))
-     (and (eq? o1 o2) (subtype t1 t2 #:obj o1))]
-    [((NotTypeProp: o2 t2) (TypeProp: o1 t1))
-     (and (eq? o1 o2) (subtype t1 t2 #:obj o1))]
-    [((? LeqProp?) (? LeqProp?)) (contradictory-Leqs? p1 p2)]
-    [((FalseProp:) _) #t]
-    [(_ (FalseProp:)) #t]
-    [(_ _) #f]))
+(define/match (atomic-contradiction? p1 p2)
+  [((TypeProp: o1 t1) (NotTypeProp: o2 t2))
+   (and (eq? o1 o2) (subtype t1 t2 o1))]
+  [((NotTypeProp: o2 t2) (TypeProp: o1 t1))
+   (and (eq? o1 o2) (subtype t1 t2 o1))]
+  [((? LeqProp?) (? LeqProp?)) (contradictory-Leqs? p1 p2)]
+  [((FalseProp:) _) #t]
+  [(_ (FalseProp:)) #t]
+  [(_ _) #f])
 
 
 ;; do pes1 and pes2 share a common suffix and,
@@ -129,75 +128,72 @@
 
 ;; like atomic-contradiction? but it tries a little
 ;; harder, reasoning about how paths overlap
-(define (contradiction? p1 p2)
-  (match* (p1 p2)
-    [((FalseProp:) _) #t]
-    [(_ (FalseProp:)) #t]
-    [((TypeProp: o t1) (NotTypeProp: o t2)) (subtype t1 t2 #:obj o)]
-    [((NotTypeProp: o t2) (TypeProp: o t1)) (subtype t1 t2 #:obj o)]
-    [((? LeqProp?) (? LeqProp?)) (contradictory-Leqs? p1 p2)]
-    [((TypeProp: (Path: pes1 x1) t1)
-      (TypeProp: (Path: pes2 x2) t2))
-     #:when (name-ref=? x1 x2)
-     (updates/pos-to-bot? pes1 t1 pes2 t2)]
-    [((TypeProp:    (Path: pes1 x1) t1)
-      (NotTypeProp: (Path: pes2 x2) t2))
-     #:when (name-ref=? x1 x2)
-     (updates/neg-to-bot? pes1 t1 pes2 t2)]
-    [((NotTypeProp: (Path: pes2 x2) t2)
-      (TypeProp:    (Path: pes1 x1) t1))
-     #:when (name-ref=? x1 x2)
-     (updates/neg-to-bot? pes1 t1 pes2 t2)]
-    [(_ _) #f]))
+(define/match (contradiction? p1 p2)
+  [((FalseProp:) _) #t]
+  [(_ (FalseProp:)) #t]
+  [((TypeProp: o t1) (NotTypeProp: o t2)) (subtype t1 t2 o)]
+  [((NotTypeProp: o t2) (TypeProp: o t1)) (subtype t1 t2 o)]
+  [((? LeqProp?) (? LeqProp?)) (contradictory-Leqs? p1 p2)]
+  [((TypeProp: (Path: pes1 x1) t1)
+    (TypeProp: (Path: pes2 x2) t2))
+   #:when (name-ref=? x1 x2)
+   (updates/pos-to-bot? pes1 t1 pes2 t2)]
+  [((TypeProp:    (Path: pes1 x1) t1)
+    (NotTypeProp: (Path: pes2 x2) t2))
+   #:when (name-ref=? x1 x2)
+   (updates/neg-to-bot? pes1 t1 pes2 t2)]
+  [((NotTypeProp: (Path: pes2 x2) t2)
+    (TypeProp:    (Path: pes1 x1) t1))
+   #:when (name-ref=? x1 x2)
+   (updates/neg-to-bot? pes1 t1 pes2 t2)]
+  [(_ _) #f])
 
 
 ;; atomic-complement?: Prop? Prop? -> boolean?
 ;; Returns true if the OR of the two props is equivalent to Top
-(define (atomic-complement? p1 p2)
-  (match* (p1 p2)
-    [((TypeProp: o1 t1) (NotTypeProp: o2 t2))
-     (and (eq? o1 o2) (subtype t2 t1 #:obj o1))]
-    [((NotTypeProp: o2 t2) (TypeProp: o1 t1))
-     (and (eq? o1 o2) (subtype t2 t1 #:obj o1))]
-    [((? LeqProp?) (? LeqProp?)) (complementary-Leqs? p1 p2)]
-    [((TrueProp:) _) #t]
-    [(_ (TrueProp:)) #t]
-    [(_ _) #f]))
+(define/match (atomic-complement? p1 p2)
+  [((TypeProp: o1 t1) (NotTypeProp: o2 t2))
+   (and (eq? o1 o2) (subtype t2 t1 o1))]
+  [((NotTypeProp: o2 t2) (TypeProp: o1 t1))
+   (and (eq? o1 o2) (subtype t2 t1 o1))]
+  [((? LeqProp?) (? LeqProp?)) (complementary-Leqs? p1 p2)]
+  [((TrueProp:) _) #t]
+  [(_ (TrueProp:)) #t]
+  [(_ _) #f])
 
 ;; does p imply q? (but only directly/simply)
 ;; NOTE: because Ors and Atomic props are
 ;; interned, we use eq? and memq
-(define (atomic-implies? p q)
-  (match* (p q)
-    ;; reflexivity
-    [(_ _) #:when (or (eq? p q)
-                      (TrueProp? q)
-                      (FalseProp? p)) #t]
-    ;; ps ⊆ qs ?
-    [((OrProp: ps) (OrProp: qs))
-     (and (for/and ([p (in-list ps)])
-            (memq p qs))
-          #t)]
-    ;; p ∈ qs ?
-    [(p (OrProp: qs)) (and (memq p qs) #t)]
-    ;; q ∈ ps ?
-    [((AndProp: ps) q) (or (equal? p q) (and (memq q ps) #t))]
-    ;; t1 <: t2 ?
-    [((TypeProp: o1 t1)
-      (TypeProp: o2 t2))
-     (and (eq? o1 o2) (subtype t1 t2 #:obj o1))]
-    ;; t2 <: t1 ?
-    [((NotTypeProp: o1 t1)
-      (NotTypeProp: o2 t2))
-     (and (eq? o1 o2) (subtype t2 t1 #:obj o1))]
-    ;; t1 ∩ t2 = ∅ ?
-    [((TypeProp:    o1 t1)
-      (NotTypeProp: o2 t2))
-     (and (eq? o1 o2) (not (overlap? t1 t2)))]
-    [((? LeqProp? p) (? LeqProp? q))
-     (Leq-implies-Leq? p q)]
-    ;; otherwise we give up
-    [(_ _) #f]))
+(define/match (atomic-implies? p q)
+  ;; reflexivity
+  [(_ _) #:when (or (eq? p q)
+                    (TrueProp? q)
+                    (FalseProp? p)) #t]
+  ;; ps ⊆ qs ?
+  [((OrProp: ps) (OrProp: qs))
+   (and (for/and ([p (in-list ps)])
+          (memq p qs))
+        #t)]
+  ;; p ∈ qs ?
+  [(p (OrProp: qs)) (and (memq p qs) #t)]
+  ;; q ∈ ps ?
+  [((AndProp: ps) q) (or (equal? p q) (and (memq q ps) #t))]
+  ;; t1 <: t2 ?
+  [((TypeProp: o1 t1)
+    (TypeProp: o2 t2))
+   (and (eq? o1 o2) (subtype t1 t2 o1))]
+  ;; t2 <: t1 ?
+  [((NotTypeProp: o1 t1)
+    (NotTypeProp: o2 t2))
+   (and (eq? o1 o2) (subtype t2 t1 o1))]
+  ;; t1 ∩ t2 = ∅ ?
+  [((TypeProp:    o1 t1)
+    (NotTypeProp: o2 t2))
+   (and (eq? o1 o2) (not (overlap? t1 t2)))]
+  [((? LeqProp? p) (? LeqProp? q))
+   (Leq-implies-Leq? p q)]
+  ;; otherwise we give up
+  [(_ _) #f])
 
 (define (implies? p q)
   (FalseProp? (-and p (negate-prop q))))
@@ -227,8 +223,8 @@
   (match props
     [(or (list) (list _)) props]
     [_
-     (define tf-map (make-hash))
-     (define ntf-map (make-hash))
+     (define tf-map (make-hasheq))
+     (define ntf-map (make-hasheq))
 
      ;; consolidate type info and separate out other props
      (define-values (leqs others)
@@ -246,9 +242,9 @@
            [_ (values leqs (cons prop others))])))
      ;; convert consolidated types into props and gather everything
      (define raw-results
-       (append (for/list ([(k v) (in-hash tf-map)])
+       (append (for/list ([(k v) (in-mutable-hash tf-map)])
                  (-is-type k v))
-               (for/list([(k v) (in-hash ntf-map)])
+               (for/list([(k v) (in-mutable-hash ntf-map)])
                  (-not-type k v))
                leqs
                others))
@@ -269,16 +265,15 @@
 
 ;; negate-prop: Prop? -> Prop?
 ;; Logically inverts a prop.
-(define (negate-prop p)
-  (match p
-    [(? FalseProp?) -tt]
-    [(? TrueProp?) -ff]
-    [(TypeProp: o t) (-not-type o t)]
-    [(NotTypeProp: o t) (-is-type o t)]
-    [(AndProp: ps) (apply -or (map negate-prop ps))]
-    [(OrProp: ps) (apply -and (map negate-prop ps))]
-    [(LeqProp: lhs rhs)
-     (-leq (-lexp-add1 rhs) lhs)]))
+(define/match (negate-prop p)
+  [((? FalseProp?)) -tt]
+  [((? TrueProp?)) -ff]
+  [((TypeProp: o t)) (-not-type o t)]
+  [((NotTypeProp: o t)) (-is-type o t)]
+  [((AndProp: ps)) (apply -or (map negate-prop ps))]
+  [((OrProp: ps)) (apply -and (map negate-prop ps))]
+  [((LeqProp: lhs rhs))
+   (-leq (-lexp-add1 rhs) lhs)])
 
 ;; -or
 ;; (listof Prop?) -> Prop?
@@ -286,46 +281,55 @@
 ;; Smart 'normalizing' constructor for disjunctions. The result
 ;; will be a disjunction of only atomic propositions (i.e. a clause
 ;; in a CNF formula)
-(define (-or . args)
-  (define mk
-    (match-lambda [(list) -ff]
-                  [(list p) p]
-                  [ps (make-OrProp ps)]))
-  (define (distribute args)
-    (define-values (ands others) (partition AndProp? args))
-    (if (null? ands)
-        (mk others)
-        (match-let ([(AndProp: elems) (car ands)])
-          (apply -and (for/list ([a (in-list elems)])
-                        (apply -or a (append (cdr ands) others)))))))
-  (define (flatten-ors/remove-duplicates ps)
-    (let loop ([ps ps]
-               [result '()])
-      (match ps
-        [(cons p rst)
-         (match p
-           [(OrProp: ps*) (loop rst (append ps* result))]
-           [_ (loop rst (cons p result))])]
-        [_ (remove-duplicates result)])))
-  (let loop ([ps (flatten-ors/remove-duplicates args)]
-             [result null])
-    (match ps
-      [(cons cur rst)
-       (cond
-         ;; trivial cases
-         [(TrueProp? cur) -tt]
-         [(FalseProp? cur) (loop rst result)]
-         ;; is there a complementary case e.g. (ϕ ∨ ¬ϕ)? if so abort
-         [(for/or ([p (in-list rst)])    (atomic-complement? p cur)) -tt]
-         [(for/or ([p (in-list result)]) (atomic-complement? p cur)) -tt]
-         ;; don't include 'cur' if its covered by another prop
-         [(for/or ([p (in-list rst)]) (atomic-implies? cur p))
-          (loop rst result)]
-         [(for/or ([p (in-list result)]) (atomic-implies? cur p))
-          (loop rst result)]
-         ;; otherwise keep 'cur' in this disjunction
-         [else (loop rst (cons cur result))])]
-      [_ (distribute (compact result #t))])))
+(define/match (-or . args)
+  ;; specialize for trivial <=2 arg cases
+  [((list)) -ff]
+  [((list p)) p]
+  [((list p p)) p]
+  [((list (TrueProp:) p)) -tt]
+  [((list p (TrueProp:))) -tt]
+  [((list (FalseProp:) p)) p]
+  [((list p (FalseProp:))) p]
+  [(args)
+   (define mk
+     (match-lambda [(list) -ff]
+                   [(list p) p]
+                   [ps (make-OrProp ps)]))
+   (define (distribute args)
+     (define-values (ands others) (partition AndProp? args))
+     (if (null? ands)
+         (mk others)
+         (match-let ([(AndProp: elems) (car ands)])
+           (apply -and (for/list ([a (in-list elems)])
+                         (apply -or a (append (cdr ands) others)))))))
+   (define (flatten-ors/remove-duplicates ps)
+     (let loop ([ps ps]
+                [result '()])
+       (match ps
+         [(cons p rst)
+          (match p
+            [(OrProp: ps*) (loop rst (append ps* result))]
+            [_ (loop rst (cons p result))])]
+         [_ (remove-duplicates result)])))
+   (let loop ([ps (flatten-ors/remove-duplicates args)]
+              [result null])
+     (match ps
+       [(cons cur rst)
+        (cond
+          ;; trivial cases
+          [(TrueProp? cur) -tt]
+          [(FalseProp? cur) (loop rst result)]
+          ;; is there a complementary case e.g. (ϕ ∨ ¬ϕ)? if so abort
+          [(for/or ([p (in-list rst)])    (atomic-complement? p cur)) -tt]
+          [(for/or ([p (in-list result)]) (atomic-complement? p cur)) -tt]
+          ;; don't include 'cur' if its covered by another prop
+          [(for/or ([p (in-list rst)]) (atomic-implies? cur p))
+           (loop rst result)]
+          [(for/or ([p (in-list result)]) (atomic-implies? cur p))
+           (loop rst result)]
+          ;; otherwise keep 'cur' in this disjunction
+          [else (loop rst (cons cur result))])]
+       [_ (distribute (compact result #t))]))])
 
 ;; -and
 ;; (listof Prop?) -> Prop?
@@ -333,105 +337,111 @@
 ;; Smart 'normalizing' constructor for conjunctions. The result
 ;; will be a conjunction of only atomic propositions and disjunctions
 ;; (i.e. a CNF proposition)
-(define (-and . args)
-  (define mk
-    (match-lambda [(list) -tt]
-                  [(list p) p]
-                  [ps (make-AndProp ps)]))
-  ;; we remove duplicates and organize the props so that the
-  ;; strongest ones come first (note: this includes considering
-  ;; smaller ors before larger ors)
-  (define (flatten-ands/remove-duplicates/order ps)
-    (define ts '())
-    (define nts '())
-    (define ors (make-hash))
-    (define others '())
-    (let partition! ([ps ps])
-      (for ([p (in-list ps)])
-        (match p
-          [(? TypeProp?) (set! ts (cons p ts))]
-          [(? NotTypeProp?) (set! nts (cons p nts))]
-          [(OrProp: ps*) (hash-update! ors (length ps*) (λ (l) (cons p l)) '())]
-          [(AndProp: ps*) (partition! ps*)]
-          [_ (set! others (cons p others))])))
-    (define ors-smallest-to-largest
-      (append-map cdr (sort (hash->list ors)
-                            (λ (len/ors1 len/ors2)
-                              (< (car len/ors1) (car len/ors2))))))
-    (remove-duplicates (append ts nts others ors-smallest-to-largest) eq?))
-  (let loop ([ps (flatten-ands/remove-duplicates/order args)]
-             [result null])
-    (match ps
-      [(cons cur rst)
-       (cond
-         ;; trivial cases
-         [(FalseProp? cur) -ff]
-         [(TrueProp? cur) (loop rst result)]
-         ;; is there a contradition e.g. (ϕ ∧ ¬ϕ), if so abort
-         [(for/or ([p (in-list rst)])    (atomic-contradiction? p cur)) -ff]
-         [(for/or ([p (in-list result)]) (atomic-contradiction? p cur)) -ff]
-         ;; don't include 'cur' if its implied by another prop
-         ;; already in our result (this is why we order the props!)
-         [(for/or ([p (in-list result)]) (atomic-implies? p cur))
-          (loop rst result)]
-         ;; otherwise keep 'cur' in this conjunction
-         [else (loop rst (cons cur result))])]
-      [_ (mk (compact result #f))])))
+(define/match (-and . args)
+  ;; specialize for trivial <=2 arg cases
+  [((list)) -tt]
+  [((list p)) p]
+  [((list p p)) p]
+  [((list (TrueProp:) p)) p]
+  [((list p (TrueProp:))) p]
+  [((list (FalseProp:) p)) -ff]
+  [((list p (FalseProp:))) -ff]
+  [(args)
+   (define mk
+     (match-lambda [(list) -tt]
+                   [(list p) p]
+                   [ps (make-AndProp ps)]))
+   ;; we remove duplicates and organize the props so that the
+   ;; strongest ones come first (note: this includes considering
+   ;; smaller ors before larger ors)
+   (define (flatten-ands/remove-duplicates/order ps)
+     (define ts '())
+     (define nts '())
+     (define ors (make-hash))
+     (define others '())
+     (let partition! ([ps ps])
+       (for ([p (in-list ps)])
+         (match p
+           [(? TypeProp?) (set! ts (cons p ts))]
+           [(? NotTypeProp?) (set! nts (cons p nts))]
+           [(OrProp: ps*) (hash-update! ors (length ps*) (λ (l) (cons p l)) '())]
+           [(AndProp: ps*) (partition! ps*)]
+           [_ (set! others (cons p others))])))
+     (define ors-smallest-to-largest
+       (append-map cdr (sort (hash->list ors)
+                             (λ (len/ors1 len/ors2)
+                               (< (car len/ors1) (car len/ors2))))))
+     (remove-duplicates (append ts nts others ors-smallest-to-largest) eq?))
+   (let loop ([ps (flatten-ands/remove-duplicates/order args)]
+              [result null])
+     (match ps
+       [(cons cur rst)
+        (cond
+          ;; trivial cases
+          [(FalseProp? cur) -ff]
+          [(TrueProp? cur) (loop rst result)]
+          ;; is there a contradition e.g. (ϕ ∧ ¬ϕ), if so abort
+          [(for/or ([p (in-list rst)])    (atomic-contradiction? p cur)) -ff]
+          [(for/or ([p (in-list result)]) (atomic-contradiction? p cur)) -ff]
+          ;; don't include 'cur' if its implied by another prop
+          ;; already in our result (this is why we order the props!)
+          [(for/or ([p (in-list result)]) (atomic-implies? p cur))
+           (loop rst result)]
+          ;; otherwise keep 'cur' in this conjunction
+          [else (loop rst (cons cur result))])]
+       [_ (mk (compact result #f))]))])
 
 ;; add-unconditional-prop: tc-results? Prop? -> tc-results?
 ;; 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 (add-unconditional-prop results prop)
-  (match results
-    [(tc-any-results: p) (tc-any-results (-and prop p))]
-    [(tc-results: ts (list (PropSet: ps+ ps-) ...) os)
-     (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)
-     (ret ts
-          (for/list ([p+ (in-list ps+)] [p- (in-list ps-)])
-            (-PS (-and prop p+) (-and prop p-)))
-          os
-          dty
-          dbound)]))
+(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)])
 
 
 ;; 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 (add-unconditional-prop-all-args arr type)
-  (match arr
-    [(Function: (list (arr: dom rng rest drest kws)))
-     (match rng
-       [(Values: (list (Result: tp (PropSet: -true-prop -false-prop) 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))))])]))
+(define/match (add-unconditional-prop-all-args arr type)
+  [((Function: (list (arr: dom rng rest drest kws))) type)
+   (match rng
+     [(Values: (list (Result: tp (PropSet: -true-prop -false-prop) 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))))])])
 
 ;; tc-results/c -> tc-results/c
-(define (erase-props tc)
-  (match 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)]))
+(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)])
diff --git a/typed-racket-lib/typed-racket/types/subtract.rkt b/typed-racket-lib/typed-racket/types/subtract.rkt
index ca0021c6..bc9f7de4 100644
--- a/typed-racket-lib/typed-racket/types/subtract.rkt
+++ b/typed-racket-lib/typed-racket/types/subtract.rkt
@@ -12,14 +12,14 @@
 ;; Type Type -> Type
 ;; conservatively calculates set subtraction
 ;; between the types (i.e. t - s)
-(define (subtract t s #:obj [obj -empty-obj])
+(define (subtract t s [obj -empty-obj])
   (define s-mask (mask s))
   (define result
     (let recurse ([t t] [obj obj])
       (define (sub t [obj -empty-obj]) (recurse t obj))
       (match t
         [_ #:when (disjoint-masks? (mask t) s-mask) t]
-        [_ #:when (subtype t s #:obj obj) -Bottom]
+        [_ #:when (subtype t s obj) -Bottom]
         [(or (App: _ _) (? Name?))
          ;; must be different, since they're not subtypes
          ;; and n must refer to a distinct struct type
@@ -43,5 +43,5 @@
         [(Poly: vs b) (make-Poly vs (sub b) obj)]
         [_ t])))
   (cond
-    [(subtype t result #:obj obj) t]
+    [(subtype t result obj) t]
     [else result]))
diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt
index 5ed91181..495864ca 100644
--- a/typed-racket-lib/typed-racket/types/subtype.rkt
+++ b/typed-racket-lib/typed-racket/types/subtype.rkt
@@ -26,7 +26,7 @@
 (provide NameStruct:)
 
 (provide/cond-contract
- [subtype (->* (Type? Type?) (#:obj OptObject?) boolean?)]
+ [subtype (->* (Type? Type?) ((or/c #f OptObject?)) boolean?)]
  [subresult (-> Result? Result? boolean?)]
  [subval (-> SomeValues? SomeValues? boolean?)]
  [type-equiv? (-> Type? Type? boolean?)]
@@ -49,15 +49,8 @@
 
 ;; is t1 a subtype of t2?
 ;; type type -> boolean
-(define (subtype t1 t2 #:obj [obj #f])
-  (and
-   (cond
-     [obj (subtype* (seen) t1 t2 obj)]
-     [else
-      (define-values (o os) (obj-seq-next (temp-objs)))
-      (parameterize ([temp-objs os])
-        (subtype* (seen) t1 t2 o))])
-   #t))
+(define (subtype t1 t2 [obj #f])
+  (and (subtype* (seen) t1 t2 obj) #t))
 
 
 ;; is v1 a subval of v2?
@@ -380,6 +373,11 @@
                (subtype* t1 t2)
                (subtype* t2 t1)))
 
+(define-syntax-rule (with-fresh-obj obj . body)
+  (let-values ([(obj os) (obj-seq-next (temp-objs))])
+    (parameterize ([temp-objs os])
+      . body)))
+
 ;; the algorithm for recursive types transcribed directly from TAPL, pg 305
 ;; List[(cons Number Number)] type type -> List[(cons Number Number)] or #f
 ;; is s a subtype of t, taking into account previously seen pairs A
@@ -388,73 +386,63 @@
 ;; types as they are encountered:
 ;; needs-resolved? types (Mus, Names, Apps),
 ;; Instances, and Structs (Prefabs?)
-(define subtype*
-  (case-lambda
-    [(A t1 t2)
-     (define-values (o os) (obj-seq-next (temp-objs)))
-     (parameterize ([temp-objs os])
-       (subtype* A t1 t2 o))]
-    [(A t1 t2 obj)
-     (cond
-       [(Univ? t2) A]
-       [(Bottom? t1) A]
-       ;; error is top and bot
-       [(or (Error? t1) (Error? t2)) A]
-       [(disjoint-masks? (mask t1) (mask t2)) #f]
-       [(equal? t1 t2) A]
-       [(seen? t1 t2 A) A]
-       [else
-        ;; first we check on a few t2 cases
-        ;; that need to come early during checking
-        (match t2
-          [(Intersection: t2s raw-prop)
-           (let ([A (for/fold ([A A])
-                              ([t2 (in-list t2s)]
-                               #:break (not A))
-                      (subtype* A t1 t2 obj))])
-             (and A
-                  (or (TrueProp? raw-prop)
-                      (let* ([obj (if (Empty? obj) (-id-path (genid)) obj)]
-                             [prop (instantiate-rep/obj raw-prop obj t1)])
-                        (implies-in-env? (lexical-env)
-                                         (-is-type obj t1)
-                                         prop)))
-                  A))]
-          [(? resolvable?)
-           (let ([A (remember t1 t2 A)])
-             (with-updated-seen A
-               (let ([t2 (resolve-once t2)])
-                 ;; check needed for if a name that hasn't been resolved yet
-                 (and (Type? t2) (subtype* A t1 t2 obj)))))]
-          [_
-           ;; otherwise we case on t1
-           (subtype-cases
-            A t1 t2 obj
-            ;; if we're still not certain after the switch,
-            ;; check the cases that need to come at the end
-            (λ (A t1 t2 obj)
-              (match* (t1 t2)
-                [(t1 (Union/set: base2 ts2 elems2))
-                 (cond
-                   [(hash-has-key? elems2 t1) A]
-                   [(subtype* A t1 base2 obj)]
-                   [else (for/or ([elem2 (in-list ts2)])
-                           (subtype* A t1 elem2 obj))])]
-                [(_ (Instance: (? resolvable? t2*)))
-                 (let ([A (remember t1 t2 A)])
-                   (with-updated-seen A
-                     (let ([t2* (resolve-once t2*)])
-                       (and (Type? t2*)
-                            (subtype* A t1 (make-Instance t2*) obj)))))]
-                [(_ (Poly: vs2 b2))
-                 #:when (null? (fv b2))
-                 (subtype* A t1 b2 obj)]
-                [(_ (PolyDots: vs2 b2))
-                 #:when (and (null? (fv b2))
-                             (null? (fi b2)))
-                 (subtype* A t1 b2 obj)]
-                [(_ _) #f])))])])]))
+(define (subtype* A t1 t2 [obj #f])
+  (cond
+    [(Univ? t2) A]
+    [(Bottom? t1) A]
+    ;; error is top and bot
+    [(or (Error? t1) (Error? t2)) A]
+    [(disjoint-masks? (mask t1) (mask t2)) #f]
+    [(equal? t1 t2) A]
+    [(seen? t1 t2 A) A]
+    [else
+     ;; first we check on a few t2 cases
+     ;; that need to come early during checking
+     (match t2
+       [(Intersection: t2s raw-prop)
+        (let ([A (for/fold ([A A])
+                           ([t2 (in-list t2s)]
+                            #:break (not A))
+                   (subtype* A t1 t2 obj))])
+          (and A
+               (or (TrueProp? raw-prop)
+                   (let* ([obj (if (Object? obj) obj (-id-path (genid)))]
+                          [prop (instantiate-rep/obj raw-prop obj t1)])
+                     (implies-in-env? (lexical-env)
+                                      (-is-type obj t1)
+                                      prop)))
+               A))]
+       [(? resolvable?)
+        (let ([A (remember t1 t2 A)])
+          (with-updated-seen A
+            (let ([t2 (resolve-once t2)])
+              ;; check needed for if a name that hasn't been resolved yet
+              (and (Type? t2) (subtype* A t1 t2 obj)))))]
+       [_ ;; otherwise we case on t1
+        (subtype-cases A t1 t2 obj)])]))
 
+(define (continue<: A t1 t2 obj)
+  (match* (t1 t2)
+    [(t1 (Union/set: base2 ts2 elems2))
+     (cond
+       [(hash-has-key? elems2 t1) A]
+       [(subtype* A t1 base2 obj)]
+       [else (for/or ([elem2 (in-list ts2)])
+               (subtype* A t1 elem2 obj))])]
+    [(_ (Instance: (? resolvable? t2*)))
+     (let ([A (remember t1 t2 A)])
+       (with-updated-seen A
+         (let ([t2* (resolve-once t2*)])
+           (and (Type? t2*)
+                (subtype* A t1 (make-Instance t2*) obj)))))]
+    [(_ (Poly: vs2 b2))
+     #:when (null? (fv b2))
+     (subtype* A t1 b2 obj)]
+    [(_ (PolyDots: vs2 b2))
+     #:when (and (null? (fv b2))
+                 (null? (fi b2)))
+     (subtype* A t1 b2 obj)]
+    [(_ _) #f]))
 
 ;; these data structures are allocated once and
 ;; used below in 'subtype-switch'
@@ -489,7 +477,7 @@
    (cons portable-fixnum? -NonNegFixnum)
    (cons values -Nat)))
 
-(define-rep-switch (subtype-cases A (#:switch t1) t2 obj continue)
+(define-rep-switch (subtype-cases A (#:switch t1) t2 obj)
   ;; NOTE: keep these in alphabetical order
   ;; or ease of finding cases
   [(case: App _)
@@ -503,7 +491,7 @@
      [(? Async-ChannelTop?) A]
      [(Async-Channel: elem2) (type≡? A elem1 elem2)]
      [(Evt: evt-t) (subtype* A elem1 evt-t)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Base (Base-bits: num? bits))
    (match t2
      [(BaseUnion: bbits nbits)
@@ -535,7 +523,7 @@
         [(Base:Log-Receiver? t1)
          (subtype* A log-vect-type evt-t)]
         [else #f])]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: BaseUnion (BaseUnion: bbits1 nbits1))
    (match t2
      [(? Base?) #f]
@@ -555,13 +543,13 @@
    (match t2
      [(? BoxTop?) A]
      [(Box: elem2) (type≡? A elem1 elem2)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Channel (Channel: elem1))
    (match t2
      [(? ChannelTop?) A]
      [(Channel: elem2) (type≡? A elem1 elem2)]
      [(Evt: evt-t) (subtype* A elem1 evt-t)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Class (Class: row inits fields methods augments init-rest))
    (match t2
      [(? ClassTop?) A]
@@ -601,13 +589,13 @@
                     (sub init-rest init-rest*))
                (and (not init-rest) (not init-rest*)
                     A)))]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Continuation-Mark-Keyof (Continuation-Mark-Keyof: val1))
    (match t2
      [(? Continuation-Mark-KeyTop?) A]
      [(Continuation-Mark-Keyof: val2)
       (type≡? A val1 val2)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: CustodianBox (CustodianBox: elem1))
    (match t2
      [(CustodianBox: elem2) (subtype* A elem1 elem2)]
@@ -615,7 +603,7 @@
       ;; Note that it's the whole box type that's being
       ;; compared against evt-t here
       (subtype* A t1 evt-t)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Distinction (Distinction: nm1 id1 t1*))
    (match t2
      [(app resolve (Distinction: nm2 id2 t2*))
@@ -623,20 +611,20 @@
       (subtype* A t1* t2*)]
      [_ (cond
           [(subtype* A t1* t2 obj)]
-          [else (continue A t1 t2 obj)])])]
+          [else (continue<: A t1 t2 obj)])])]
   [(case: Ephemeron (Ephemeron: elem1))
    (match t2
      [(Ephemeron: elem2) (subtype* A elem1 elem2)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Evt (Evt: result1))
    (match t2
      [(Evt: result2) (subtype* A result1 result2)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: F (F: var1))
    (match t2
      ;; tvars are equal if they are the same variable
      [(F: var2) (eq? var1 var2)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Function (Function: arrs1))
    (match t2
      ;; special-case for case-lambda/union with only one argument              
@@ -656,11 +644,11 @@
               [(supertype-of-one/arr A (car arrs2) arrs1)
                => (λ (A) (loop-arities A (cdr arrs2)))]
               [else #f])))]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Future (Future: elem1))
    (match t2
      [(Future: elem2) (subtype* A elem1 elem2)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Hashtable (Hashtable: key1 val1))
    (match t2
      [(? HashtableTop?) A]
@@ -671,7 +659,7 @@
       (subtype-seq A
                    (subtype* key1 key2)
                    (subtype* val1 val2))]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: HeterogeneousVector (HeterogeneousVector: elems1))
    (match t2
      [(VectorTop:) A]
@@ -693,7 +681,7 @@
                 ([elem1 (in-list elems1)]
                  #:break (not A))
         (subtype* A elem1 seq-t))]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Instance (Instance: inst-t1))
    (cond
      [(resolvable? inst-t1)
@@ -723,7 +711,7 @@
          (and ;; Note that init & augment clauses don't matter for objects
           (subtype-clause? method-map method-map*)
           (subtype-clause? field-map field-map*))]
-        [(_ _) (continue A t1 t2 obj)])])]
+        [(_ _) (continue<: A t1 t2 obj)])])]
   [(case: Intersection (Intersection: t1s _))
    (match t1
      [(Refine: t1* raw-prop)
@@ -736,17 +724,16 @@
            [else (with-lexical-env env
                    (subtype* A t1* t2 obj))])]
         [else
-         (define id (genid))
-         (define obj (-id-path id))
-         (define prop (instantiate-rep/obj raw-prop obj t1*))
-         ;; 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))])]
+         (with-fresh-obj obj
+           (define prop (instantiate-rep/obj raw-prop obj t1*))
+           ;; 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)))])]
      [_
       (cond
         [(for/or ([t1 (in-list t1s)])
            (subtype* A t1 t2 obj))]
-        [else (continue A t1 t2 obj)])])]
+        [else (continue<: A t1 t2 obj)])])]
   [(case: ListDots (ListDots: dty1 dbound1))
    (match t2
      ;; recur structurally on dotted lists, assuming same bounds
@@ -760,7 +747,7 @@
      ;; variance issues.
      [(Listof: elem2)
       (subtype* A (-poly (dbound1) dty1) elem2)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: MPair (MPair: t11 t12))
    (match t2
      [(? MPairTop?) A]
@@ -775,7 +762,7 @@
                    (subtype* t11 seq-t)
                    (subtype* t12 null-or-mpair-top)
                    (subtype* t12 (make-Sequence (list seq-t))))]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Mu _)
    (let ([A (remember t1 t2 A)])
      (with-updated-seen A
@@ -805,21 +792,21 @@
       (subtype-seq A
                    (subtype* t11 seq-t)
                    (subtype* t12 (-lst seq-t)))]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Param (Param: in1 out1))
    (match t2
      [(Param: in2 out2) (subtype-seq A
                                      (subtype* in2 in1)
                                      (subtype* out1 out2))]
      [_ (subtype* A (cl->* (t-> out1) (t-> in1 -Void)) t2)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Poly (Poly: names b1))
    (match t2
      [(? Poly?) #:when (= (length names) (Poly-n t2))
                 (subtype* A b1 (Poly-body names t2))]
      ;; use local inference to see if we can use the polytype here
      [_ #:when (infer names null (list b1) (list t2) Univ) A]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: PolyDots (PolyDots: (list ns ... n-dotted) b1))
    (match t2
      [(PolyDots: (list ms ... m-dotted) b2)
@@ -847,7 +834,7 @@
       (subtype* A (subst-all subst b1) b2)]
      [_ #:when (infer ns (list n-dotted) (list b1) (list t2) Univ)
         A]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Prefab (Prefab: k1 ss))
    (match t2
      [(Prefab: k2 ts)
@@ -866,11 +853,11 @@
                                             (subtype* t s)
                                             (subtype* s t))
                                (subtype* A s t))))))))]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Promise (Promise: elem1))
    (match t2
      [(Promise: elem2) (subtype* A elem1 elem2)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Prompt-Tagof (Prompt-Tagof: body1 handler1))
    (match t2
      [(? Prompt-TagTop?) A]
@@ -878,7 +865,7 @@
       (subtype-seq A
                    (type≡? body1 body2)
                    (type≡? handler1 handler2))]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Refinement (Refinement: t1-parent id1))
    (match t2
      [(Refinement: t2-parent id2)
@@ -886,17 +873,17 @@
       (subtype* A t1-parent t2-parent)]
      [_ (cond
           [(subtype* A t1-parent t2)]
-          [else (continue A t1 t2 obj)])])]
+          [else (continue<: A t1 t2 obj)])])]
   ;; sequences are covariant
   [(case: Sequence (Sequence: ts1))
    (match t2
      [(Sequence: ts2) (subtypes* A ts1 ts2)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Set (Set: elem1))
    (match t2
      [(Set: elem2) (subtype* A elem1 elem2)]
      [(Sequence: (list seq-t)) (subtype* A elem1 seq-t)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Struct (Struct: nm1 parent1 flds1 proc1 _ _))
    (match t2
      ;; Avoid resolving things that refer to different structs.
@@ -934,21 +921,21 @@
                 (let ([A (remember t1 t2 A)])
                   (with-updated-seen A
                     (subtype* A parent1 t2))))]
-          [else (continue A t1 t2 obj)])]
-     [_ (continue A t1 t2 obj)])]
+          [else (continue<: A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: StructType (StructType: t1*))
    (match t2
      [(StructTypeTop:) A]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Syntax (Syntax: elem1))
    (match t2
      [(Syntax: elem2) (subtype* A elem1 elem2)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: ThreadCell (ThreadCell: elem1))
    (match t2
      [(? ThreadCellTop?) A]
      [(ThreadCell: elem2) (type≡? A elem1 elem2)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Union (Union/set: base1 ts1 elems1))
    (let ([A (subtype* A base1 t2 obj)])
      (and A
@@ -977,7 +964,7 @@
            (check-sub-signatures? exports1 exports2)
            (check-sub-signatures? init-depends2 init-depends1)
            (subval* A t1* t2*))]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Value (Value: val1))
    (match t2
      [(Base-predicate: pred) (and (pred val1) A)]
@@ -1006,16 +993,16 @@
                                           (-is-type obj t1)
                                           (instantiate-rep/obj p* obj t1)))))
       A]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Vector (Vector: elem1))
    (match t2
      [(? VectorTop?) A]
      [(Vector: elem2) (type≡? A elem1 elem2)]
      [(Sequence: (list seq-t)) (subtype* A elem1 seq-t)]
-     [_ (continue A t1 t2 obj)])]
+     [_ (continue<: A t1 t2 obj)])]
   [(case: Weak-Box (Weak-Box: elem1))
    (match t2
      [(? Weak-BoxTop?) A]
      [(Weak-Box: elem2) (type≡? A elem1 elem2)]
-     [_ (continue A t1 t2 obj)])]
-  [else: (continue A t1 t2 obj)])
+     [_ (continue<: A t1 t2 obj)])]
+  [else: (continue<: A t1 t2 obj)])
diff --git a/typed-racket-lib/typed-racket/utils/utils.rkt b/typed-racket-lib/typed-racket/utils/utils.rkt
index f7ee5e1f..aa9b40a6 100644
--- a/typed-racket-lib/typed-racket/utils/utils.rkt
+++ b/typed-racket-lib/typed-racket/utils/utils.rkt
@@ -27,7 +27,8 @@ at least theoretically.
  filter-multiple
  syntax-length
  in-pair
- in-sequence-forever
+ in-list/rest
+ list-ref/default
  match*/no-order
  bind
  genid
@@ -257,17 +258,6 @@ at least theoretically.
   (let ((list (syntax->list stx)))
     (and list (length list))))
 
-(define (in-sequence-forever seq val)
-  (make-do-sequence
-   (λ ()
-     (let-values ([(more? gen) (sequence-generate seq)])
-       (values (λ (e) (if (more?) (gen) val))
-               (λ (_) #t)
-               #t
-               (λ (_) #t)
-               (λ _ #t)
-               (λ _ #t))))))
-
 (define-syntax (match*/no-order stx)
   (define (parse-clauses clauses)
     (syntax-parse clauses
@@ -344,3 +334,75 @@ at least theoretically.
               (syntax-source-module id)))))
 
 (require 'local-ids)
+
+
+;; in-list/rest
+;; (in-list/rest l v)
+;;
+;; iterates through the elements of the
+;; list 'l' until they are exhausted, at which
+;; point 'v' is used for each subsequent iteration
+
+(define (in-list/rest-proc l rest)
+  (in-sequences l (in-cycle (in-value rest))))
+
+(define-sequence-syntax in-list/rest
+  (λ () #'in-list/rest-proc)
+  (λ (stx)
+    (syntax-case stx ()
+      [[(val) (_ list-exp rest-exp)]
+       #'[(val)
+          (:do-in
+           ;; ([(outer-id ...) outer-expr] ...)
+           ([(list) list-exp]
+            [(rest) rest-exp])
+           ;; outer-check
+           #t
+           ;; ([loop-id loop-expr] ...)
+           ([pos list])
+           ;; pos-guard
+           #t
+           ;; ([(inner-id ...) inner-expr] ...)
+           ([(val pos) (if (pair? pos)
+                           (values (car pos) (cdr pos))
+                           (values rest '()))])
+           ;; pre-guard
+           #t
+           ;; post-guard
+           #t
+           ;; (loop-arg ...)
+           (pos))]]
+      [[xs (_ dd-exp)]
+       (list? (syntax->datum #'xs))
+       (raise-syntax-error 'in-list/rest
+                           (format "expected an identifier, given ~a"
+                                   (syntax->list #'xs))
+                           #'xs)]
+      [blah (raise-syntax-error 'in-list/rest "invalid usage" #'blah)])))
+
+;; quick in-list/rest sanity checks
+(module+ test
+  (unless (equal? (for/list ([_ (in-range 0)]
+                             [val (in-list/rest (list 1 2) #f)])
+                    val)
+                  (list))
+    (error 'in-list/rest "broken!"))
+  (unless (equal? (for/list ([_ (in-range 2)]
+                             [val (in-list/rest (list 1 2) #f)])
+                    val)
+                  (list 1 2))
+    (error 'in-list/rest "broken!"))
+  (unless (equal? (for/list ([_ (in-range 4)]
+                             [val (in-list/rest (list 1 2) #f)])
+                    val)
+                  (list 1 2 #f #f))
+    (error 'in-list/rest "broken!")))
+
+
+(define (list-ref/default xs idx default)
+  (match xs
+    ['() default]
+    [(cons x xs)
+     (if (eqv? 0 idx)
+         x
+         (list-ref/default xs (sub1 idx) default))]))
\ No newline at end of file
diff --git a/typed-racket-test/succeed/with-integer-linear-arith2.rkt b/typed-racket-test/succeed/with-integer-linear-arith2.rkt
new file mode 100644
index 00000000..7cde21bf
--- /dev/null
+++ b/typed-racket-test/succeed/with-integer-linear-arith2.rkt
@@ -0,0 +1,105 @@
+#lang typed/racket
+#:with-linear-integer-arithmetic
+
+
+(define-type (V8 A) (Refine [v : (Vectorof A)] (= 8 (vector-length v))))
+(define-type Nat<8 (Refine [i : Natural] (< i 8)))
+(: v8ref (-> (V8 Any) Nat<8 Any))
+(define (v8ref v i)
+  (vector-ref v i))
+
+(: poly-v8ref (All (A) (-> (V8 A) Nat<8 A)))
+(define (poly-v8ref v i)
+  (vector-ref v i))
+
+
+(ann (vector 0 1 2 3 4 5 6 7) (V8 Any))
+(ann (vector 0 1 2 3 4 5 6 7) (V8 Byte))
+(ann '#(0 1 2 3 4 5 6 7) (V8 Any))
+(ann '#(0 1 2 3 4 5 6 7) (V8 Byte))
+ 
+;;(v8ref (vector 0 1 2 3 4 5 6) 4) ;; should fail
+(v8ref (vector 0 1 2 3 4 5 6 7) 4)
+(poly-v8ref (vector 0 1 2 3 4 5 6 7) 4)
+;(v8ref (vector 0 1 2 3 4 5 6 7) 9) ;; should fail
+;(v8ref (vector 0 1 2 3 4 5 6 7 8) 4) ;; should fail
+;(poly-v8ref (vector 0 1 2 3 4 5 6 7) 9) ;; should fail
+
+(define v0 : (V8 Any) (vector 0 1 2 3 4 5 6 7))
+(define v1 : (Vectorof Any) (vector 0 1 2 3 4 5 6 7))
+
+
+(if (= 8 (vector-length v0))
+    (v8ref v0 3)
+    (ann "hello" Number))
+
+;; TODO
+;; this doesn't work right now because aliasing
+;; vector-length makes the type un-updatable (i.e. silly
+;; implementation bug that needs a minor refactoring of
+;; our object representations)
+;; (define (byte->byte [b : Byte]) b)
+;;(let ([len (vector-length v0)])
+;;    (when (byte? len)
+;;      (byte->byte len)))
+
+
+(when (and (<= 8 (vector-length v1))
+           (<= (vector-length v1) 8))
+  (v8ref v1 3)) 
+
+(define zero 0)
+(define one 1)
+(define two 2)
+(define three 3)
+
+;; cute syntax that forces an integer equality/inequality/etc
+;; else typechecking will fail -- also the type check
+;; error highlights the test case
+(define-syntax (assert= stx)
+  (syntax-case stx ()
+    [(_ expr1 expr2)
+     #`(unless (= expr1 expr2)
+         #,(quasisyntax/loc stx
+             (add1 #,(syntax/loc stx "undead = code"))))]))
+
+(define-syntax (assert< stx)
+  (syntax-case stx ()
+    [(_ expr1 expr2)
+     #`(unless (< expr1 expr2)
+         #,(quasisyntax/loc stx
+             (add1 #,(syntax/loc stx "undead < code"))))]))
+
+(define-syntax (assert<= stx)
+  (syntax-case stx ()
+    [(_ expr1 expr2)
+     #`(unless (<= expr1 expr2)
+         #,(quasisyntax/loc stx
+             (add1 #,(syntax/loc stx "undead <= code"))))]))
+
+(assert= (- three zero) three)
+(assert= (- 3 zero) three)
+(assert= (- three 0) three)
+(assert= (- three zero) 3)
+(assert= (- three two) one)
+(assert= (+ one two) three)
+(assert= (+ one two) three)
+(assert= (- (+ one two) one) two)
+(assert= (* 2 2 (+ one two)) 12)
+(assert= (add1 one) two)
+(assert= (sub1 one) 0)
+
+;; would be nice if this worked... I think it doesn't currently
+;; because the (min...) expression has a specific type, but
+;; no object, and so we learn (<= empty-obj two) =(
+;; solutions:
+;; 1 - existential results a la the paper
+;; 2 - check for contradictions before erasing
+;;     the empty object? (this is sort of what
+;;     we do anyway right now but we dont' do it
+;;     enough to see this contradiction? maybe this is
+;;     a subtyping limitation...)
+;(assert<= (min one two three) two)  
+
+
+