diff --git a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss
index adba6e63..9c3c7d34 100644
--- a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss
@@ -23,6 +23,8 @@
 			      (begin (test-suite "Tests for subtyping"
 						 new-cl ...))))]))
 
+(infer-param infer)
+
 (define (subtype-tests)
   (subtyping-tests
    ;; trivial examples
@@ -121,6 +123,8 @@
 
    (FAIL (-poly (a b) (-> a a)) (-poly (a b) (-> a b)))
    
+   ;; polymorphic function types should be subtypes of the function top
+   [(-poly (a) (a . -> . a)) top-func]   
    ))
 
 (define-go 
diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss
index c83e0706..bcfc0e85 100644
--- a/collects/typed-scheme/infer/infer-unit.ss
+++ b/collects/typed-scheme/infer/infer-unit.ss
@@ -251,154 +251,157 @@
       (parameterize ([match-equality-test type-equal?]
                      [current-seen (remember S T (current-seen))])
         (match* 
-         (S T)
-         [(a a) empty]
-         [(_ (Univ:)) empty]
-         
-         [((F: (? (lambda (e) (memq e X)) v)) S)
-          (when (match S
-                  [(F: v*)
-                   (just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))]
-                  [_ #f])
-            (fail! S T))
-          (singleton (Un) v (var-demote S V))]
-         [(S (F: (? (lambda (e) (memq e X)) v)))
-          (when (match S
-                  [(F: v*)
-                   (just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))]
-                  [_ #f])
-            (fail! S T))
-          (singleton (var-promote S V) v Univ)]
-         
-         ;; two unions with the same number of elements, so we just try to unify them pairwise
-         #;[((Union: l1) (Union: l2))
-            (=> unmatch)
-            (unless (= (length l1) (length l2))
-              (unmatch))
-            (cgen-union V X l1 l2)]
-         
-         #;[((Poly: v1 b1) (Poly: v2 b2))
-          (unless (= (length v1) (length v2))
-            (fail! S T))
-          (let ([b2* (subst-all (map list v2 v1) b2)])
-            (cg b1 b2*))]
-         
-         #;[((PolyDots: (list v1 ... r1) b1) (PolyDots: (list v2 ... r2) b2))
-          (unless (= (length v1) (length v2))
-            (fail! S T))
-          (let ([b2* (substitute-dotted v1 v1 v2 (subst-all (map list v2 v1) b2))])
-            (cg b1 b2*))]
-         
-         [((Poly: v1 b1) T)
-          (cgen (append v1 V) X b1 T)]
-
-         #;[((PolyDots: (list v1 ... r1) b1) T)
-          (let ([b1* (var-demote b1 (cons r1 v1))])
-            (cg b1* T))]
-
-         #;
-         [((Poly-unsafe: n b) (Poly-unsafe: n* b*))
-          (unless (= n n*)
-            (fail! S T))
-          (cg b b*)]
-         
-         
-         [((Union: es) S) (cset-meet* (cons empty (for/list ([e es]) (cg e S))))]
-         ;; we might want to use multiple csets here, but I don't think it makes a difference
-         [(S (Union: es)) (or
-                           (for/or 
-                            ([e es]) 
-                            (with-handlers
-                                ([exn:infer? (lambda _ #f)])
-                              (cg S e)))
-                           (fail! S T))]
-         
-         [((Struct: nm p flds proc _ _ _) (Struct: nm p flds* proc* _ _ _))
-          (let-values ([(flds flds*)
-                        (cond [(and proc proc*)
-                               (values (cons proc flds) (cons proc* flds*))]
-                              [(or proc proc*)
-                               (fail! S T)]
-                              [else (values flds flds*)])])
-            (cgen/list V X flds flds*))]
-         [((Name: n) (Name: n*))
-          (if (free-identifier=? n n*)
-              null
-              (fail! S T))]
-         [((Pair: a b) (Pair: a* b*))
-          (cset-meet (cg a a*) (cg b b*))]
-         ;; if we have two mu's, we rename them to have the same variable
-         ;; and then compare the bodies
-         [((Mu-unsafe: s) (Mu-unsafe: t)) 
-          (cg s t)]
-         ;; other mu's just get unfolded
-         [(s (? Mu? t)) (cg s (unfold t))]
-         [((? Mu? s) t) (cg (unfold s) t)]
-         ;; type application          
-         [((App: (Name: n) args _)
-           (App: (Name: n*) args* _))
-          (unless (free-identifier=? n n*)
-            (fail! S T))
-          (let ([x (instantiate-poly (lookup-type-name n) args)]
-                [y (instantiate-poly (lookup-type-name n) args*)])
-            (cg x y))]
-         [((Values: ss) (Values: ts))
-          (unless (= (length ss) (length ts))
-            (fail! ss ts))
-          (cgen/list V X ss ts)]
-         [((Values: ss) (ValuesDots: ts t-dty dbound))
-          (unless (>= (length ss) (length ts))
-            (fail! ss ts))
-          (unless (memq dbound X)
-            (fail! S T))
-          (let* ([num-vars (- (length ss) (length ts))]
-                 [vars     (for/list ([n (in-range num-vars)])
-                                     (gensym dbound))]
-                 [new-tys  (for/list ([var vars])
-                                     (substitute (make-F var) dbound t-dty))]
-                 [new-cset (cgen/list V (append vars X) ss (append ts new-tys))])
-            (move-vars-to-dmap new-cset dbound vars))]
-         [((ValuesDots: ss s-dty dbound) (Values: ts))
-          (unless (>= (length ts) (length ss))
-            (fail! ss ts))
-          (unless (memq dbound X)
-            (fail! S T))
-          (let* ([num-vars (- (length ts) (length ss))]
-                 [vars     (for/list ([n (in-range num-vars)])
-                                     (gensym dbound))]
-                 [new-tys  (for/list ([var vars])
-                                     (substitute (make-F var) dbound s-dty))]
-                 [new-cset (cgen/list V (append vars X) (append ss new-tys) ts)])
-            (move-vars-to-dmap new-cset dbound vars))]
-         [((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound))
-          (when (memq dbound X) (fail! ss ts))          
-          (cgen/list V X (cons s-dty ss) (cons t-dty ts))]
-         [((Vector: e) (Vector: e*))
-          (cset-meet (cg e e*) (cg e* e))]
-         [((Box: e) (Box: e*))
-          (cset-meet (cg e e*) (cg e* e))]
-         [((Hashtable: s1 s2) (Hashtable: t1 t2))
-          ;; the key is covariant, the value is invariant
-          (cset-meet* (list (cg s1 t1) (cg t2 s2) (cg s2 t2)))]
-         [((Syntax: s1) (Syntax: s2))
-          (cg s1 s2)]
-         ;; parameters are just like one-arg functions
-         [((Param: in1 out1) (Param: in2 out2))
-          (cset-meet (cg in2 in1) (cg out1 out2))]
-         [((Function: (list t-arr ...))
-           (Function: (list s-arr ...)))
-          (=> unmatch)
-          (cset-combine
-           (filter 
-            values ;; only generate the successful csets
-            (for*/list 
-             ([t-arr t-arr] [s-arr s-arr])
-             (with-handlers ([exn:infer? (lambda (_) #f)])
-               (cgen/arr V X t-arr s-arr)))))]
-         [(_ _)
-          (cond [(subtype S T) empty]
-                ;; or, nothing worked, and we fail
-                [else (fail! S T)])]))))
+            (S T)
+          [(a a) empty]
+          [(_ (Univ:)) empty]
+          
+          [((F: (? (lambda (e) (memq e X)) v)) S)
+           (when (match S
+                   [(F: v*)
+                    (just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))]
+                   [_ #f])
+             (fail! S T))
+           (singleton (Un) v (var-demote S V))]
+          [(S (F: (? (lambda (e) (memq e X)) v)))
+           (when (match S
+                   [(F: v*)
+                    (just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))]
+                   [_ #f])
+             (fail! S T))
+           (singleton (var-promote S V) v Univ)]
+          
+          ;; two unions with the same number of elements, so we just try to unify them pairwise
+          #;[((Union: l1) (Union: l2))
+             (=> unmatch)
+             (unless (= (length l1) (length l2))
+               (unmatch))
+             (cgen-union V X l1 l2)]
+          
+          #;[((Poly: v1 b1) (Poly: v2 b2))
+             (unless (= (length v1) (length v2))
+               (fail! S T))
+             (let ([b2* (subst-all (map list v2 v1) b2)])
+               (cg b1 b2*))]
+          
+          #;[((PolyDots: (list v1 ... r1) b1) (PolyDots: (list v2 ... r2) b2))
+             (unless (= (length v1) (length v2))
+               (fail! S T))
+             (let ([b2* (substitute-dotted v1 v1 v2 (subst-all (map list v2 v1) b2))])
+               (cg b1 b2*))]
+          
+          [((Poly: v1 b1) T)
+           (cgen (append v1 V) X b1 T)]
+          
+          #;[((PolyDots: (list v1 ... r1) b1) T)
+             (let ([b1* (var-demote b1 (cons r1 v1))])
+               (cg b1* T))]
+          
+          #;
+          [((Poly-unsafe: n b) (Poly-unsafe: n* b*))
+           (unless (= n n*)
+             (fail! S T))
+           (cg b b*)]
+          
+          
+          [((Union: es) S) (cset-meet* (cons empty (for/list ([e es]) (cg e S))))]
+          ;; we might want to use multiple csets here, but I don't think it makes a difference
+          [(S (Union: es)) (or
+                            (for/or 
+                             ([e es]) 
+                             (with-handlers
+                                 ([exn:infer? (lambda _ #f)])
+                               (cg S e)))
+                            (fail! S T))]
+          
+          [((Struct: nm p flds proc _ _ _) (Struct: nm p flds* proc* _ _ _))
+           (let-values ([(flds flds*)
+                         (cond [(and proc proc*)
+                                (values (cons proc flds) (cons proc* flds*))]
+                               [(or proc proc*)
+                                (fail! S T)]
+                               [else (values flds flds*)])])
+             (cgen/list V X flds flds*))]
+          [((Name: n) (Name: n*))
+           (if (free-identifier=? n n*)
+               null
+               (fail! S T))]
+          [((Pair: a b) (Pair: a* b*))
+           (cset-meet (cg a a*) (cg b b*))]
+          ;; if we have two mu's, we rename them to have the same variable
+          ;; and then compare the bodies
+          [((Mu-unsafe: s) (Mu-unsafe: t)) 
+           (cg s t)]
+          ;; other mu's just get unfolded
+          [(s (? Mu? t)) (cg s (unfold t))]
+          [((? Mu? s) t) (cg (unfold s) t)]
+          ;; type application          
+          [((App: (Name: n) args _)
+            (App: (Name: n*) args* _))
+           (unless (free-identifier=? n n*)
+             (fail! S T))
+           (let ([x (instantiate-poly (lookup-type-name n) args)]
+                 [y (instantiate-poly (lookup-type-name n) args*)])
+             (cg x y))]
+          [((Values: ss) (Values: ts))
+           (unless (= (length ss) (length ts))
+             (fail! ss ts))
+           (cgen/list V X ss ts)]
+          [((Values: ss) (ValuesDots: ts t-dty dbound))
+           (unless (>= (length ss) (length ts))
+             (fail! ss ts))
+           (unless (memq dbound X)
+             (fail! S T))
+           (let* ([num-vars (- (length ss) (length ts))]
+                  [vars     (for/list ([n (in-range num-vars)])
+                              (gensym dbound))]
+                  [new-tys  (for/list ([var vars])
+                              (substitute (make-F var) dbound t-dty))]
+                  [new-cset (cgen/list V (append vars X) ss (append ts new-tys))])
+             (move-vars-to-dmap new-cset dbound vars))]
+          [((ValuesDots: ss s-dty dbound) (Values: ts))
+           (unless (>= (length ts) (length ss))
+             (fail! ss ts))
+           (unless (memq dbound X)
+             (fail! S T))
+           (let* ([num-vars (- (length ts) (length ss))]
+                  [vars     (for/list ([n (in-range num-vars)])
+                              (gensym dbound))]
+                  [new-tys  (for/list ([var vars])
+                              (substitute (make-F var) dbound s-dty))]
+                  [new-cset (cgen/list V (append vars X) (append ss new-tys) ts)])
+             (move-vars-to-dmap new-cset dbound vars))]
+          [((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound))
+           (when (memq dbound X) (fail! ss ts))          
+           (cgen/list V X (cons s-dty ss) (cons t-dty ts))]
+          [((Vector: e) (Vector: e*))
+           (cset-meet (cg e e*) (cg e* e))]
+          [((Box: e) (Box: e*))
+           (cset-meet (cg e e*) (cg e* e))]
+          [((Hashtable: s1 s2) (Hashtable: t1 t2))
+           ;; the key is covariant, the value is invariant
+           (cset-meet* (list (cg s1 t1) (cg t2 s2) (cg s2 t2)))]
+          [((Syntax: s1) (Syntax: s2))
+           (cg s1 s2)]
+          ;; parameters are just like one-arg functions
+          [((Param: in1 out1) (Param: in2 out2))
+           (cset-meet (cg in2 in1) (cg out1 out2))]
+          [((Function: _)
+            (Function: (list (top-arr:))))
+           empty]
+          [((Function: (list t-arr ...))
+            (Function: (list s-arr ...)))
+           (=> unmatch)
+           (cset-combine
+            (filter 
+             values ;; only generate the successful csets
+             (for*/list 
+              ([t-arr t-arr] [s-arr s-arr])
+              (with-handlers ([exn:infer? (lambda (_) #f)])
+                (cgen/arr V X t-arr s-arr)))))]
+          [(_ _)
+           (cond [(subtype S T) empty]
+                 ;; or, nothing worked, and we fail
+                 [else (fail! S T)])]))))
 
 (define (check-vars must-vars subst)
   (and (for/and ([v must-vars])
@@ -488,4 +491,4 @@
 (define (i s t r)
   (infer/simple (list s) (list t) r))
 
-;(trace cgen/arr #;cgen #;cgen/list)
+;(trace cgen)
diff --git a/collects/typed-scheme/infer/signatures.ss b/collects/typed-scheme/infer/signatures.ss
index 6db02b38..a3b85665 100644
--- a/collects/typed-scheme/infer/signatures.ss
+++ b/collects/typed-scheme/infer/signatures.ss
@@ -1,29 +1,42 @@
 #lang scheme/base
-(require scheme/unit)
+(require scheme/unit scheme/contract "constraint-structs.ss" "../utils/utils.ss")
+(require (rep type-rep) (utils unit-utils))
 (provide (all-defined-out))
 
 (define-signature dmap^
-  (dmap-meet))
+  ([cnt dmap-meet (dmap? dmap? . -> . dmap?)]))
 
 (define-signature promote-demote^
-  (var-promote var-demote))
+  ([cnt var-promote (Type? (listof symbol?) . -> . Type?)]
+   [cnt var-demote  (Type? (listof symbol?) . -> . Type?)]))
 
 (define-signature constraints^
-  (exn:infer?
-   fail-sym
+  ([cnt exn:infer? (any/c . -> . boolean?)]
+   [cnt fail-sym symbol?]
    ;; inference failure - masked before it gets to the user program
    (define-syntaxes (fail!)
      (syntax-rules ()
        [(_ s t) (raise fail-sym)]))
-   cset-meet cset-meet*
+   [cnt cset-meet (cset? cset? . -> . cset?)]
+   [cnt cset-meet* ((listof cset?) . -> . cset?)]
    no-constraint
-   empty-cset
-   insert
-   cset-combine
-   c-meet))
+   [cnt empty-cset ((listof symbol?) . -> . cset?)]
+   [cnt insert (cset? symbol? Type? Type? . -> . cset?)]
+   [cnt cset-combine ((listof cset?) . -> . cset?)]
+   [cnt c-meet ((c? c?) (symbol?) . ->* . c?)]))
 
 (define-signature restrict^
-  (restrict))
+  ([cnt restrict (Type? Type? . -> . Type?)]))
 
 (define-signature infer^
-  (infer infer/vararg infer/dots))
+  ([cnt infer (((listof symbol?) (listof Type?) (listof Type?) Type? (listof symbol?)) ((or/c #f Type?)) . ->* . any)]
+   [cnt infer/vararg (((listof symbol?) 
+                       (listof Type?)
+                       (listof Type?)
+                       Type? Type?
+                       (listof symbol?))
+                      ((or/c #f Type?)) . ->* . any)]
+   [cnt infer/dots (((listof symbol?) 
+                     symbol?
+                     (listof Type?) (listof Type?) Type? Type? (listof symbol?))
+                    (#:expected (or/c #f Type?)) . ->* . any)]))
diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index f09bfea2..aaad95ba 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -90,7 +90,7 @@
 [symbol? (make-pred-ty Sym)]
 [list? (make-pred-ty (-lst Univ))]
 [list (-poly (a) (->* '() a (-lst a)))]
-[procedure? (make-pred-ty (make-Function (list (make-top-arr))))]
+[procedure? (make-pred-ty top-func)]
 [map (-polydots (c a b) ((list ((list a) (b b) . ->... . c) (-lst a))
                          ((-lst b) b) . ->... .(-lst c)))]
 [for-each (-polydots (c a b) ((list ((list a) (b b) . ->... . Univ) (-lst a))
@@ -561,4 +561,4 @@
 ;; string.ss
 [real->decimal-string (N [-Nat] . ->opt .  -String)]
 
-[current-continuation-marks (-> -Cont-Mark-Set)]
\ No newline at end of file
+[current-continuation-marks (-> -Cont-Mark-Set)]
diff --git a/collects/typed-scheme/private/base-types.ss b/collects/typed-scheme/private/base-types.ss
index 28c595e9..296bd88f 100644
--- a/collects/typed-scheme/private/base-types.ss
+++ b/collects/typed-scheme/private/base-types.ss
@@ -27,5 +27,5 @@
 [Boxof (-poly (a) (make-Box a))]
 [Syntax Any-Syntax]
 [Identifier Ident]
-[Procedure (make-Function (list (make-top-arr)))]
+[Procedure top-func]
 
diff --git a/collects/typed-scheme/private/require-contract.ss b/collects/typed-scheme/private/require-contract.ss
index c718b42f..bcfcc2ef 100644
--- a/collects/typed-scheme/private/require-contract.ss
+++ b/collects/typed-scheme/private/require-contract.ss
@@ -12,20 +12,20 @@
        (begin define-values)
        [(begin (define-values (n) e) e*)
         #`(begin (define-values (n) e)
-                 (define name #,(syntax-property #'e*
-                                                 'inferred-name
-                                                 (syntax-e #'name))))]
+                 (define name e*))]
        [(begin (begin e))
-        #`(define name #,(syntax-property #'e
-                                          'inferred-name
-                                          (syntax-e #'name)))])]))
+        #`(define name e)])]))
 
 (define-syntax (require/contract stx)
   (syntax-case stx ()
     [(require/contract nm cnt lib)
      (identifier? #'nm)
      #`(begin (require (only-in lib [nm tmp]))     
-              (define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen (quote-syntax nm))))]
+              (define-ignored nm (contract (let ([nm cnt]) nm) tmp 
+                                           '#,(syntax->datum #'nm)
+                                           'never-happen
+                                           (list (make-srcloc tmp #f #f #f #f) (symbol->string 'nm)))))]
     [(require/contract (orig-nm nm) cnt lib)     
      #`(begin (require (only-in lib [orig-nm tmp]))
-              (define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen (quote-syntax nm))))]))
+              (define-ignored nm (contract (let ([nm cnt]) nm)
+                                           tmp '#,(syntax->datum #'nm) 'never-happen (quote-syntax nm))))]))
diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index 699e966b..49f21dd8 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -17,11 +17,13 @@
 
 (provide (all-defined-out) 
          ;; these should all eventually go away
-         make-Name make-ValuesDots make-Function make-top-arr make-Latent-Restrict-Effect make-Latent-Remove-Effect)
+         make-Name make-ValuesDots make-Function make-Latent-Restrict-Effect make-Latent-Remove-Effect)
 
 (define (one-of/c . args)
   (apply Un (map -val args)))
 
+(define top-func (make-Function (list (make-top-arr))))
+
 (define (-vet id) (make-Var-True-Effect id))
 (define (-vef id) (make-Var-False-Effect id))
 
diff --git a/collects/typed-scheme/typecheck/check-subforms-unit.ss b/collects/typed-scheme/typecheck/check-subforms-unit.ss
index e37c6f37..3dd9208d 100644
--- a/collects/typed-scheme/typecheck/check-subforms-unit.ss
+++ b/collects/typed-scheme/typecheck/check-subforms-unit.ss
@@ -12,7 +12,7 @@
 (export check-subforms^)
 
 ;; find the subexpressions that need to be typechecked in an ignored form
-;; syntax -> void
+;; syntax -> any
 (define (check-subforms/with-handlers form)
   (define handler-tys '())
   (define body-ty #f)    
@@ -48,6 +48,7 @@
         [_ (void)])))
   (ret (apply Un body-ty handler-tys)))
 
+;; syntax type -> any
 (define (check-subforms/with-handlers/check form expected)
   (let loop ([form form])
     (parameterize ([current-orig-stx form])
@@ -73,7 +74,7 @@
   (ret expected))
 
 ;; typecheck the expansion of a with-handlers form
-;; syntax -> type
+;; syntax -> any
 (define (check-subforms/ignore form)
   (let loop ([form form])
     (kernel-syntax-case* form #f ()
diff --git a/collects/typed-scheme/typecheck/signatures.ss b/collects/typed-scheme/typecheck/signatures.ss
index 572becfd..530ad009 100644
--- a/collects/typed-scheme/typecheck/signatures.ss
+++ b/collects/typed-scheme/typecheck/signatures.ss
@@ -1,28 +1,49 @@
 #lang scheme/base
-(require scheme/unit)
+(require scheme/unit scheme/contract "../utils/utils.ss")
+(require (rep type-rep)
+         (utils unit-utils)
+         (private type-utils))
 (provide (all-defined-out))
 
 (define-signature typechecker^
-  (type-check tc-toplevel-form))
+  ([cnt type-check (syntax? . -> . syntax?)] 
+   [cnt tc-toplevel-form (syntax? . -> . any)]))
 
 (define-signature tc-expr^
-  (tc-expr tc-expr/check tc-expr/check/t check-below tc-literal tc-exprs tc-exprs/check tc-expr/t))
+  ([cnt tc-expr (syntax? . -> . tc-result?)]
+   [cnt tc-expr/check (syntax? Type? . -> . tc-result?)]
+   [cnt tc-expr/check/t (syntax? Type? . -> . Type?)]
+   [cnt check-below (->d ([s (or/c Type? tc-result?)] [t Type?]) () [_ (if (Type? s) Type? tc-result?)])]
+   [cnt tc-literal (any/c . -> . Type?)]
+   [cnt tc-exprs ((listof syntax?) . -> . tc-result?)]
+   [cnt tc-exprs/check ((listof syntax?) Type? . -> . tc-result?)]
+   [cnt tc-expr/t (syntax? . -> . Type?)]))
 
 (define-signature check-subforms^
-  (check-subforms/ignore check-subforms/with-handlers check-subforms/with-handlers/check))
+  ([cnt check-subforms/ignore (syntax? . -> . any)]
+   [cnt check-subforms/with-handlers (syntax? . -> . any)]
+   [cnt check-subforms/with-handlers/check (syntax? Type? . -> . any)]))
 
 (define-signature tc-if^
-  (tc/if-onearm tc/if-twoarm tc/if-onearm/check tc/if-twoarm/check))
+  ([cnt tc/if-twoarm (syntax? syntax? syntax? . -> . tc-result?)]   
+   [cnt tc/if-twoarm/check (syntax? syntax? syntax? Type? . -> . tc-result?)]))
 
 (define-signature tc-lambda^
-  (tc/lambda tc/lambda/check tc/rec-lambda/check))
+  ([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-result?)]
+   [cnt tc/lambda/check (syntax? syntax? syntax? Type? . -> . tc-result?)]
+   [cnt tc/rec-lambda/check (syntax? syntax? syntax? syntax? (listof Type?) Type? . -> . Type?)]))
 
 (define-signature tc-app^
-  (tc/app tc/app/check tc/funapp))
+  ([cnt tc/app (syntax? . -> . tc-result?)] 
+   [cnt tc/app/check (syntax? Type? . -> . tc-result?)]
+   [cnt tc/funapp (syntax? syntax? tc-result? (listof tc-result?) (or/c #f Type?) . -> . tc-result?)]))
 
 (define-signature tc-let^
-  (tc/let-values tc/letrec-values tc/let-values/check tc/letrec-values/check))
+  ([cnt tc/let-values (syntax? syntax? syntax? syntax? . -> . tc-result?)]
+   [cnt tc/letrec-values (syntax? syntax? syntax? syntax? . -> . tc-result?)]
+   [cnt tc/let-values/check (syntax? syntax? syntax? syntax? Type? . -> . tc-result?)]
+   [cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? Type? . -> . tc-result?)]))
 
 (define-signature tc-dots^
-  (tc/dots))
+  ([cnt tc/dots (syntax? . -> . (values Type? symbol?))]))
 
diff --git a/collects/typed-scheme/typecheck/tc-app-unit.ss b/collects/typed-scheme/typecheck/tc-app-unit.ss
index a341e184..739025da 100644
--- a/collects/typed-scheme/typecheck/tc-app-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-app-unit.ss
@@ -368,8 +368,8 @@
                      (let ([substitution (infer vars ... rng)])
                        (and substitution
                             (log-result substitution)
-                            (or expected
-                                (ret (subst-all substitution rng))))))             
+                            (ret (or expected
+                                     (subst-all substitution rng))))))
              (poly-fail t argtypes #:name (and (identifier? f-stx) f-stx)))))]))
 
 (define (poly-fail t argtypes #:name [name #f])
diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss
index 9f0831ae..f7769e73 100644
--- a/collects/typed-scheme/typecheck/tc-expr-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss
@@ -190,7 +190,6 @@
          (begin (tc-exprs/check (syntax->list #'es) Univ)
                 (tc-expr/check #'e expected))]          
         ;; if
-        [(if tst body) (tc/if-onearm/check #'tst #'body expected)]
         [(if tst thn els) (tc/if-twoarm/check #'tst #'thn #'els expected)]
         ;; lambda
         [(#%plain-lambda formals . body)
diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.ss b/collects/typed-scheme/typecheck/tc-lambda-unit.ss
index 962c480e..a4159fb6 100644
--- a/collects/typed-scheme/typecheck/tc-lambda-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-lambda-unit.ss
@@ -199,16 +199,18 @@
                  (cons (car bodies) bodies*)
                  (cons (syntax-len (car formals)) nums-seen))]))))
 
+;; tc/lambda : syntax syntax-list syntax-list -> tc-result
 (define (tc/lambda form formals bodies)
   (tc/lambda/internal form formals bodies #f))
 
 ;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic
-;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> Type
+;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> tc-result
 (define (tc/lambda/internal form formals bodies expected)
   (if (or (syntax-property form 'typechecker:plambda) (Poly? expected) (PolyDots? expected))
       (tc/plambda form formals bodies expected)
       (ret (tc/mono-lambda formals bodies expected))))
 
+;; tc/lambda : syntax syntax-list syntax-list Type -> tc-result
 (define (tc/lambda/check form formals bodies expected)
   (tc/lambda/internal form formals bodies expected))
 
diff --git a/collects/typed/net/cgi.ss b/collects/typed/net/cgi.ss
index 7287e6f0..65aac77c 100644
--- a/collects/typed/net/cgi.ss
+++ b/collects/typed/net/cgi.ss
@@ -3,13 +3,14 @@
 (require typed/private/utils)
 
 (require-typed-struct cgi-error () net/cgi)
-(require-typed-struct incomplete-%-suffix  ([chars : (Listof Char)]) net/cgi) 
-(require-typed-struct invalid-%-suffix  ([char : Char]) net/cgi)
+(require-typed-struct (incomplete-%-suffix cgi-error)  ([chars : (Listof Char)]) net/cgi) 
+(require-typed-struct (invalid-%-suffix cgi-error)  ([char : Char]) net/cgi)
   
+
 (require/typed/provide net/cgi
   [get-bindings (-> (Listof (cons (U Symbol String) String)))]
   [get-bindings/post (-> (Listof (Pair (U Symbol String) String)))]
-  [get-bindings/get (-> (Listof (Pair (U Symbol String) String)) )]
+  [get-bindings/get (-> (Listof (Pair (U Symbol String) String)))]
   [output-http-headers (-> Void)]
   [generate-html-output (case-lambda (String (Listof String) -> Void) 
 				     (String (Listof String) String String String String String -> Void))]
@@ -21,6 +22,7 @@
   [string->html (String -> String)]
   [generate-link-text (String String -> String)])
 
+
 (provide
  (struct-out cgi-error)
  (struct-out incomplete-%-suffix)
diff --git a/collects/typed/net/cookie.ss b/collects/typed/net/cookie.ss
index f2ff6022..391463b9 100644
--- a/collects/typed/net/cookie.ss
+++ b/collects/typed/net/cookie.ss
@@ -18,6 +18,6 @@
   [get-cookie (String String -> (Listof String))]
   [get-cookie/single (String String -> (Option String))])
 
-(require-typed-struct  cookie-error () net/cookie)
+(require-typed-struct (cookie-error exn:fail) () net/cookie)
 
 (provide Cookie cookie? (struct-out cookie-error))
\ No newline at end of file
diff --git a/collects/typed/net/mime.ss b/collects/typed/net/mime.ss
index 167f0003..5a9b3f7b 100644
--- a/collects/typed/net/mime.ss
+++ b/collects/typed/net/mime.ss
@@ -30,42 +30,35 @@
 
 
 ;; -- exceptions raised --
-(require/typed mime-error? (Any -> Boolean : (Opaque mime-error?)) net/mime)
-(require/typed unexpected-termination? (Any -> Boolean :(Opaque unexpected-termination?)) net/mime)
-(require/typed unexpected-termination-msg ((Opaque unexpected-termination?) -> message) net/mime)
-(require/typed missing-multipart-boundary-parameter? (Any -> Boolean : (Opaque missing-multipart-boundary-parameter?)) net/mime)
-(require/typed malformed-multipart-entity? (Any -> Boolean : (Opaque malformed-multipart-entity?)) net/mime)
-(require/typed malformed-multipart-entity-msg ((Opaque malformed-multipart-entity?)-> message) net/mime)
-(require/typed empty-mechanism? (Any -> Boolean : (Opaque empty-mechanism?)) net/mime)
-(require/typed empty-type? (Any -> Boolean : (Opaque empty-type?)) net/mime)
-(require/typed empty-subtype? (Any -> Boolean : (Opaque empty-subtype?)) net/mime)
-(require/typed empty-disposition-type? (Any -> Boolean : (Opaque empty-disposition-type?)) net/mime)
-
+#|
+(require-typed-struct mime-error () net/mime)
+(require-typed-struct (unexpected-termination mime-error) ([msg : String]) net/mime)
+(require-typed-struct (missing-multipart-boundary-parameter mime-error) () net/mime)
+(require-typed-struct (malformed-multipart-entity mime-error) ([msg : String]) net/mime)
+(require-typed-struct (empty-mechanism mime-error) () net/mime)
+(require-typed-struct (empty-type mime-error) () net/mime)
+(require-typed-struct (empty-subtype mime-error) () net/mime)
+(require-typed-struct (empty-disposition-type mime-error) () net/mime)
+|#
 
 ;; -- mime methods --
 (require/typed/provide net/mime
   [mime-analyze ((U Bytes Input-Port) Any -> message)])
 
 (provide
- ;; -- exceptions raised --
- mime-error? 
- unexpected-termination? 
- unexpected-termination-msg
- missing-multipart-boundary-parameter? 
- malformed-multipart-entity?
- malformed-multipart-entity-msg
- empty-mechanism? 
- empty-type? 
- empty-subtype?
- empty-disposition-type? 
- 
  ;; -- basic mime structures --
- message 
- entity
- 
- disposition
- 
- ;; -- mime methods --
- mime-analyze
-)
+ (struct-out message)
+ (struct-out entity) 
+ (struct-out disposition)
+ #|
+ (struct-out mime-error)
+ (struct-out unexpected-termination)
+ (struct-out missing-multipart-boundary)
+ (struct-out malformed-multipart-entity)
+ (struct-out empty-mechanism)
+ (struct-out empty-type)
+ (struct-out empty-subtype)
+ (struct-out empty-disposition-type)
+|#
+ )
 
diff --git a/collects/typed/net/nntp.ss b/collects/typed/net/nntp.ss
index 04468077..b66b7a53 100644
--- a/collects/typed/net/nntp.ss
+++ b/collects/typed/net/nntp.ss
@@ -2,8 +2,9 @@
   
 (require typed/private/utils)
 
-(require-typed-struct communicator ([sender : Number] [receiver : Number] [server : String] [port : Number])
-		      net/nntp)
+(require-typed-struct/provide
+ communicator ([sender : Number] [receiver : Number] [server : String] [port : Number])
+ net/nntp)
 
 (require/typed/provide net/nntp  
   [connect-to-server (case-lambda (String -> communicator) (String Number -> communicator))]
@@ -14,18 +15,17 @@
   [body-of-message (communicator Number -> (Listof String))]
   [newnews-since  (communicator Number -> (Listof String))]
   [generic-message-command (communicator Number -> (Listof String))]
-  [make-desired-header  (String -> String)] ;;-> Regexp
-  [extract-desired-headers ((Listof String) (Listof String) -> (Listof String))]) ;;2nd: Of Regexp
-#|
-;; requires structure inheritance
-(require-typed-struct nntp ()]
-(require-typed-struct unexpected-response ([code : Number] [text : String])]
-(require-typed-struct bad-status-line ([line : String])]
-(require-typed-struct premature-close ([communicator : communicator])]
-(require-typed-struct bad-newsgroup-line ([line : String])]
-(require-typed-struct non-existent-group ([group : String])]
-(require-typed-struct article-not-in-group ([article : Number])]
-(require-typed-struct no-group-selected ()]
-(require-typed-struct article-not-found ([article : Number])]
-(require-typed-struct authentication-rejected ()]
-|#
+  [make-desired-header  (String -> String)]
+  [extract-desired-headers ((Listof String) (Listof String) -> (Listof String))])
+
+(require-typed-struct/provide (nntp exn:fail) () net/nntp)
+(require-typed-struct/provide (unexpected-response nntp) ([code : Number] [text : String]) net/nntp)
+(require-typed-struct/provide (bad-status-line nntp) ([line : String]) net/nntp)
+(require-typed-struct/provide (premature-close nntp) ([communicator : communicator]) net/nntp)
+(require-typed-struct/provide (bad-newsgroup-line nntp) ([line : String]) net/nntp)
+(require-typed-struct/provide (non-existent-group nntp) ([group : String]) net/nntp)
+(require-typed-struct/provide (article-not-in-group nntp) ([article : Number]) net/nntp)
+(require-typed-struct/provide (no-group-selected nntp) () net/nntp)
+(require-typed-struct/provide (article-not-found nntp) ([article : Number]) net/nntp)
+(require-typed-struct/provide (authentication-rejected nntp) () net/nntp)
+
diff --git a/collects/typed/net/pop3.ss b/collects/typed/net/pop3.ss
index 8ecaa8f5..ddc23237 100644
--- a/collects/typed/net/pop3.ss
+++ b/collects/typed/net/pop3.ss
@@ -2,37 +2,43 @@
 
 (require typed/private/utils)
 
-(require-typed-struct communicator ([sender : Number] [receiver : Number] [server : String] [port : Number] [state : Symbol])net/pop3)
+(require-typed-struct/provide communicator
+			      ([sender : Number] [receiver : Number] [server : String] [port : Number] [state : Symbol])
+			      net/pop3)
 
 (require/typed/provide net/pop3
-  [connect-to-server ( case-lambda (String -> (Opaque communicator?)) (String Number -> (Opaque communicator?)) )] 
+  [connect-to-server (case-lambda (String -> communicator) (String Number -> communicator))] 
 
-  [disconnect-from-server ( (Opaque communicator?) -> Void )]
-  [authenticate/plain-text ( String String (Opaque communicator?) -> Void )]
-  [get-mailbox-status ( (Opaque communicator?) -> (values Number Number) )]
-  [get-message/complete  ( (Opaque communicator?) Number -> (values (Listof String)(Listof String)) )]
-  [get-message/headers  ( (Opaque communicator?) Number -> (Listof String) )]
-  [get-message/body ( (Opaque communicator?) Number -> (Listof String) )]
-  [delete-message ( (Opaque communicator?) Number -> Void )]
-  [get-unique-id/single  ( (Opaque communicator?) Number -> String )]
-  [get-unique-id/all ( (Opaque communicator?) -> (Listof (cons Number String)) )]
+  [disconnect-from-server (communicator -> Void)]
+  [authenticate/plain-text (String String communicator -> Void)]
+  [get-mailbox-status (communicator -> (values Number Number))]
+  [get-message/complete  (communicator Number -> (values (Listof String)(Listof String)))]
+  [get-message/headers  (communicator Number -> (Listof String))]
+  [get-message/body (communicator Number -> (Listof String))]
+  [delete-message (communicator Number -> Void)]
+  [get-unique-id/single  (communicator Number -> String)]
+  [get-unique-id/all (communicator -> (Listof (cons Number String)))]
   
-  [make-desired-header  ( String -> String )];-> Regexp
-  [extract-desired-headers ( (Listof String)(Listof String)-> (Listof String) )];2nd:of Regexp
-  )
-(provide (struct-out communicator))
+  [make-desired-header  (String -> String)]
+  [extract-desired-headers ((Listof String)(Listof String)-> (Listof String))])
+ 
+
+(require-typed-struct/provide (pop3 exn) () net/pop3)
+(require-typed-struct/provide (cannot-connect pop3) () net/pop3)
+(require-typed-struct/provide (username-rejected pop3) () net/pop3)
+(require-typed-struct/provide (password-rejected pop3) () net/pop3)
+(require-typed-struct/provide (not-ready-for-transaction pop3) 
+			      ([communicator : communicator]) net/pop3) 
+(require-typed-struct/provide (not-given-headers pop3)
+			      ([communicator : communicator] [message : Integer]) net/pop3)
+(require-typed-struct/provide (illegal-message-number pop3)
+			      ([communicator : communicator] [message : Integer]) net/pop3)
+(require-typed-struct/provide (cannot-delete-message pop3)
+			      ([communicator : communicator] [message : Integer]) net/pop3) 
+(require-typed-struct/provide (disconnect-not-quiet pop3)
+			      ([communicator : communicator]) net/pop3)
+(require-typed-struct/provide (malformed-server-response pop3) 
+			      ([communicator : communicator]) net/pop3) 
 
-#|
-(require-typed-struct pop3 ()]
-(require-typed-struct cannot-connect ()]
-(require-typed-struct username-rejected ()]
-(require-typed-struct password-rejected ()]
-(require-typed-struct not-ready-for-transaction ([ communicator : (Opaque communicator?) ])net/pop3) 
-(require-typed-struct not-given-headers ([ communicator : (Opaque communicator?) ] [message : String])]
-(require-typed-struct illegal-message-number ([communicator : (Opaque communicator?)] [message : String])]
-(require-typed-struct cannot-delete-message ([communicator : (Opaque communicator?)] [message : String])] 
-(require-typed-struct disconnect-not-quiet ([communicator : (Opaque communicator?)])]
-(require-typed-struct malformed-server-response ([communicator : (Opaque communicator?)])net/pop3) 
-|#
 
   
\ No newline at end of file
diff --git a/collects/typed/net/url.ss b/collects/typed/net/url.ss
index 86add4fe..b9623196 100644
--- a/collects/typed/net/url.ss
+++ b/collects/typed/net/url.ss
@@ -2,19 +2,21 @@
 
 (require typed/private/utils)
 
-(require-typed-struct path/param ([path : (U String 'up 'same)] [param : (Listof String)]) net/url)
+(require-typed-struct/provide path/param ([path : (U String 'up 'same)] [param : (Listof String)]) net/url)
 
-(require-typed-struct url ([scheme : (Option String)]
-                           [user : (Option String)]
-                           [host : (Option String)]
-                           [port : (Option Integer)]
-                           [path-absolute? : Boolean]
-                           [path : (Listof path/param)] 
-                           [query : (Listof (Pair Symbol (Option String)))]
-                           [fragment : (Option String)])
-                      net/url)
+(require-typed-struct/provide
+ url ([scheme : (Option String)]
+      [user : (Option String)]
+      [host : (Option String)]
+      [port : (Option Integer)]
+      [path-absolute? : Boolean]
+      [path : (Listof path/param)] 
+      [query : (Listof (Pair Symbol (Option String)))]
+      [fragment : (Option String)])
+ net/url)
 
 (require/opaque-type URL-Exception url-exception? net/url)
+(provide URL-Exception url-exception?)   
 
 (define-type-alias PortT (case-lambda (url -> Input-Port) (url (Listof String)-> Input-Port)))
 (define-type-alias PortT/String (case-lambda (url String -> Input-Port) (url String (Listof String)-> Input-Port)))
@@ -52,8 +54,3 @@
   [url->string (url -> String)]
   [combine-url/relative (url String -> url)])
 
-(provide
- URL-Exception
- url-exception?
- (struct-out url)
- (struct-out path/param))   
diff --git a/collects/typed/private/utils.ss b/collects/typed/private/utils.ss
index c1fdbea7..5abf5a87 100644
--- a/collects/typed/private/utils.ss
+++ b/collects/typed/private/utils.ss
@@ -8,4 +8,13 @@
     (require/typed lib [nm t] ...)
     (provide nm ...)))
 
-(provide dt require/typed/provide)
+(define-syntax require-typed-struct/provide
+  (syntax-rules ()
+    [(_ (nm par) . rest)
+     (begin (require-typed-struct (nm par) . rest)
+            (provide (struct-out nm)))]
+    [(_ nm . rest)
+     (begin (require-typed-struct nm . rest)
+            (provide (struct-out nm)))]))
+
+(provide dt require/typed/provide require-typed-struct/provide)