diff --git a/collects/tests/typed-scheme/fail/with-type1.ss b/collects/tests/typed-scheme/fail/with-type1.ss
index 4acf56ae..0bdefd3b 100644
--- a/collects/tests/typed-scheme/fail/with-type1.ss
+++ b/collects/tests/typed-scheme/fail/with-type1.ss
@@ -3,6 +3,6 @@
 #lang scheme
 (require typed/scheme)
 
-((with-type (Number -> Number)
+((with-type #:result (Number -> Number)
    (lambda: ([x : Number]) (add1 x)))
  #f)
diff --git a/collects/tests/typed-scheme/fail/with-type2.ss b/collects/tests/typed-scheme/fail/with-type2.ss
index 75824a07..f435976c 100644
--- a/collects/tests/typed-scheme/fail/with-type2.ss
+++ b/collects/tests/typed-scheme/fail/with-type2.ss
@@ -5,6 +5,7 @@
 (require typed/scheme)
 
 (let ([x 'hello])
-  (with-type String
-    #:freevars ([x String])
-    (string-append x ", world")))
\ No newline at end of file
+  (with-type
+   #:result String
+   #:freevars ([x String])
+   (string-append x ", world")))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/require-procedure.ss b/collects/tests/typed-scheme/succeed/require-procedure.ss
new file mode 100644
index 00000000..42fe3f7d
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/require-procedure.ss
@@ -0,0 +1,2 @@
+#lang typed/scheme
+(require/typed scheme [procedure-arity (Procedure -> Natural)])
diff --git a/collects/tests/typed-scheme/succeed/with-type.ss b/collects/tests/typed-scheme/succeed/with-type.ss
index 2ce8853d..05907864 100644
--- a/collects/tests/typed-scheme/succeed/with-type.ss
+++ b/collects/tests/typed-scheme/succeed/with-type.ss
@@ -1,9 +1,18 @@
 #lang scheme
 (require typed/scheme)
 
-(with-type Number 3)
+(with-type #:result Number 3)
 
 (let ([x "hello"])
-  (with-type String
+  (with-type #:result String
     #:freevars ([x String])
     (string-append x ", world")))
+
+(with-type ([fun (Number -> Number)]
+            [val Number])
+  (define (fun x) x)
+  (define val 17))
+
+(fun val)
+val
+
diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss
index 6f0bf6c7..472524a4 100644
--- a/collects/typed-scheme/env/init-envs.ss
+++ b/collects/typed-scheme/env/init-envs.ss
@@ -41,10 +41,10 @@
     [(? (lambda (e) (or (LatentFilter? e)
                         (LatentObject? e)
                         (PathElem? e)))
-        (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals))) 
+        (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx vals)))
      `(,(gen-constructor tag) ,@(map sub vals))]
-    [(? (lambda (e) (or (Type? e)))
-        (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag key seq 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)]))
 
diff --git a/collects/typed-scheme/private/base-types-new.ss b/collects/typed-scheme/private/base-types-new.ss
index ffa92162..33ea9c7b 100644
--- a/collects/typed-scheme/private/base-types-new.ss
+++ b/collects/typed-scheme/private/base-types-new.ss
@@ -49,3 +49,4 @@
 [Nothing (Un)]
 [Pairof (-poly (a b) (-pair a b))]
 [MPairof (-poly (a b) (-mpair a b))]
+
diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss
index aaf679b6..269e91fa 100644
--- a/collects/typed-scheme/private/type-contract.ss
+++ b/collects/typed-scheme/private/type-contract.ss
@@ -57,6 +57,7 @@
       (define (t->c/neg t #:seen [structs-seen structs-seen]) (loop t (not pos?) (not from-typed?) structs-seen))
       (define (t->c/fun f #:method [method? #f])
         (match f
+          [(Function: (list (top-arr:))) #'procedure?]
           [(Function: arrs)
            (let ()           
              (define (f a)
@@ -90,11 +91,15 @@
                      #'((dom* ...) (opt-dom* ...) #:rest (listof rst*) . ->* . rng*)
                      #'(dom* ... . -> . rng*))))
              (unless (no-duplicates (for/list ([t arrs])
-                                      (match t [(arr: dom _ _ _ _) (length dom)])))
+                                      (match t
+                                        [(arr: dom _ _ _ _) (length dom)]
+                                        ;; is there something more sensible here?
+                                        [(top-arr:) (int-err "got top-arr")])))
                (exit (fail)))
              (match (map f arrs)
                [(list e) e]
-               [l #`(case-> #,@l)]))]))
+               [l #`(case-> #,@l)]))]
+          [_ (int-err "not a function" f)]))
       (match ty
         [(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))]
         ;; any/c doesn't provide protection in positive position
diff --git a/collects/typed-scheme/private/with-types.ss b/collects/typed-scheme/private/with-types.ss
index 1cb4d12b..484ea45b 100644
--- a/collects/typed-scheme/private/with-types.ss
+++ b/collects/typed-scheme/private/with-types.ss
@@ -9,85 +9,135 @@
 	 "extra-procs.ss"
          "prims.ss"
          "base-types.ss"
-         scheme/contract/regions scheme/contract/base
-         (for-syntax "base-types-extra.ss")
-         (for-syntax (except-in "../utils/utils.ss" infer)
-                     "../utils/tc-utils.ss"
-                     (except-in (combine-in "../types/convenience.ss" "../types/abbrev.ss") ->)                     
-                     "../types/utils.ss"
-                     "../infer/infer.ss"
-                     "../env/type-env.ss"
-                     "../env/type-environments.ss"
-                     "../env/type-name-env.ss"
-                     "../env/type-alias-env.ss"
-                     "../infer/infer-dummy.ss"
-                     "../private/parse-type.ss"
-                     "../private/type-contract.ss"
-                     "../typecheck/typechecker.ss"))
+         scheme/contract/regions scheme/contract/base         
+         (for-syntax 
+          "base-types-extra.ss"
+          unstable/debug
+          (path-up "env/type-name-env.ss"
+                   "env/type-alias-env.ss"
+                   "infer/infer-dummy.ss"
+                   "private/parse-type.ss"
+                   "private/type-contract.ss"
+                   "typecheck/typechecker.ss"
+                   "env/type-environments.ss" 
+                   "env/type-env.ss"
+                   "infer/infer.ss"
+                   "utils/tc-utils.ss"
+                   "types/utils.ss")
+          (except-in (path-up "utils/utils.ss" "types/convenience.ss" "types/abbrev.ss") infer ->)))
 
 (provide with-type)
+
+(define-for-syntax (with-type-helper stx body fvids fvtys exids extys resty expr? ctx)
+  (begin-with-definitions
+    (define old-context (unbox typed-context?))
+    (set-box! typed-context? #t)
+    (define fv-types (for/list ([t (in-list (syntax->list fvtys))])
+                       (parse-type t)))
+    (define fv-cnts (for/list ([t (in-list fv-types)]
+                               [stx (in-list (syntax->list fvtys))])
+                      (type->contract t #:typed-side #f 
+                                      (lambda () (tc-error/stx stx "Type ~a could not be converted to a contract." t)))))
+    (define ex-types (for/list ([t (syntax->list extys)])
+                       (parse-type t)))
+    (define ex-cnts (for/list ([t (in-list ex-types)]
+                               [stx (in-list (syntax->list extys))])
+                      (type->contract t #:typed-side #t
+                                      (lambda () (tc-error/stx stx "Type ~a could not be converted to a contract." t)))))
+    (define region-tc-result 
+      (and expr? (parse-tc-results resty)))
+    (define region-cnt 
+      (and region-tc-result
+           (match region-tc-result 
+             [(tc-result1: t) (type->contract 
+                               t 
+                               #:typed-side #t
+                               (lambda () (tc-error/stx #'region-ty-stx "Type ~a could not be converted to a contract." t)))])))
+    (for ([i (in-list (syntax->list fvids))]
+          [ty (in-list fv-types)])
+      (register-type i ty))
+    (define expanded-body 
+      (if expr?
+          (with-syntax ([body body])
+            (local-expand #'(let () . body) ctx null))
+          (with-syntax ([(body ...) body]
+                        [(id ...) exids]
+                        [(ty ...) extys])
+            (local-expand #'(let () (begin (: id ty) ... body ... (values id ...))) ctx null))))
+    (parameterize (;; disable fancy printing?
+                   [custom-printer #t]
+                   ;; a cheat to avoid units
+                   [infer-param infer]
+                   ;; do we report multiple errors
+                   [delay-errors? #t]
+                   ;; this parameter is for parsing types
+                   [current-tvars initial-tvar-env]
+                   ;; this parameter is just for printing types
+                   ;; this is a parameter to avoid dependency issues
+                   [current-type-names
+                    (lambda ()
+                      (append 
+                       (type-name-env-map (lambda (id ty)
+                                            (cons (syntax-e id) ty)))
+                       (type-alias-env-map (lambda (id ty)
+                                             (cons (syntax-e id) ty)))))]
+                   ;; reinitialize seen type variables
+                   [type-name-references null]
+                   ;; for error reporting
+                   [orig-module-stx stx]
+                   [expanded-module-stx expanded-body])
+      (if expr?
+          (tc-expr/check expanded-body region-tc-result)
+          (tc-expr/check expanded-body (ret ex-types))))
+    (report-all-errors)
+    (set-box! typed-context? old-context)
+    ;; then clear the new entries from the env ht
+    (for ([i (in-list (syntax->list fvids))])
+      (unregister-type i))
+    (with-syntax ([(fv.id ...) fvids]
+                  [(cnt ...) fv-cnts]
+                  [(ex-id ...) exids]
+                  [(ex-cnt ...) ex-cnts]
+                  [region-cnt region-cnt]
+                  [body expanded-body]
+                  [check-syntax-help (syntax-property #'(void) 'disappeared-use (type-name-references))])
+      (if expr?
+          (quasisyntax/loc stx
+            (begin check-syntax-help
+                   (with-contract typed-region
+                     #:result region-cnt
+                     #:freevars ([fv.id cnt] ...)                                
+                     body)))
+          (syntax/loc stx
+            (begin
+              (define-values () (begin check-syntax-help (values)))
+              (with-contract typed-region
+                ([ex-id ex-cnt] ...)
+                (define-values (ex-id ...) body))))))))
+
 (define-syntax (with-type stx)
+  (define-syntax-class typed-id
+    #:description "[id type]"
+    [pattern (id ty)])
   (define-splicing-syntax-class free-vars
+    #:description "free variable specification"
     #:attributes ((id 1) (ty 1))
-    [pattern (~seq #:freevars ([id ty] ...))]
+    [pattern (~seq #:freevars (:typed-id ...))]
     [pattern (~seq)
              #:with (id ...) null
              #:with (ty ...) null])
+  (define-syntax-class typed-ids
+    #:description "sequence of typed identifiers"
+    #:attributes ((id 1) (ty 1))
+    [pattern (t:typed-id ...)
+             #:with (id ...) #'(t.id ...)
+             #:with (ty ...) #'(t.ty ...)])
+  (define-splicing-syntax-class result-ty
+    #:description "result specification"
+    [pattern (~seq #:result ty:expr)])
   (syntax-parse stx
-    [(_ region-ty-stx fv:free-vars . body)
-     (begin-with-definitions
-       (define old-context (unbox typed-context?))
-       (set-box! typed-context? #t)
-       (define region-tc-result (parse-tc-results #'region-ty-stx))
-       (define region-cnt (match region-tc-result 
-                            [(tc-result1: t) (type->contract 
-                                              t 
-                                              (lambda () (tc-error/stx #'region-ty-stx "Type ~a could not be converted to a contract." t)))]))
-       (define fv-types (for/list ([t (syntax->list #'(fv.ty ...))])
-                          (parse-type t)))
-       (define fv-cnts (for/list ([t (in-list fv-types)]
-                                  [stx (in-list (syntax->list #'(fv.ty ...)))])
-                         (type->contract t #:typed-side #f 
-                                         (lambda () (tc-error/stx stx "Type ~a could not be converted to a contract." t)))))
-       (for ([i (in-list (syntax->list #'(fv.id ...)))]
-             [ty (in-list fv-types)])
-         (register-type i ty))
-       (define expanded-body (local-expand #'(let () . body) 'expression null))
-       (parameterize (;; disable fancy printing?
-                      [custom-printer #t]
-                      ;; a cheat to avoid units
-                      [infer-param infer]
-                      ;; do we report multiple errors
-                      [delay-errors? #t]
-                      ;; this parameter is for parsing types
-                      [current-tvars initial-tvar-env]
-                      ;; this parameter is just for printing types
-                      ;; this is a parameter to avoid dependency issues
-                      [current-type-names
-                       (lambda ()
-                         (append 
-                          (type-name-env-map (lambda (id ty)
-                                               (cons (syntax-e id) ty)))
-                          (type-alias-env-map (lambda (id ty)
-                                                (cons (syntax-e id) ty)))))]
-                      ;; reinitialize seen type variables
-                      [type-name-references null]
-                      ;; for error reporting
-                      [orig-module-stx stx]
-                      [expanded-module-stx expanded-body])
-         (tc-expr/check expanded-body region-tc-result))
-       (report-all-errors)
-       (set-box! typed-context? old-context)
-       ;; then clear the new entries from the env ht
-       (for ([i (in-list (syntax->list #'(fv.id ...)))])
-         (unregister-type i))
-       (with-syntax ([(cnt ...) fv-cnts]
-                     [region-cnt region-cnt]
-                     [check-syntax-help (syntax-property #'(void) 'disappeared-use (type-name-references))])
-         (quasisyntax/loc stx
-           (begin check-syntax-help
-                  (with-contract typed-region
-                                 #:result region-cnt
-                                 #:freevars ([fv.id cnt] ...)                                
-                                 . body)))))]))
+    [(_ :typed-ids fv:free-vars . body)
+     (with-type-helper stx #'body #'(fv.id ...) #'(fv.ty ...) #'(id ...) #'(ty ...) #f #f (syntax-local-context))]
+    [(_ :result-ty fv:free-vars . body)
+     (with-type-helper stx #'body #'(fv.id ...) #'(fv.ty ...) #'() #'() #'ty #t (syntax-local-context))]))
  
\ No newline at end of file
diff --git a/collects/typed-scheme/rep/rep-utils.ss b/collects/typed-scheme/rep/rep-utils.ss
index 8721b913..331d888e 100644
--- a/collects/typed-scheme/rep/rep-utils.ss
+++ b/collects/typed-scheme/rep/rep-utils.ss
@@ -25,7 +25,7 @@
 
 (provide == defintern hash-id (for-syntax fold-target))
 
-(define-struct Rep (seq free-vars free-idxs stx))
+(define-struct Rep (seq free-vars free-idxs stx) #:transparent)
 
 (define-for-syntax fold-target #'fold-target)
 (define-for-syntax default-fields (list #'seq #'free-vars #'free-idxs #'stx))
diff --git a/collects/typed-scheme/scribblings/ts-reference.scrbl b/collects/typed-scheme/scribblings/ts-reference.scrbl
index 5b7bd3d2..e9cd7889 100644
--- a/collects/typed-scheme/scribblings/ts-reference.scrbl
+++ b/collects/typed-scheme/scribblings/ts-reference.scrbl
@@ -337,28 +337,43 @@ Examples:
 
 The @scheme[with-type] for allows for localized Typed Scheme regions in otherwise untyped code.
 
-@defform/subs[(with-type type fv-clause body ...+)
+@defform*/subs[[(with-type result-spec fv-clause body ...+)
+                (with-type export-spec fv-clause body ...+)]
               ([fv-clause code:blank
-                          (code:line #:freevars ([id fv-type] ...))])]{
-Checks that @scheme[body ...+] has the type @scheme[type].  The @scheme[id]s are assumed to 
-have the types ascribed to them; these types are converted to contracts and checked dynamically.
-Uses of the result value are also appropriately checked by a contract generated from 
+                          (code:line #:freevars ([id fv-type] ...))]
+               [result-spec (code:line #:result type)]
+               [export-spec ([export-id export-type] ...)])]{
+The first form, an expression, checks that @scheme[body ...+] has the type @scheme[type].  
+Uses of the result value are appropriately checked by a contract generated from 
 @scheme[type].
 
+The second form, which can be used as a definition, checks that each of the @scheme[export-id]s 
+has the specified type.  These types are also enforced in the surrounding code with contracts.
+
+The @scheme[id]s are assumed to 
+have the types ascribed to them; these types are converted to contracts and checked dynamically.
+
 @examples[#:eval the-eval
 (with-type Number 3)
 
-((with-type (Number -> Number)
+((with-type #:result (Number -> Number)
    (lambda: ([x : Number]) (add1 x)))
  #f)
 
 (let ([x "hello"])
-  (with-type String
+  (with-type #:result String
     #:freevars ([x String])
     (string-append x ", world")))
 
 (let ([x 'hello])
-  (with-type String
+  (with-type #:result String
     #:freevars ([x String])
-    (string-append x ", world")))]
+    (string-append x ", world")))
+
+(with-type ([fun (Number -> Number)]
+            [val Number])
+  (define (fun x) x)
+  (define val 17))
+
+(fun val)]
 }
diff --git a/collects/typed-scheme/types/convenience.ss b/collects/typed-scheme/types/convenience.ss
index c4e9e96b..ae5fbb4e 100644
--- a/collects/typed-scheme/types/convenience.ss
+++ b/collects/typed-scheme/types/convenience.ss
@@ -2,7 +2,7 @@
 (require "../utils/utils.ss"
          (rep type-rep filter-rep object-rep)
          (utils tc-utils)
-         "abbrev.ss"
+         "abbrev.ss" (only-in scheme/contract current-blame-format)
 	 (types comparison printer union subtype utils)
          scheme/list scheme/match scheme/promise
          (for-syntax syntax/parse scheme/base)
@@ -14,7 +14,6 @@
          make-Name make-ValuesDots make-Function
          (rep-out filter-rep object-rep))
 
-
 (define (one-of/c . args)
   (apply Un (map -val args)))
 
@@ -47,7 +46,7 @@
 
 (define In-Syntax
   (-mu e
-       (*Un -Boolean -Symbol -String -Keyword -Char -Number (-val null)
+       (*Un (-val null) -Boolean -Symbol -String -Keyword -Char -Number 
             (make-Vector (-Syntax e))
             (make-Box (-Syntax e))
             (-lst (-Syntax e))
@@ -57,8 +56,8 @@
 
 (define (-Sexpof t)
   (-mu sexp
-       (Un -Number -Boolean -Symbol -String -Keyword -Char
-           (-val '())
+       (Un (-val '())
+           -Number -Boolean -Symbol -String -Keyword -Char           
            (-pair sexp sexp)
            (make-Vector sexp)
            (make-Box sexp)
diff --git a/collects/typed-scheme/utils/utils.ss b/collects/typed-scheme/utils/utils.ss
index d51753ad..86a287ed 100644
--- a/collects/typed-scheme/utils/utils.ss
+++ b/collects/typed-scheme/utils/utils.ss
@@ -126,8 +126,6 @@ at least theoretically.
 ;; - 1 printers have to be defined at the same time as the structs
 ;; - 2 we want to support things printing corectly even when the custom printer is off
 
-(define-for-syntax printing? #t)
-
 (define-syntax-rule (defprinter t ...)
   (begin
     (define t (box (lambda _ (error (format "~a not yet defined" 't))))) ...
@@ -147,16 +145,14 @@ at least theoretically.
       (pretty-print (print-convert s))
       (newline))))
 
-(define custom-printer (make-parameter #t))
+(define custom-printer (make-parameter #f))
   
 (define-syntax (define-struct/printer stx)
   (syntax-parse stx
     [(form name (flds ...) printer:expr)
      #`(define-struct name (flds ...) 
          #:property prop:custom-write 
-         #,(if printing? 
-               #'(lambda (a b c) (if (custom-printer) (printer a b c) (pseudo-printer a b c)))
-               #'pseudo-printer)
+         (lambda (a b c) (if (custom-printer) (printer a b c) (pseudo-printer a b c)))
          #:inspector #f)]))