diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index 013e945526..a150d1d5c7 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -440,66 +440,9 @@
                         (cgen/filter-set V X Y f-s f-t)
                         (cgen/object V X Y o-s o-t))]
 
-          ;; values are covariant
-          [((Values: ss) (Values: ts))
-           #:return-unless (= (length ss) (length ts))
-           #f
-           (cgen/list V X Y ss ts)]
-
-          ;; this constrains `dbound' to be |ts| - |ss|
-          [((ValuesDots: ss s-dty dbound) (Values: ts))
-           #:return-unless (>= (length ts) (length ss)) #f
-           #:return-unless (memq dbound Y) #f
-
-           (let* ([vars     (var-store-take dbound s-dty (- (length ts) (length ss)))]
-                  ;; new-tys are dummy plain type variables,
-                  ;; standing in for the elements of dbound that need to be generated
-                  [new-tys  (for/list ([var (in-list vars)])
-                              ;; must be a Result since we are matching these against
-                              ;; the contents of the `Values`, which are Results
-                              (-result (substitute (make-F var) dbound s-dty)))]
-                  ;; generate constraints on the prefixes, and on the dummy types
-                  [new-cset (cgen/list V (append vars X) Y (append ss new-tys) ts)])
-             ;; now take all the dummy types, and use them to constrain dbound appropriately
-             (% move-vars-to-dmap new-cset dbound vars))]
-
-          ;; like the case above, but constrains `dbound' to be |ss| - |ts|
-          [((Values: ss) (ValuesDots: ts t-dty dbound))
-           #:return-unless (>= (length ss) (length ts)) #f
-           #:return-unless (memq dbound Y) #f
-
-           ;; see comments for last case, this case swaps `s` and `t` order
-           (let* ([vars     (var-store-take dbound t-dty (- (length ss) (length ts)))]
-                  [new-tys  (for/list ([var (in-list vars)])
-                              (-result (substitute (make-F var) dbound t-dty)))]
-                  [new-cset (cgen/list V (append vars X) Y ss (append ts new-tys))])
-             (% move-vars-to-dmap new-cset dbound vars))]
-
-          ;; identical bounds - just unify pairwise
-          [((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound))
-           #:return-when (memq dbound Y) #f
-           (cgen/list V X Y (cons s-dty ss) (cons t-dty ts))]
-          [((ValuesDots: ss s-dty (? (λ (db) (memq db Y)) s-dbound))
-            (ValuesDots: ts t-dty t-dbound))
-           ;; What should we do if both are in Y?
-           #:return-when (memq t-dbound Y) #f
-           (% cset-meet
-              (cgen/list V X Y ss ts)
-              (extend-tvars (list t-dbound)
-                (% move-dotted-rest-to-dmap (cgen V (cons s-dbound X) Y s-dty t-dty) s-dbound t-dbound)))]
-          [((ValuesDots: ss s-dty s-dbound)
-            (ValuesDots: ts t-dty (? (λ (db) (memq db Y)) t-dbound)))
-           ;; s-dbound can't be in Y, due to previous rule
-           (% cset-meet
-              (cgen/list V X Y ss ts)
-              (extend-tvars (list s-dbound)
-                (% move-dotted-rest-to-dmap (cgen V (cons t-dbound X) Y s-dty t-dty) t-dbound s-dbound)))]
-
           ;; Values just delegate to cgen/seq
-          ;; This is currently buggy because cgen/seq assumes types and not results
-
-          ;; [((ValuesSeq: s-seq) (ValuesSeq: t-seq))
-          ;; (cgen/seq V X Y s-seq t-seq)]
+          [((ValuesSeq: s-seq) (ValuesSeq: t-seq))
+           (cgen/seq V X Y s-seq t-seq)]
 
           ;; they're subtypes. easy.
           [(a b) 
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/substitute.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/substitute.rkt
index f466b0961f..7ab1503457 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/substitute.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/substitute.rkt
@@ -39,8 +39,7 @@
 
 ;; substitute-many : Hash[Name,Type] Type -> Type
 (define/cond-contract (substitute-many subst target #:Un [Un (lambda (args) (apply Un args))])
-  ((simple-substitution/c (or/c SomeValues/c Values/c arr?)) (#:Un procedure?)
-   . ->* .  (or/c SomeValues/c Values/c arr?))
+  ((simple-substitution/c Type?) (#:Un procedure?) . ->* .  Type?)
   (define (sb t) (substitute-many subst t #:Un Un))
   (define names (hash-keys subst))
   (define fvs (free-vars* target))
@@ -83,14 +82,13 @@
 
 ;; substitute : Type Name Type -> Type
 (define/cond-contract (substitute image name target #:Un [Un (lambda (args) (apply Un args))])
-  ((Type/c symbol? Type/c) (#:Un procedure?) . ->* . Type/c)
+  ((Type/c symbol? Type?) (#:Un procedure?) . ->* . Type?)
   (substitute-many (hash name image) target #:Un Un))
 
 ;; implements angle bracket substitution from the formalism
 ;; substitute-dots : Listof[Type] Option[type] Name Type -> Type
 (define/cond-contract (substitute-dots images rimage name target)
-  ((listof Type/c) (or/c #f Type/c) symbol? (or/c arr? SomeValues/c Values/c)
-   . -> . (or/c arr?  SomeValues/c Values/c))
+  ((listof Type/c) (or/c #f Type/c) symbol? Type?  . -> . Type?)
   (define (sb t) (substitute-dots images rimage name t))
   (if (or (set-member? (free-vars-names (free-idxs* target)) name)
           (set-member? (free-vars-names (free-vars* target)) name))
@@ -172,7 +170,7 @@
 ;; substitute many variables
 ;; subst-all : substitution/c Type -> Type
 (define/cond-contract (subst-all s ty)
-  (substitution/c (or/c arr? Values/c SomeValues/c) . -> . (or/c arr? Values/c SomeValues/c))
+  (substitution/c Type? . -> . Type?)
 
   (define t-substs
     (for/fold ([acc (hash)]) ([(v r) (in-hash s)])
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/utils.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/utils.rkt
index 36a6a8b04e..134f59d380 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/utils.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/utils.rkt
@@ -20,7 +20,7 @@ at least theoretically.
  rep utils typecheck infer env private types static-contracts)
 
 (define optimize? (make-parameter #t))
-(define-for-syntax enable-contracts? (and (getenv "PLT_TR_CONTRACTS") #t))
+(define-for-syntax enable-contracts? (or (getenv "PLT_TR_CONTRACTS") #t))
 
 (define-syntax do-contract-req
   (if enable-contracts?