diff --git a/collects/tests/typed-scheme/fail/require-typed-missing.rkt b/collects/tests/typed-scheme/fail/require-typed-missing.rkt
new file mode 100644
index 00000000..66c8b4e0
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/require-typed-missing.rkt
@@ -0,0 +1,16 @@
+#;
+(exn-pred "at least one")
+#lang typed/racket
+
+
+(require/typed  (make-main (([Listof Node] [Listof Edge] -> Graph)
+                           (State Number Number MouseEvent -> State)
+                           (State KeyEvent -> State)
+                           (State -> Scene)
+                           (Any -> Boolean)
+                           (State -> Boolean)
+                           (Stop -> Graph)
+                           (Any -> Edge)
+                           (Edge -> Graph)
+                           ->
+                           (Boolean -> Graph))))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/fixnum.rkt b/collects/tests/typed-scheme/succeed/fixnum.rkt
index 27e50ba5..b345dd1b 100644
--- a/collects/tests/typed-scheme/succeed/fixnum.rkt
+++ b/collects/tests/typed-scheme/succeed/fixnum.rkt
@@ -10,7 +10,7 @@
 ;; really badly wrong.
 
 (: check (All (a) ((a a -> Boolean) a a -> Boolean)))
-;; Simple check function as RacUnit doesn't work in Typed Scheme (yet)
+;; Simple check function as RackUnit doesn't work in Typed Scheme (yet)
 (define (check f a b)
   (if (f a b)
       #t
diff --git a/collects/tests/typed-scheme/succeed/flonum.rkt b/collects/tests/typed-scheme/succeed/flonum.rkt
index 0c709e64..58139c71 100644
--- a/collects/tests/typed-scheme/succeed/flonum.rkt
+++ b/collects/tests/typed-scheme/succeed/flonum.rkt
@@ -5,7 +5,7 @@
  scheme/unsafe/ops)
 
 (: check (All (a) ((a a -> Boolean) a a -> Boolean)))
-;; Simple check function as RacUnit doesn't work in Typed Scheme (yet)
+;; Simple check function as RackUnit doesn't work in Typed Scheme (yet)
 (define (check f a b)
   (if (f a b)
       #t
diff --git a/collects/tests/typed-scheme/succeed/flvector.rkt b/collects/tests/typed-scheme/succeed/flvector.rkt
index 255776ed..4a359a43 100644
--- a/collects/tests/typed-scheme/succeed/flvector.rkt
+++ b/collects/tests/typed-scheme/succeed/flvector.rkt
@@ -11,7 +11,7 @@
 ;; really badly wrong.
 
 (: check (All (a) ((a a -> Boolean) a a -> Boolean)))
-;; Simple check function as RacUnit doesn't work in Typed Scheme (yet)
+;; Simple check function as RackUnit doesn't work in Typed Scheme (yet)
 (define (check f a b)
   (if (f a b)
       #t
diff --git a/collects/tests/typed-scheme/succeed/or-sym.rkt b/collects/tests/typed-scheme/succeed/or-sym.rkt
new file mode 100644
index 00000000..767af129
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/or-sym.rkt
@@ -0,0 +1,25 @@
+#lang typed/scheme
+
+#;#;
+(: g (Any -> Boolean : (U 'r 's)))
+(define (g x) 
+  (let ([q x])
+    (let ([op2 (eq? 'r x)])
+      (if op2 op2 (eq? 's x)))))
+
+
+(define: f? : (Any -> Boolean : (U 'q 'r 's))
+  (lambda (x)
+    (let ([op1 (eq? 'q x)])
+      (if op1 op1
+        (let ([op2 (eq? 'r x)])
+               (if op2 
+                   ;; !#f_op2
+                   op2
+                   (eq? 's x)))))))
+
+(define: f2? : (Any -> Boolean : (U 'q 'r 's))
+  (lambda (x)
+    (or (eq? 'q x)
+        (eq? 'r x)
+        (eq? 's x))))
diff --git a/collects/tests/typed-scheme/succeed/pr10470.rkt b/collects/tests/typed-scheme/succeed/pr10470.rkt
new file mode 100644
index 00000000..bfc21cc2
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/pr10470.rkt
@@ -0,0 +1,15 @@
+(module pr10470 typed-scheme
+
+  (define-type-alias (Memo alpha) (U (Option alpha) (-> (Option alpha))))
+
+  (define-struct: table ([val : (Memo Number)]) #:mutable)
+
+  (: f (table -> (Option Number)))
+  (define (f tab)
+    (let ([proc-or-num (table-val tab)])
+      (cond
+        [(procedure? proc-or-num)
+         (let ([result (proc-or-num)])
+           (set-table-val! tab result)
+           result)]
+        [else proc-or-num]))))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/unit-tests/parse-type-tests.rkt b/collects/tests/typed-scheme/unit-tests/parse-type-tests.rkt
index 7de981d3..b365336b 100644
--- a/collects/tests/typed-scheme/unit-tests/parse-type-tests.rkt
+++ b/collects/tests/typed-scheme/unit-tests/parse-type-tests.rkt
@@ -106,6 +106,8 @@
     (-polydots (a) ((list) [a a] . ->... . N))]
    
    [(Any -> Boolean : Number) (make-pred-ty -Number)]
+   [(Integer -> (All (X) (X -> X)))
+    (t:-> -Integer (-poly (x) (t:-> x x)))]
    
    ))
 
diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt b/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt
index 142385a5..f46fb27d 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt
@@ -611,7 +611,7 @@
            (do: : Number ((x : (Listof Number) x (cdr x))
                           (sum : Number 0 (+ sum (car x))))
                 ((null? x) sum)))
-         N]
+         #:ret (ret N (-FS -top -top) (make-NoObject))]
         
         [tc-e/t (if #f 1 'foo) (-val 'foo)]
         
@@ -794,6 +794,14 @@
         [tc-e (floor 1/2) -Integer]
         [tc-e (ceiling 1/2) -Integer]
         [tc-e (truncate 0.5) -Flonum]
+        [tc-e/t (ann (lambda (x) (lambda (x) x))
+                     (Integer -> (All (X) (X -> X))))
+                (t:-> -Integer (-poly (x) (t:-> x x)))]
+        [tc-e/t (lambda: ([x : Any])
+                         (or (eq? 'q x)
+                             (eq? 'r x)
+                             (eq? 's x)))
+                (make-pred-ty (t:Un (-val 'q) (-val 'r) (-val 's)))]
         )
   (test-suite
    "check-type tests"
diff --git a/collects/typed-scheme/private/base-env-numeric.rkt b/collects/typed-scheme/private/base-env-numeric.rkt
index c80d9ad6..61becebd 100644
--- a/collects/typed-scheme/private/base-env-numeric.rkt
+++ b/collects/typed-scheme/private/base-env-numeric.rkt
@@ -19,6 +19,8 @@
   (define-for-syntax binop 
     (lambda (t [r t])
       (t t . -> . r)))
+  (define-for-syntax rounder 
+    (cl->* (-> -ExactRational -Integer) (-> -Flonum -Flonum) (-> -Real -Real)))
   
   (define-for-syntax (unop t) (-> t t))
   
@@ -112,18 +114,10 @@
                  (-Real . -> . -ExactRational)
                  (N . -> . N))]
 
-[floor    (cl->*
-           (-> -ExactRational -Integer)
-           (-> -Flonum -Flonum)
-           (-> -Real -Real))]
-[ceiling  (cl->*
-           (-> -ExactRational -Integer)
-           (-> -Flonum -Flonum)
-           (-> -Real -Real))]
-[truncate (cl->*
-           (-> -ExactRational -Integer)
-           (-> -Flonum -Flonum)
-           (-> -Real -Real))]
+[floor rounder]
+[ceiling rounder]
+[truncate rounder]
+[round rounder]
 [make-rectangular (-Real -Real . -> . N)]
 [make-polar (-Real -Real . -> . N)]
 [real-part (N . -> . -Real)]
@@ -150,8 +144,6 @@
 [gcd  (null -Integer . ->* . -Integer)]
 [lcm  (null -Integer . ->* . -Integer)]
 
-[round (-Real . -> . -Real)]
-
 ;; scheme/math
 
 [sgn (-Real . -> . -Real)]
diff --git a/collects/typed-scheme/private/base-env.rkt b/collects/typed-scheme/private/base-env.rkt
index f3fe6081..db91883d 100644
--- a/collects/typed-scheme/private/base-env.rkt
+++ b/collects/typed-scheme/private/base-env.rkt
@@ -422,13 +422,19 @@
 
 [match:error ((list) Univ . ->* . (Un))]
 
-[arithmetic-shift (-Integer -Integer . -> . -Integer)]
-[bitwise-and (null -Integer . ->* . -Integer)]
-[bitwise-ior (null -Integer . ->* . -Integer)]
-[bitwise-not (null -Integer . ->* . -Integer)]
-[bitwise-xor (null -Integer . ->* . -Integer)]
+[arithmetic-shift (cl->* (-Nat -Nat . -> . -Nat)
+                         (-Integer -Integer . -> . -Integer))]
+[bitwise-and (cl->* (null -Nat . ->* . -Nat)
+                    (null -Integer . ->* . -Integer))]
+[bitwise-ior (cl->* (null -Nat . ->* . -Nat)
+                    (null -Integer . ->* . -Integer))]
+[bitwise-not (cl->* (null -Nat . ->* . -Nat)
+                    (null -Integer . ->* . -Integer))]
+[bitwise-xor (cl->* (null -Nat . ->* . -Nat)
+                    (null -Integer . ->* . -Integer))]
 
-[abs (-Real . -> . -Real)]
+[abs (cl->* (-Integer . -> . -Nat)
+            (-Real . -> . -Real))]
 
 [file-exists? (-Pathlike . -> . B)]
 [string->symbol (-String . -> . Sym)]
diff --git a/collects/typed-scheme/private/for-clauses.rkt b/collects/typed-scheme/private/for-clauses.rkt
new file mode 100644
index 00000000..57d65685
--- /dev/null
+++ b/collects/typed-scheme/private/for-clauses.rkt
@@ -0,0 +1,44 @@
+#lang racket/base
+
+(require syntax/parse
+         "annotate-classes.rkt"
+         (for-template racket/base))
+
+(provide convert-for-clauses)
+
+;; we need handle #:when clauses manually because we need to annotate
+;; the type of each nested for
+(define (convert-for-clauses name clauses body ty)
+  (let loop ((clauses clauses))
+    (define-splicing-syntax-class for-clause
+    ;; single-valued seq-expr
+    (pattern (var:annotated-name seq-expr:expr)
+             #:with expand #'(var.ann-name seq-expr))
+    ;; multi-valued seq-expr
+    (pattern ((v:annotated-name ...) seq-expr:expr)
+             #:with expand #'((v.ann-name ...) seq-expr)))
+    (syntax-parse clauses
+      [(head:for-clause next:for-clause ... #:when rest ...)
+       (syntax-property
+        (quasisyntax/loc clauses
+          (#,name
+           (head.expand next.expand ...)
+           #,(loop #'(#:when rest ...))))
+        'type-ascription
+        ty)]
+      [(head:for-clause ...) ; we reached the end
+       (syntax-property
+        (quasisyntax/loc clauses
+          (#,name
+           (head.expand ...)
+           #,@body))
+        'type-ascription
+        ty)]
+      [(#:when guard) ; we end on a #:when clause
+       (quasisyntax/loc clauses
+         (when guard
+           #,@body))]
+      [(#:when guard rest ...)
+       (quasisyntax/loc clauses
+         (when guard
+           #,(loop #'(rest ...))))])))
diff --git a/collects/typed-scheme/private/optimize.rkt b/collects/typed-scheme/private/optimize.rkt
index 5542553e..8e7358ea 100644
--- a/collects/typed-scheme/private/optimize.rkt
+++ b/collects/typed-scheme/private/optimize.rkt
@@ -1,6 +1,6 @@
 #lang scheme/base
 
-(require syntax/parse (for-template scheme/base scheme/unsafe/ops)
+(require syntax/parse (for-template scheme/base scheme/flonum scheme/unsafe/ops)
          "../utils/utils.rkt" unstable/match scheme/match unstable/syntax
          (rep type-rep)
          (types abbrev type-table utils))
@@ -13,14 +13,20 @@
            #:with opt #'e.opt))
 
 (define-syntax-class float-binary-op
-  #:literals (+ - * / = <= < > >= min max)
+  #:literals (+ - * / = <= < > >= min max
+              fl+ fl- fl* fl/ fl= fl<= fl< fl> fl>= flmin flmax)
   (pattern (~and i:id (~or + - * / = <= < > >= min max))
-           #:with unsafe (format-id #'here "unsafe-fl~a" #'i)))
+           #:with unsafe (format-id #'here "unsafe-fl~a" #'i))
+  (pattern (~and i:id (~or fl+ fl- fl* fl/ fl= fl<= fl< fl> fl>= flmin flmax))
+           #:with unsafe (format-id #'here "unsafe-~a" #'i)))
 
 (define-syntax-class float-unary-op
-  #:literals (abs sin cos tan asin acos atan log exp)
-  (pattern (~and i:id (~or abs sin cos tan asin acos atan log exp))
-           #:with unsafe (format-id #'here "unsafe-fl~a" #'i)))
+  #:literals (abs sin cos tan asin acos atan log exp sqrt round floor ceiling truncate
+              flabs flsin flcos fltan flasin flacos flatan fllog flexp flsqrt flround flfloor flceiling fltruncate)
+  (pattern (~and i:id (~or abs sin cos tan asin acos atan log exp sqrt round floor ceiling truncate))
+           #:with unsafe (format-id #'here "unsafe-fl~a" #'i))
+  (pattern (~and i:id (~or flabs flsin flcos fltan flasin flacos flatan fllog flexp flsqrt flround flfloor flceiling fltruncate))
+           #:with unsafe (format-id #'here "unsafe-~a" #'i)))
 
 (define-syntax-class pair-opt-expr
   (pattern e:opt-expr
@@ -60,11 +66,11 @@
            (begin (log-optimization "unary float" #'op)
                   #'(op.unsafe f.opt)))
   ;; unlike their safe counterparts, unsafe binary operators can only take 2 arguments
-  (pattern (#%plain-app op:float-binary-op f fs ...)
+  (pattern (#%plain-app op:float-binary-op f1 f2 fs ...)
            #:with opt 
            (begin (log-optimization "binary float" #'op)
-                  (for/fold ([o #'f.opt])
-                      ([e (syntax->list #'(fs.opt ...))])
+                  (for/fold ([o #'f1.opt])
+                      ([e (syntax->list #'(f2.opt fs.opt ...))])
                     #`(op.unsafe #,o #,e))))
   (pattern (#%plain-app op:pair-unary-op p)
            #:with opt
@@ -99,10 +105,10 @@
                                     #:exists 'append)
                   (current-output-port))))
     (begin0
-          (parameterize ([current-output-port port])
-            (syntax-parse stx #:literal-sets (kernel-literals)
-                          [e:opt-expr
-                           (syntax/loc stx e.opt)]))
+      (parameterize ([current-output-port port])
+        (syntax-parse stx #:literal-sets (kernel-literals)
+                      [e:opt-expr
+                       (syntax/loc stx e.opt)]))
       (if (and *log-optimizations?*
                *log-optimizatons-to-log-file?*)
           (close-output-port port)
diff --git a/collects/typed-scheme/private/parse-type.rkt b/collects/typed-scheme/private/parse-type.rkt
index 77287839..3477ec06 100644
--- a/collects/typed-scheme/private/parse-type.rkt
+++ b/collects/typed-scheme/private/parse-type.rkt
@@ -365,8 +365,6 @@
       [((~and kw values) tys ...) 
        (add-type-name-reference #'kw)
        (-values (map parse-type (syntax->list #'(tys ...))))]
-      [(t:All . rest)
-       (parse-all-type stx parse-values-type)]
       [t
        (-values (list (parse-type #'t)))])))
 
diff --git a/collects/typed-scheme/private/prims.rkt b/collects/typed-scheme/private/prims.rkt
index 7101c3be..048cd7f0 100644
--- a/collects/typed-scheme/private/prims.rkt
+++ b/collects/typed-scheme/private/prims.rkt
@@ -39,7 +39,8 @@ This file defines two sorts of primitives. All of them are provided into any mod
           (private internal)
 	  (except-in (utils utils tc-utils))
           (env type-name-env)
-          "type-contract.rkt"))
+          "type-contract.rkt"
+          "for-clauses.rkt"))
 
 (require (utils require-contract)
          "colon.rkt"
@@ -47,7 +48,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
          (except-in mzlib/contract ->)
          (only-in mzlib/contract [-> c->])
          mzlib/struct
-         "base-types.rkt"
+         "base-types-new.rkt"
          "base-types-extra.rkt")
 
 (define-for-syntax (ignore stx) (syntax-property stx 'typechecker:ignore #t))
@@ -79,7 +80,9 @@ This file defines two sorts of primitives. All of them are provided into any mod
              #:fail-unless (eq? 'opaque (syntax-e #'opaque)) #f
              #:with opt #'(#:name-exists)))
   (syntax-parse stx
-    [(_ lib (~or sc:simple-clause strc:struct-clause oc:opaque-clause) ...)
+    [(_ lib:expr (~or sc:simple-clause strc:struct-clause oc:opaque-clause) ...)
+     (unless (< 0 (length (syntax->list #'(sc ... strc ... oc ...))))
+       (raise-syntax-error #f "at least one specification is required" stx))
      #'(begin 
 	 (require/opaque-type oc.ty oc.pred lib . oc.opt) ...
 	 (require/typed sc.nm sc.ty lib) ... 
@@ -366,15 +369,39 @@ This file defines two sorts of primitives. All of them are provided into any mod
 (define-syntax (do: stx)
   (syntax-parse stx #:literals (:)
     [(_ : ty 
-        ((var:annotated-name init (~optional step:expr #:defaults ([step #'var]))) ...) 
-        (stop?:expr (~optional (~seq finish0:expr finish:expr ...) #:defaults ([finish0 #'(void)] [(finish 1) '()])))
+        ((var:annotated-name rest ...) ...) 
+        (stop?:expr ret ...)
         c:expr ...)
      (syntax/loc
          stx
-       (let: doloop : ty ([var.name : var.ty init] ...)
-         (if stop?
-             (begin finish0 finish ...)
-             (begin c ... (doloop step ...)))))]))
+       (ann (do ((var.ann-name rest ...) ...)
+                (stop? ret ...)
+              c ...)
+            ty))]))
+
+(define-for-syntax (define-for-variant name)
+  (lambda (stx)
+    (syntax-parse stx #:literals (:)
+      [(_ : ty
+          clauses
+          c:expr ...)
+       (convert-for-clauses name #'clauses #'(c ...) #'ty)])))
+(define-syntax (define-for-variants stx)
+  (syntax-parse stx
+    [(_ (name untyped-name) ...)
+     (quasisyntax/loc
+         stx
+       (begin (define-syntax name (define-for-variant #'untyped-name)) ...))]))
+(define-for-variants
+  (for: for)
+  (for/list: for/list)
+  (for/hash: for/hash)
+  (for/hasheq: for/hasheq)
+  (for/hasheqv: for/hasheqv)
+  (for/and: for/and)
+  (for/or: for/or)
+  (for/first: for/first)
+  (for/last: for/last))
 
 (define-syntax (provide: stx)
   (syntax-parse stx
diff --git a/collects/typed-scheme/private/with-types.rkt b/collects/typed-scheme/private/with-types.rkt
index 52b506a5..29d30b10 100644
--- a/collects/typed-scheme/private/with-types.rkt
+++ b/collects/typed-scheme/private/with-types.rkt
@@ -8,7 +8,6 @@
 	 "base-env-indexing-old.rkt"
 	 "extra-procs.rkt"
          "prims.rkt"
-         "base-types.rkt"
          racket/contract/regions racket/contract/base
          (for-syntax 
           "base-types-extra.rkt"
diff --git a/collects/typed-scheme/rep/rep-utils.rkt b/collects/typed-scheme/rep/rep-utils.rkt
index 3e3cc464..ade55c9f 100644
--- a/collects/typed-scheme/rep/rep-utils.rkt
+++ b/collects/typed-scheme/rep/rep-utils.rkt
@@ -1,7 +1,7 @@
 #lang scheme/base
 (require "../utils/utils.rkt")
 
-(require mzlib/struct 
+(require mzlib/struct mzlib/pconvert
          scheme/match
          syntax/boundmap
          "free-variance.rkt"
@@ -265,4 +265,20 @@
   (apply maker (list-update flds idx new-val)))
 
 (define (replace-syntax rep stx)
-  (replace-field rep stx 3))
\ No newline at end of file
+  (replace-field rep stx 3))
+
+(define (converter v basic sub)
+  (define (gen-constructor sym)
+    (string->symbol (string-append "make-" (substring (symbol->string sym) 7))))
+  (match v
+    [(? (lambda (e) (or (Filter? e)
+                        (Object? e)
+                        (PathElem? e)))
+        (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx vals)))
+     `(,(gen-constructor tag) ,@(map sub vals))]
+    [(? Type?
+        (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx key vals)))
+     `(,(gen-constructor tag) ,@(map sub vals))]
+    [_ (basic v)]))
+
+(current-print-convert-hook converter)
\ No newline at end of file
diff --git a/collects/typed-scheme/typecheck/signatures.rkt b/collects/typed-scheme/typecheck/signatures.rkt
index 15ff49be..14103c35 100644
--- a/collects/typed-scheme/typecheck/signatures.rkt
+++ b/collects/typed-scheme/typecheck/signatures.rkt
@@ -6,10 +6,6 @@
          (types utils))
 (provide (all-defined-out))
 
-(define-signature typechecker^
-  ([cnt type-check (syntax? . -> . syntax?)] 
-   [cnt tc-toplevel-form (syntax? . -> . any)]))
-
 (define-signature tc-expr^
   ([cnt tc-expr (syntax? . -> . tc-results?)]
    [cnt tc-literal (->* (syntax?) ((or/c #f Type/c)) Type/c)]
diff --git a/collects/typed-scheme/typecheck/tc-app-helper.rkt b/collects/typed-scheme/typecheck/tc-app-helper.rkt
index a2c7457c..d829d632 100644
--- a/collects/typed-scheme/typecheck/tc-app-helper.rkt
+++ b/collects/typed-scheme/typecheck/tc-app-helper.rkt
@@ -1,13 +1,14 @@
 #lang scheme/base
 
 (require "../utils/utils.rkt" scheme/match unstable/list
-         (utils tc-utils) (rep type-rep) (types utils union))
+         (utils tc-utils) (rep type-rep) (types utils union abbrev))
 
 (provide (all-defined-out))
 
 (define (make-printable t)
   (match t
     [(tc-result1: t) t]
+    [(tc-results: ts) (-values ts)]
     [_ t]))
 
 (define (stringify-domain dom rst drst [rng #f])
diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.rkt b/collects/typed-scheme/typecheck/tc-expr-unit.rkt
index 06f04b5e..6a102aca 100644
--- a/collects/typed-scheme/typecheck/tc-expr-unit.rkt
+++ b/collects/typed-scheme/typecheck/tc-expr-unit.rkt
@@ -181,88 +181,69 @@
     (match* (o1 o2)
       [(o o) #t]
       [(o (or (NoObject:) (Empty:))) #t]
-      [(_ _) #f]))
-  (define (maybe-abstract r)
-    (define l (hash-ref to-be-abstr expected #f))
-    (define (sub-one proc i)
-      (for/fold ([s i])
-        ([nm (in-list l)])
-        (proc s nm (make-Empty) #t)))
-    (define (subber proc lst)
-      (for/list ([i (in-list lst)])
-        (sub-one proc i)))
-    (if l
-        (match r
-          [(tc-results: ts fs os) 
-           (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os))]
-          [(tc-results: ts fs os dt db) 
-           (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os) (sub-one subst-type dt) db)]
-          [t (sub-one subst-type t)])
-        r))
-  (let ([tr1 (maybe-abstract tr1)])
-    (match* (tr1 expected)
-      ;; these two have to be first so that errors can be allowed in cases where multiple values are expected
-      [((tc-result1: (? (lambda (t) (type-equal? t (Un))))) (tc-results: ts2 (NoFilter:) (NoObject:)))
-       (ret ts2)]
-      [((tc-result1: (? (lambda (t) (type-equal? t (Un))))) _)
-       expected]
-      
-      [((tc-results: ts fs os) (tc-results: ts2 (NoFilter:) (NoObject:)))
-       (unless (= (length ts) (length ts2))
-         (tc-error/expr "Expected ~a values, but got ~a" (length ts2) (length ts)))
-       (unless (for/and ([t ts] [s ts2]) (subtype t s))
-         (tc-error/expr "Expected ~a, but got ~a" (stringify ts2) (stringify ts)))
-       (if (= (length ts) (length ts2))
-           (ret ts2 fs os)
-           (ret ts2))]
-      [((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (Top:) (Top:)) (Empty:)))
-       (cond 
-         [(not (subtype t1 t2))
-          (tc-error/expr "Expected ~a, but got ~a" t2 t1)])
-       expected]
-      [((tc-result1: t1 f1 o1) (tc-result1: t2 f2 o2))
-       (cond 
-         [(not (subtype t1 t2))
-          (tc-error/expr "Expected ~a, but got ~a" t2 t1)]
-         [(and (not (filter-better? f1 f2))
-               (object-better? o1 o2))
-          (tc-error/expr "Expected result with filter ~a, got filter ~a" f2 f1)]
-         [(and (filter-better? f1 f2)
-               (not (object-better? o1 o2)))
-          (tc-error/expr "Expected result with object ~a, got object ~a" o2 o1)]
-         [(and (not (filter-better? f1 f2))
-               (not (object-better? o1 o2)))
-          (tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))]
-         [else
-          expected])]
-      [((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound))
-       (unless (andmap subtype t1 t2)
-         (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
-       expected]
-      [((tc-results: t1 fs os) (tc-results: t2 fs os))
-       (unless (= (length t1) (length t2))
-         (tc-error/expr "Expected ~a values, but got ~a" (length t2) (length t1)))
-       (unless (for/and ([t t1] [s t2]) (subtype t s))
-         (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
-       expected]
-      [((tc-result1: t1 f o) (? Type? t2))
-       (unless (subtype t1 t2)
+      [(_ _) #f]))  
+  (match* (tr1 expected)
+    ;; these two have to be first so that errors can be allowed in cases where multiple values are expected
+    [((tc-result1: (? (lambda (t) (type-equal? t (Un))))) (tc-results: ts2 (NoFilter:) (NoObject:)))
+     (ret ts2)]
+    [((tc-result1: (? (lambda (t) (type-equal? t (Un))))) _)
+     expected]
+    
+    [((tc-results: ts fs os) (tc-results: ts2 (NoFilter:) (NoObject:)))
+     (unless (= (length ts) (length ts2))
+       (tc-error/expr "Expected ~a values, but got ~a" (length ts2) (length ts)))
+     (unless (for/and ([t ts] [s ts2]) (subtype t s))
+       (tc-error/expr "Expected ~a, but got ~a" (stringify ts2) (stringify ts)))
+     (if (= (length ts) (length ts2))
+         (ret ts2 fs os)
+         (ret ts2))]
+    [((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (Top:) (Top:)) (Empty:)))
+     (cond 
+       [(not (subtype t1 t2))
+        (tc-error/expr "Expected ~a, but got ~a" t2 t1)])
+     expected]
+    [((tc-result1: t1 f1 o1) (tc-result1: t2 f2 o2))
+     (cond 
+       [(not (subtype t1 t2))
+        (tc-error/expr "Expected ~a, but got ~a" t2 t1)]
+       [(and (not (filter-better? f1 f2))
+             (object-better? o1 o2))
+        (tc-error/expr "Expected result with filter ~a, got filter ~a" f2 f1)]
+       [(and (filter-better? f1 f2)
+             (not (object-better? o1 o2)))
+        (tc-error/expr "Expected result with object ~a, got object ~a" o2 o1)]
+       [(and (not (filter-better? f1 f2))
+             (not (object-better? o1 o2)))
+        (tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))])
+     expected]
+    [((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound))
+     (unless (andmap subtype t1 t2)
+       (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
+     expected]
+    [((tc-results: t1 fs os) (tc-results: t2 fs os))
+     (unless (= (length t1) (length t2))
+       (tc-error/expr "Expected ~a values, but got ~a" (length t2) (length t1)))
+     (unless (for/and ([t t1] [s t2]) (subtype t s))
+       (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
+     expected]
+    [((tc-result1: t1 f o) (? Type? t2))
+     (unless (subtype t1 t2)
+       (tc-error/expr "Expected ~a, but got ~a" t2 t1))
+     (ret t2 f o)]
+    [((? Type? t1) (tc-result1: t2 (FilterSet: (list) (list)) (Empty:)))
+     (unless (subtype t1 t2)
+       (tc-error/expr "Expected ~a, but got ~a" t2 t1))
+     t1]
+    [((? Type? t1) (tc-result1: t2 f o))
+     (if (subtype t1 t2)
+         (tc-error/expr "Expected result with filter ~a and ~a, got ~a" f (print-object o) t1)
          (tc-error/expr "Expected ~a, but got ~a" t2 t1))
-       (ret t2 f o)]
-      [((? Type? t1) (tc-result1: t2 (FilterSet: (list) (list)) (Empty:)))
-       (unless (subtype t1 t2)
-         (tc-error/expr "Expected ~a, but got ~a" t2 t1))
-       t1]
-      [((? Type? t1) (tc-result1: t2 f o))
-       (if (subtype t1 t2)
-           (tc-error/expr "Expected result with filter ~a and ~a, got ~a" f (print-object o) t1)
-           (tc-error/expr "Expected ~a, but got ~a" t2 t1))
-       t1]
-      [((? Type? t1) (? Type? t2))
-       (unless (subtype t1 t2)
-         (tc-error/expr "Expected ~a, but got ~a" t2 t1))
-       expected]
-      [(a b) (int-err "unexpected input for check-below: ~a ~a" a b)])))
+     t1]
+    [((? Type? t1) (? Type? t2))
+     (unless (subtype t1 t2)
+       (tc-error/expr "Expected ~a, but got ~a" t2 t1))
+     expected]
+    [(a b) (int-err "unexpected input for check-below: ~a ~a" a b)]))
 
 (define (tc-expr/check/type form expected)
   #;(syntax? Type/c . -> . tc-results?)
diff --git a/collects/typed-scheme/typecheck/tc-if.rkt b/collects/typed-scheme/typecheck/tc-if.rkt
index 5fedc8e2..aa50b85b 100644
--- a/collects/typed-scheme/typecheck/tc-if.rkt
+++ b/collects/typed-scheme/typecheck/tc-if.rkt
@@ -50,10 +50,12 @@
                                            (env-props env-els))]
                     [(tc-results: ts fs2 os2) (with-lexical-env env-thn (tc thn (unbox flag+)))]
                     [(tc-results: us fs3 os3) (with-lexical-env env-els (tc els (unbox flag-)))])
-         ;(printf "old els-props: ~a\n" (env-props (lexical-env)))
+         ;(printf "old props: ~a\n" (env-props (lexical-env)))
+         ;(printf "fs+: ~a~n" fs+)
          ;(printf "fs-: ~a~n" fs-)
-         ;(printf "els-props: ~a~n" (env-props env-els))
          ;(printf "thn-props: ~a~n" (env-props env-thn))
+         ;(printf "els-props: ~a~n" (env-props env-els))
+         ;(printf "new-thn-props: ~a~n" new-thn-props)
          ;(printf "new-els-props: ~a~n" new-els-props)
          ;; if we have the same number of values in both cases
          (cond [(= (length ts) (length us))
@@ -66,6 +68,7 @@
                                      [(_ (NoFilter:))
                                       (-FS -top -top)]
                                      [((FilterSet: f2+ f2-) (FilterSet: f3+ f3-))
+                                      ;(printf "f2- ~a f+ ~a\n" f2- fs+)
                                       (-FS (-or (apply -and fs+ f2+ new-thn-props) (apply -and fs- f3+ new-els-props))
                                            (-or (apply -and fs+ f2- new-thn-props) (apply -and fs- f3- new-els-props)))])]
                                   [type (Un t2 t3)]
diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.rkt b/collects/typed-scheme/typecheck/tc-lambda-unit.rkt
index 4aab25a9..f2438b08 100644
--- a/collects/typed-scheme/typecheck/tc-lambda-unit.rkt
+++ b/collects/typed-scheme/typecheck/tc-lambda-unit.rkt
@@ -41,7 +41,8 @@
         (abstract-results body arg-names)
         #:kws (map make-Keyword kw kw-ty req?)
         #:rest (if rest (second rest) #f)
-        #:drest (if drest (cdr drest) #f)))]))
+        #:drest (if drest (cdr drest) #f)))]
+    [_ (int-err "not a lam-result")]))
 
 (define (expected-str tys-len rest-ty drest arg-len rest)
   (format "Expected function with ~a argument~a~a, but got function with ~a argument~a~a"
@@ -74,11 +75,11 @@
     (define (check-body)
       (with-lexical-env/extend 
        arg-list arg-types
-       (lam-result (for/list ([al arg-list] [at arg-types] [a-ty arg-tys]) (list al at)) null 
-                   (and rest-ty (list (or rest (generate-temporary)) rest-ty))
-                   ;; make up a fake name if none exists, this is an error case anyway
-                   (and drest (cons (or rest (generate-temporary)) drest))
-                   (tc-exprs/check (syntax->list body) ret-ty))))
+       (make-lam-result (for/list ([al arg-list] [at arg-types] [a-ty arg-tys]) (list al at)) null 
+                        (and rest-ty (list (or rest (generate-temporary)) rest-ty))
+                        ;; make up a fake name if none exists, this is an error case anyway
+                        (and drest (cons (or rest (generate-temporary)) drest))
+                        (tc-exprs/check (syntax->list body) ret-ty))))
     (when (or (not (= arg-len tys-len))
               (and (or rest-ty drest) (not rest)))
       (tc-error/delayed (expected-str tys-len rest-ty drest arg-len rest)))
@@ -152,7 +153,7 @@
                (parameterize ([dotted-env (extend-env (list #'rest)
                                                       (list (cons rest-type bound))
                                                       (dotted-env))])
-                 (make lam-result
+                 (make-lam-result
                        (map list arg-list arg-types)
                        null
                        #f
@@ -163,7 +164,7 @@
             (with-lexical-env/extend 
              (cons #'rest arg-list) 
              (cons (make-Listof rest-type) arg-types)
-             (make lam-result
+             (make-lam-result
                    (map list arg-list arg-types)
                    null
                    (list #'rest rest-type)
@@ -245,7 +246,7 @@
        (tc/plambda form formals bodies expected)]
       [(tc-result1: (Error:)) (tc/mono-lambda/type formals bodies #f)]
       [(tc-result1: (and v (Values: _))) (maybe-loop form formals bodies (values->tc-results v #f))]
-      [(tc-result1: t) (int-err "expected not an appropriate tc-result: ~a ~a" expected t)]))
+      [_ (int-err "expected not an appropriate tc-result: ~a" expected)]))
   (match expected
     [(tc-result1: (and t (Poly-names: ns expected*)))
      (let* ([tvars (let ([p (syntax-property form 'typechecker:plambda)])
@@ -299,7 +300,8 @@
      (unless (check-below (tc/plambda form formals bodies #f) t)
        (tc-error/expr #:return expected
                       "Expected a value of type ~a, but got a polymorphic function." t))
-     t]))
+     t]
+    [_ (int-err "not a good expected value: ~a" expected)]))
 
 ;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic
 ;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> tc-result
diff --git a/collects/typed-scheme/typecheck/tc-let-unit.rkt b/collects/typed-scheme/typecheck/tc-let-unit.rkt
index 1569f46c..23cf379a 100644
--- a/collects/typed-scheme/typecheck/tc-let-unit.rkt
+++ b/collects/typed-scheme/typecheck/tc-let-unit.rkt
@@ -21,6 +21,11 @@
 (import tc-expr^)
 (export tc-let^)
 
+(define (erase-filter tc)
+  (match tc
+    [(tc-results: ts _ _)
+     (ret ts (for/list ([f ts]) (make-NoFilter)) (for/list ([f ts]) (make-NoObject)))]))
+
 (d/c (do-check expr->type namess results form exprs body clauses expected #:abstract [abstract null])
      (((syntax? syntax? tc-results? . c:-> . any/c)
        (listof (listof identifier?)) (listof tc-results?)
@@ -66,17 +71,17 @@
                      (for/fold ([s i])
                        ([nm (in-list (apply append abstract namess))])
                        (proc s nm (make-Empty) #t))))])
+     (define (run res)
+       (match res
+         [(tc-results: ts fs os)
+          (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os))]
+         [(tc-results: ts fs os dt db)
+          (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os) dt db)]))
      (if expected 
-         (begin
-           (hash-update! to-be-abstr expected
-                         (lambda (old-l) (apply append old-l abstract namess))
-                         null)
-           (tc-exprs/check (syntax->list body) expected))
-         (match (tc-exprs (syntax->list body))           
-           [(tc-results: ts fs os)
-            (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os))]
-           [(tc-results: ts fs os dt db)
-            (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os) dt db)])))))
+         (check-below 
+          (run (tc-exprs/check (syntax->list body) (erase-filter expected)))
+          expected)
+         (run (tc-exprs (syntax->list body)))))))
 
 (define (tc/letrec-values/check namess exprs body form expected)
   (tc/letrec-values/internal namess exprs body form expected))
diff --git a/collects/typed-scheme/typecheck/tc-toplevel.rkt b/collects/typed-scheme/typecheck/tc-toplevel.rkt
index b0e02534..7db4b125 100644
--- a/collects/typed-scheme/typecheck/tc-toplevel.rkt
+++ b/collects/typed-scheme/typecheck/tc-toplevel.rkt
@@ -1,31 +1,33 @@
-#lang scheme/unit
+#lang racket/base
 
-
-(require (rename-in "../utils/utils.rkt" [infer r:infer]))
-(require syntax/kerncase
-	 unstable/list unstable/syntax syntax/parse unstable/debug
+(require (rename-in "../utils/utils.rkt" [infer r:infer])
+         syntax/kerncase
+         unstable/list unstable/syntax syntax/parse unstable/debug
          mzlib/etc
          scheme/match
          "signatures.rkt"
          "tc-structs.rkt"
+         "typechecker.rkt"
          ;; to appease syntax-parse
          "internal-forms.rkt"
          (rep type-rep)
          (types utils convenience)
          (private parse-type type-annotation type-contract)
          (env type-env init-envs type-name-env type-alias-env lexical-env)
-	 unstable/mutated-vars syntax/id-table
+         unstable/mutated-vars syntax/id-table
          (utils tc-utils)
          "provide-handling.rkt"
          "def-binding.rkt"
+         (prefix-in c: racket/contract)
          (for-template
           "internal-forms.rkt"
           unstable/location
           mzlib/contract
           scheme/base))
 
-(import tc-expr^ check-subforms^)
-(export typechecker^)
+(c:provide/contract 
+ [type-check (syntax? . c:-> . syntax?)] 
+ [tc-toplevel-form (syntax? . c:-> . c:any/c)])
 
 (define unann-defs (make-free-id-table))
 
diff --git a/collects/typed-scheme/typecheck/typechecker.rkt b/collects/typed-scheme/typecheck/typechecker.rkt
index 13da5f36..1434e0b9 100644
--- a/collects/typed-scheme/typecheck/typechecker.rkt
+++ b/collects/typed-scheme/typecheck/typechecker.rkt
@@ -6,12 +6,12 @@
          (only-in scheme/unit
                   provide-signature-elements
                   define-values/invoke-unit/infer link)
-         "signatures.rkt" "tc-toplevel.rkt"
+         "signatures.rkt"
          "tc-if.rkt" "tc-lambda-unit.rkt" "tc-app.rkt"
          "tc-let-unit.rkt" "tc-dots-unit.rkt"
          "tc-expr-unit.rkt" "check-subforms-unit.rkt")
 
-(provide-signature-elements typechecker^ tc-expr^)
+(provide-signature-elements tc-expr^ check-subforms^)
 
 (define-values/invoke-unit/infer
-  (link tc-toplevel@ tc-if@ tc-lambda@ tc-dots@ tc-app@ tc-let@ tc-expr@ check-subforms@))
+  (link tc-if@ tc-lambda@ tc-dots@ tc-app@ tc-let@ tc-expr@ check-subforms@))
diff --git a/collects/typed-scheme/typed-scheme.rkt b/collects/typed-scheme/typed-scheme.rkt
index 6798070f..615cc6b4 100644
--- a/collects/typed-scheme/typed-scheme.rkt
+++ b/collects/typed-scheme/typed-scheme.rkt
@@ -2,13 +2,13 @@
 
 (require (rename-in "utils/utils.rkt" [infer r:infer]))
 
-(require (private base-types with-types)
+(require (private with-types)
          (for-syntax 
           (except-in syntax/parse id)
           scheme/base
           (private type-contract optimize)
           (types utils convenience)
-	  (typecheck typechecker provide-handling)
+	  (typecheck typechecker provide-handling tc-toplevel)
 	  (env type-environments type-name-env type-alias-env)
 	  (r:infer infer)
 	  (utils tc-utils)
diff --git a/collects/typed-scheme/types/printer.rkt b/collects/typed-scheme/types/printer.rkt
index 61d92dd9..ba991333 100644
--- a/collects/typed-scheme/types/printer.rkt
+++ b/collects/typed-scheme/types/printer.rkt
@@ -1,9 +1,8 @@
 #lang scheme/base
 
-(require "../utils/utils.rkt")
-(require (rep type-rep filter-rep object-rep rep-utils)
-	 (utils tc-utils)
-	 scheme/match)
+(require unstable/sequence racket/require racket/match
+         (path-up "rep/type-rep.rkt" "rep/filter-rep.rkt" "rep/object-rep.rkt"
+                  "rep/rep-utils.rkt" "utils/utils.rkt" "utils/tc-utils.rkt"))
 
 ;; do we attempt to find instantiations of polymorphic types to print? 
 ;; FIXME - currently broken
@@ -18,16 +17,10 @@
 ;; does t have a type name associated with it currently?
 ;; has-name : Type -> Maybe[Symbol]
 (define (has-name? t) 
-  (define ns ((current-type-names)))
-  (let/ec return
-    (unless print-aliases
-      (return #f))
-    (for-each
-     (lambda (pair)
-       (cond [(eq? t (cdr pair))
-              (return (car pair))]))
-     ns)
-    #f))
+  (and print-aliases
+       (for/first ([(n t*) (in-pairs (in-list ((current-type-names))))]
+                   #:when (and (Type? t*) (type-equal? t t*)))
+         n)))
 
 (define (print-filter c port write?)
   (define (fp . args) (apply fprintf port args))
@@ -61,7 +54,7 @@
   (define (fp . args) (apply fprintf port args))
   (match c
     [(NoObject:) (fp "-")]
-    [(Empty:) (fp "")]
+    [(Empty:) (fp "-")]
     [(Path: pes i) (fp "~a" (append pes (list i)))]    
     [else (fp "(Unknown Object: ~a)" (struct->vector c))]))
 
@@ -126,9 +119,8 @@
     [(Univ:) (fp "Any")]
     ;; special case number until something better happens
     ;;[(Base: 'Number _) (fp "Number")]
-    [(? has-name?) 
-     #;(printf "has a name\n")
-     (fp "~a" (has-name? c))]
+    [(app has-name? (? values name))
+     (fp "~a" name)]
     [(StructTop: st) (fp "~a" st)]
     [(BoxTop:) (fp "Box")]
     [(VectorTop:) (fp "Vector")]
diff --git a/collects/typed-scheme/utils/utils.rkt b/collects/typed-scheme/utils/utils.rkt
index b6d9364b..493ab95a 100644
--- a/collects/typed-scheme/utils/utils.rkt
+++ b/collects/typed-scheme/utils/utils.rkt
@@ -139,15 +139,12 @@ at least theoretically.
   print-type* print-filter* print-latentfilter* print-object* print-latentobject*
   print-pathelem*)
 
-(define pseudo-printer
-  (lambda (s port mode)
-    (parameterize ([current-output-port port]
-                   [show-sharing #f]
-                   [booleans-as-true/false #f]
-                   [constructor-style-printing #t])
-      (newline)
-      (pretty-print (print-convert s))
-      (newline))))
+(define (pseudo-printer s port mode)
+  (parameterize ([current-output-port port]
+                 [show-sharing #f]
+                 [booleans-as-true/false #f]
+                 [constructor-style-printing #t])
+    (pretty-print (print-convert s))))
 
 (define custom-printer (make-parameter #t))
   
diff --git a/collects/typed/racket/base.rkt b/collects/typed/racket/base.rkt
index 8c71a40b..6f7c5c75 100644
--- a/collects/typed/racket/base.rkt
+++ b/collects/typed/racket/base.rkt
@@ -2,7 +2,7 @@
            
 
 
-(providing (libs (except racket/base #%module-begin #%top-interaction with-handlers lambda #%app)
+(providing (libs (except racket/base #%module-begin #%top-interaction with-handlers lambda #%app define-struct)
                  (except typed-scheme/private/prims)
                  (except typed-scheme/private/base-types-new)
                  (except typed-scheme/private/base-types-extra))
diff --git a/collects/typed/scheme/base.rkt b/collects/typed/scheme/base.rkt
index 4c6c52cb..fa662f89 100644
--- a/collects/typed/scheme/base.rkt
+++ b/collects/typed/scheme/base.rkt
@@ -2,7 +2,7 @@
            
 
 
-(providing (libs (except scheme/base #%module-begin #%top-interaction with-handlers lambda #%app)
+(providing (libs (except scheme/base #%module-begin #%top-interaction with-handlers lambda #%app define-struct)
                  (except typed-scheme/private/prims)
                  (except typed-scheme/private/base-types-new)
                  (except typed-scheme/private/base-types-extra))