diff --git a/collects/tests/typed-scheme/fail/dup-ann.rkt b/collects/tests/typed-scheme/fail/dup-ann.rkt
new file mode 100644
index 0000000000..0633266d61
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/dup-ann.rkt
@@ -0,0 +1,18 @@
+#;
+(exn-pred 4)
+#lang typed/racket
+(: bar : (String -> String))
+(: bar : (Number -> Number))
+(define (bar x)
+  (+ x 1))
+
+
+(define: (foo) : Number
+  (: bar : (Number -> Number))
+  (define: (bar [x : Number]) : Number
+    (+ x 1))
+  (bar 5))
+
+
+(: baz Number)
+(define: baz : Number 7)
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/fail/internal-ann.rkt b/collects/tests/typed-scheme/fail/internal-ann.rkt
new file mode 100644
index 0000000000..f38852fd2d
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/internal-ann.rkt
@@ -0,0 +1,8 @@
+
+#lang typed/scheme/base
+
+(define (f x)
+ (: g (Integer -> Integer))
+ (define (g x)
+   (+ x 2))
+ (g x))
diff --git a/collects/tests/typed-scheme/xfail/cl-expected.rkt b/collects/tests/typed-scheme/xfail/cl-expected.rkt
new file mode 100644
index 0000000000..23462c59d4
--- /dev/null
+++ b/collects/tests/typed-scheme/xfail/cl-expected.rkt
@@ -0,0 +1,8 @@
+#lang typed/scheme
+
+
+(: add (case-lambda (Integer -> Integer) (Integer Integer -> Integer)))
+(define add
+  (case-lambda
+    [(x) (add x 0)]
+    [(x y) (+ x y)]))
\ No newline at end of file
diff --git a/collects/typed-scheme/env/type-env.rkt b/collects/typed-scheme/env/type-env.rkt
index 300220b874..0cb028b854 100644
--- a/collects/typed-scheme/env/type-env.rkt
+++ b/collects/typed-scheme/env/type-env.rkt
@@ -26,16 +26,19 @@
   (free-id-table-set! the-mapping id type))
 
 (define (register-type-if-undefined id type)
-  (if (free-id-table-ref the-mapping id (lambda _ #f))
-      (tc-error/stx id "Duplicate type annotation for ~a" (syntax-e id))
-      (register-type id type)))
+  (cond [(free-id-table-ref the-mapping id (lambda _ #f))
+         => (lambda (e)
+              (tc-error/expr #:stx id "Duplicate type annotation for ~a" (syntax-e id))
+              (when (box? e)
+                (free-id-table-set! the-mapping id (unbox e))))]
+        [else (register-type id type)]))
 
 ;; add a single type to the mapping
 ;; identifier type -> void
 (define (register-type/undefined id type)
   ;(printf "register-type/undef ~a~n" (syntax-e id))
   (if (free-id-table-ref the-mapping id (lambda _ #f))
-      (tc-error/stx id "Duplicate type annotation for ~a" (syntax-e id))
+      (void (tc-error/expr #:stx id "Duplicate type annotation for ~a" (syntax-e id)))
       (free-id-table-set! the-mapping id (box type))))
 
 ;; add a bunch of types to the mapping
@@ -61,7 +64,8 @@
 
 (define (finish-register-type id)
   (unless (maybe-finish-register-type id)
-    (tc-error/stx id "Duplicate defintion for ~a" (syntax-e id))))
+    (tc-error/expr #:stx id "Duplicate defintion for ~a" (syntax-e id)))
+  (void))
 
 (define (check-all-registered-types)
   (free-id-table-for-each 
@@ -69,11 +73,13 @@
    (lambda (id e) 
      (when (box? e) 
        (let ([bnd (identifier-binding id)])
-         (tc-error/stx id "Declaration for ~a provided, but ~a ~a" 
-                       (syntax-e id) (syntax-e id)
-                       (cond [(eq? bnd 'lexical) "is a lexical binding"] ;; should never happen
-                             [(not bnd) "has no definition"] 
-                             [else "is defined in another module"])))))))
+         (tc-error/expr #:stx id
+                        "Declaration for ~a provided, but ~a ~a" 
+                        (syntax-e id) (syntax-e id)
+                        (cond [(eq? bnd 'lexical) "is a lexical binding"] ;; should never happen
+                              [(not bnd) "has no definition"] 
+                              [else "is defined in another module"]))))
+     (void))))
 
 ;; map over the-mapping, producing a list
 ;; (id type -> T) -> listof[T]  
diff --git a/collects/typed-scheme/private/type-annotation.rkt b/collects/typed-scheme/private/type-annotation.rkt
index b459c837a9..7109f5dd42 100644
--- a/collects/typed-scheme/private/type-annotation.rkt
+++ b/collects/typed-scheme/private/type-annotation.rkt
@@ -37,7 +37,11 @@
 ;; is let-binding really necessary? - remember to record the bugs!
 (define (type-annotation stx #:infer [let-binding #f])
   (define (pt prop)
-    #;(print-size prop)
+    (when (and (identifier? stx) 
+               let-binding
+               (lookup-type stx (lambda () #f)))
+      (maybe-finish-register-type stx)
+      (tc-error/expr #:stx stx "Duplicate type annotation for ~a" (syntax-e stx)))
     (if (syntax? prop)
         (parse-type prop)
         (parse-type/id stx prop)))
@@ -92,14 +96,14 @@
 ;; get the type annotation of this identifier, otherwise error
 ;; if #:default is provided, return that instead of error
 ;; identifier #:default Type -> Type
-(define (get-type stx #:default [default #f])
+(define (get-type stx #:default [default #f] #:infer [infer #t])
   (parameterize
       ([current-orig-stx stx])
     (cond
-      [(type-annotation stx #:infer #t)]
+      [(type-annotation stx #:infer infer)]
       [default default]
       [(not (syntax-original? stx))
-       (tc-error "untyped var: ~a" (syntax-e stx))]
+       (tc-error "untyped variable: ~a" (syntax-e stx))]
       [else
        (tc-error "no type information on variable ~a" (syntax-e stx))])))
 
diff --git a/collects/typed-scheme/typecheck/tc-let-unit.rkt b/collects/typed-scheme/typecheck/tc-let-unit.rkt
index d27568b4bb..1569f46c8d 100644
--- a/collects/typed-scheme/typecheck/tc-let-unit.rkt
+++ b/collects/typed-scheme/typecheck/tc-let-unit.rkt
@@ -108,7 +108,7 @@
                   [(begin (quote-syntax (define-type-alias-internal nm ty)) (#%plain-app values))
                    (register-resolved-type-alias #'nm (parse-type #'ty))]
                   [(begin (quote-syntax (:-internal nm ty)) (#%plain-app values))
-                   (register-type/undefined #'nm (parse-type #'ty))]
+                   (register-type-if-undefined #'nm (parse-type #'ty))]
                   [_ (void)]))
               names
               exprs)
diff --git a/collects/typed-scheme/typecheck/tc-toplevel.rkt b/collects/typed-scheme/typecheck/tc-toplevel.rkt
index 169f118ed9..b0e025346d 100644
--- a/collects/typed-scheme/typecheck/tc-toplevel.rkt
+++ b/collects/typed-scheme/typecheck/tc-toplevel.rkt
@@ -3,7 +3,7 @@
 
 (require (rename-in "../utils/utils.rkt" [infer r:infer]))
 (require syntax/kerncase
-	 unstable/list unstable/syntax syntax/parse
+	 unstable/list unstable/syntax syntax/parse unstable/debug
          mzlib/etc
          scheme/match
          "signatures.rkt"
@@ -14,7 +14,7 @@
          (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
+	 unstable/mutated-vars syntax/id-table
          (utils tc-utils)
          "provide-handling.rkt"
          "def-binding.rkt"
@@ -27,6 +27,8 @@
 (import tc-expr^ check-subforms^)
 (export typechecker^)
 
+(define unann-defs (make-free-id-table))
+
 (define (tc-toplevel/pass1 form)
   ;(printf "form-top: ~a~n" form)
   ;; first, find the mutated variables:
@@ -115,7 +117,7 @@
          (cond
            ;; if all the variables have types, we stick them into the environment
            [(andmap (lambda (s) (syntax-property s 'type-label)) vars)        
-            (let ([ts (map get-type vars)])
+            (let ([ts (map (λ (x) (get-type x #:infer #f)) vars)])
               (for-each register-type-if-undefined vars ts)
               (map make-def-binding vars ts))]
            ;; if this already had an annotation, we just construct the binding reps
@@ -123,16 +125,13 @@
             (for-each finish-register-type vars)
             (map (lambda (s) (make-def-binding s (lookup-type s))) vars)]
            ;; special case to infer types for top level defines - should handle the multiple values case here
-           [(and (= 1 (length vars)) 
-                 (with-handlers ([exn:fail? (lambda _ #f)])
-                   (save-errors!)
-                   (begin0 (tc-expr #'expr)
-                           (restore-errors!))))
-            => (match-lambda 
-                 [(tc-result1: t)
-                  (register-type (car vars) t)
-                  (list (make-def-binding (car vars) t))]
-                 [t (int-err "~a is not a tc-result" t)])]
+           [(= 1 (length vars))
+            (match (tc-expr #'expr)
+              [(tc-result1: t)
+               (register-type (car vars) t)
+               (free-id-table-set! unann-defs (car vars) #t)
+               (list (make-def-binding (car vars) t))]
+              [t (int-err "~a is not a tc-result" t)])]
            [else
             (tc-error "Untyped definition : ~a" (map syntax-e vars))]))]
       
@@ -186,10 +185,12 @@
       
       ;; definitions just need to typecheck their bodies
       [(define-values (var ...) expr)
-       (begin (let* ([vars (syntax->list #'(var ...))]
-                     [ts (map lookup-type vars)])
-                (tc-expr/check #'expr (ret ts)))
-              (void))]
+       (let* ([vars (syntax->list #'(var ...))]
+              [ts (map lookup-type vars)])
+         (unless (for/and ([v (syntax->list #'(var ...))])
+                   (free-id-table-ref unann-defs v (lambda _ #f)))
+           (tc-expr/check #'expr (ret ts)))
+         (void))]
       
       ;; to handle the top-level, we have to recur into begins
       [(begin) (void)]