diff --git a/collects/tests/typed-scheme/succeed/opt-arg-test.rkt b/collects/tests/typed-scheme/succeed/opt-arg-test.rkt
new file mode 100644
index 00000000..6dea2a1c
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/opt-arg-test.rkt
@@ -0,0 +1,18 @@
+#lang typed/racket
+
+(: f (case-> (-> Integer)
+             (Integer -> Integer)))
+(define (f [#{z : Integer} 0]) z)
+#;
+(define-values
+  (f)
+  (let-values (((#{core3 : (case-> (Integer True -> Integer)
+                                   (Univ False -> Integer))})
+                (lambda (z1 z2) (let-values (((#{z : Integer}) (if z2 z1 '0)))
+                                  (let-values () z)))))
+    (case-lambda (() (#%app core3 '#f '#f)) 
+                 ((z1) (#%app core3 z1 '#t)))))
+
+
+(add1 (f 0))
+(add1 (f))
\ No newline at end of file
diff --git a/collects/typed-scheme/private/type-annotation.rkt b/collects/typed-scheme/private/type-annotation.rkt
index b642589e..198d3165 100644
--- a/collects/typed-scheme/private/type-annotation.rkt
+++ b/collects/typed-scheme/private/type-annotation.rkt
@@ -104,6 +104,7 @@
       ([current-orig-stx stx])
     (cond
       [(type-annotation stx #:infer infer)]
+      [(procedure? default) (default)]
       [default default]
       [(not (syntax-original? stx))
        (tc-error "insufficient type information to typecheck. please add more type annotations")]
diff --git a/collects/typed-scheme/tc-setup.rkt b/collects/typed-scheme/tc-setup.rkt
index e8dd1060..a52f9a13 100644
--- a/collects/typed-scheme/tc-setup.rkt
+++ b/collects/typed-scheme/tc-setup.rkt
@@ -46,7 +46,7 @@
                      ;; do we report multiple errors
                      [delay-errors? #t]
                      ;; do we print the fully-expanded syntax?
-                     [print-syntax? #f]
+                     [print-syntax? #t]
                      ;; this parameter is just for printing types
                      ;; this is a parameter to avoid dependency issues
                      [current-type-names
diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.rkt b/collects/typed-scheme/typecheck/tc-lambda-unit.rkt
index f3dafeba..07fac85c 100644
--- a/collects/typed-scheme/typecheck/tc-lambda-unit.rkt
+++ b/collects/typed-scheme/typecheck/tc-lambda-unit.rkt
@@ -4,8 +4,8 @@
          "signatures.rkt"
          "tc-metafunctions.rkt"
          "tc-subst.rkt" "check-below.rkt"
-         mzlib/trace
-         scheme/list
+         mzlib/trace racket/dict
+         scheme/list syntax/parse "parse-cl.rkt"
          racket/syntax unstable/struct syntax/stx
          (rename-in scheme/contract [-> -->] [->* -->*] [one-of/c -one-of/c])
          (except-in (rep type-rep) make-arr)
@@ -119,18 +119,46 @@
 
 ;; syntax-list[id] block -> lam-result
 (define (tc/lambda-clause args body)
+  (define-values (aux-table flag-table)
+    (syntax-parse body
+      [(b:rebuild-let*) (values (attribute b.mapping) (attribute b.flag-mapping))]
+      [_ (values #hash() #hash())]))
+  ;(printf "body: ~a\n" body)
   (syntax-case args ()
     [(args ...)
      (let* ([arg-list (syntax->list #'(args ...))]
-            [arg-types (get-types arg-list #:default Univ)])
-       (with-lexical-env/extend
-        arg-list arg-types
-        (make lam-result
-              (map list arg-list arg-types)
-              null
-              #f
-              #f
-              (tc-exprs (syntax->list body)))))]
+            [arg-types (for/list ([a arg-list]) 
+                         (get-type a #:default (lambda () 
+                                                 #;(printf "got to here ~a ~a ~a\n~a ~a\n" 
+                                                         (syntax-e a) (syntax-e (dict-ref aux-table a #'no)) (dict-ref aux-table a #'no)
+                                                         aux-table (dict-keys aux-table))
+                                                 (get-type (dict-ref aux-table a #'no) #:default Univ))))])
+       (define new-arg-types
+         (if (= 0 (dict-count flag-table))
+             (list arg-types)
+             (apply append
+                    (for/list ([(k v) (in-dict flag-table)])
+                      (list
+                       (for/list ([i arg-list]
+                                  [t arg-types])
+                         (cond [(free-identifier=? i k) t]
+                               [(free-identifier=? i v) (-val #t)]
+                               [else t]))
+                       (for/list ([i arg-list]
+                                  [t arg-types])
+                         (cond [(free-identifier=? i k) (-val #f)]
+                               [(free-identifier=? i v) (-val #f)]
+                               [else t])))))))
+       #;(printf "nat: ~a\n" new-arg-types)
+       (for/list ([arg-types (in-list new-arg-types)])
+         (with-lexical-env/extend
+          arg-list arg-types
+          (make lam-result
+                (map list arg-list arg-types)
+                null
+                #f
+                #f
+                (tc-exprs (syntax->list body))))))]
     [(args ... . rest)
      (let* ([arg-list (syntax->list #'(args ...))]
             [arg-types (get-types arg-list #:default Univ)])
@@ -147,23 +175,24 @@
               (with-lexical-env/extend
                (cons #'rest arg-list)
                (cons (make-ListDots rest-type bound) arg-types)
-               (make-lam-result
-                (map list arg-list arg-types)
-                null
-                #f
-                (cons #'rest (cons rest-type bound))
-                (tc-exprs (syntax->list body))))))]
+               (list (make lam-result
+                           (map list arg-list arg-types)
+                           null
+                           #f
+                           (cons #'rest (cons rest-type bound))
+                           (tc-exprs (syntax->list body)))))))]
          [else
           (let ([rest-type (get-type #'rest #:default Univ)])
             (with-lexical-env/extend
              (cons #'rest arg-list)
              (cons (make-Listof rest-type) arg-types)
-             (make-lam-result
-                   (map list arg-list arg-types)
-                   null
-                   (list #'rest rest-type)
-                   #f
-                   (tc-exprs (syntax->list body)))))]))]))
+             (list
+              (make lam-result
+                    (map list arg-list arg-types)
+                    null
+                    (list #'rest rest-type)
+                    #f
+                    (tc-exprs (syntax->list body))))))]))]))
 
 (define (formals->list l)
   (let loop ([l (syntax-e l)])
@@ -217,7 +246,7 @@
                        (tc-error/expr #:return (list (lam-result null null (list #'here Univ) #f (ret (Un))))
                                       "Expected a function of type ~a, but got a function with the wrong arity"
                                       (match expected [(tc-result1: t) t]))
-                       (list (tc/lambda-clause f* b*)))]
+                       (tc/lambda-clause f* b*))]
                   [(list (arr: argss rets rests drests '()) ...) 
                    (for/list ([args argss] [ret rets] [rest rests] [drest drests])
                      (tc/lambda-clause/check