diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 0076bd5f99..6cf257f6e1 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -52,7 +52,7 @@
         [make-lst/elements -pair])
     (make-env
      
-     [string->sexpr (-> -String (-mu x (Un Sym -String N B (-lst x))))]
+     [raise (Univ . -> . (Un))]
      
      (car (make-Poly (list 'a 'b) (cl-> [((-pair (-v a) (-v b))) (-v a)]
                                         [((make-lst (-v a))) (-v a)])))
@@ -95,8 +95,12 @@
      (number? (make-pred-ty N))
      (integer? (make-pred-ty -Integer))
      (boolean? (make-pred-ty B))
-     (add1 (-> N N))
-     (sub1 (-> N N))
+     (add1 (cl->*
+            #;(-> -Integer -Integer)
+            (-> N N)))
+     (sub1 (cl->*
+            #;(-> -Integer -Integer)
+            (-> N N)))
      (eq? (-> Univ Univ B))
      (eqv? (-> Univ Univ B))
      (equal? (-> Univ Univ B))
@@ -179,10 +183,10 @@
      (<= (->* (list N N) N B))
      [> (->* (list N) N B)]
      (zero? (N . -> . B))
-     (* (->* '() N N))
-     (/ (->* (list N) N N))
-     (+ (->* '() N N))
-     (- (->* (list N) N N))
+     (* (cl->* (->* '() -Integer -Integer) (->* '() N N)))
+     (/ (cl->* (->* (list N) N N)))
+     (+ (cl->* (->* '() -Integer -Integer) (->* '() N N)))
+     (- (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N)))
      (max (->* (list N) N N))
      (min (->* (list N) N N))
      [values  (make-Poly '(a) (-> (-v a) (-v a)))]
@@ -463,8 +467,8 @@
      
      [make-directory (-> -Path -Void)]
      
-     [hash-table-for-each (-poly (a b c)
-                                 (-> (-HT a b) (-> a b c) -Void))]
+     [hash-for-each (-poly (a b c)
+                           (-> (-HT a b) (-> a b c) -Void))]
      
      [delete-file (-> -Pathlike -Void)]
      [make-namespace (cl->* (-> -Namespace)
diff --git a/collects/typed-scheme/private/base-types.ss b/collects/typed-scheme/private/base-types.ss
index 807f5e2da8..736ad62d35 100644
--- a/collects/typed-scheme/private/base-types.ss
+++ b/collects/typed-scheme/private/base-types.ss
@@ -95,7 +95,7 @@
   [HashTable (-poly (a b) (-HT a b))]
   [Promise (-poly (a) (-Promise a))]
   [Pair (-poly (a b) (-pair a b))]
-  [Box (-poly (a) (make-Box a))]
+  [Boxof (-poly (a) (make-Box a))]
   [Syntax Any-Syntax]
   [Identifier Ident]
   )
diff --git a/collects/typed-scheme/private/infer-ops.ss b/collects/typed-scheme/private/infer-ops.ss
index 17590cf259..25554c0d11 100644
--- a/collects/typed-scheme/private/infer-ops.ss
+++ b/collects/typed-scheme/private/infer-ops.ss
@@ -139,6 +139,11 @@
       (unless (= (length l1) (length l2))
         (unmatch))
       (cgen-union V X l1 l2)]
+     #;
+     [((Poly-unsafe: n b) (Poly-unsafe: n* b*))
+      (unless (= n n*)
+        (fail! S T))
+      (cgen V X b b*)]
      
      
      [((Union: es) S) (cset-meet* X (for/list ([e es]) (cgen V X e S)))]
diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss
index f1999a76ae..cbc5632bd0 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -114,7 +114,10 @@
               [tvar (make-F var)])
          (add-type-name-reference #'mu)           
          (parameterize ([current-tvars (extend-env (list var) (list tvar) (current-tvars))])
-           (make-Mu var (parse-type #'t))))]
+           (let ([t (parse-type #'t)])
+             (if (memq var (fv t))
+                 (make-Mu var t)
+                 t))))]
       [(U ts ...)
        (eq? (syntax-e #'U) 'U)
        (begin
diff --git a/collects/typed-scheme/private/syntax-traversal.ss b/collects/typed-scheme/private/syntax-traversal.ss
index 6b5c7c50a8..9bc373a904 100644
--- a/collects/typed-scheme/private/syntax-traversal.ss
+++ b/collects/typed-scheme/private/syntax-traversal.ss
@@ -41,15 +41,18 @@
 (define (look-for-in-orig orig expanded lookfor)
   (define src (syntax-source orig))
   ;; we just might get a lookfor that is already in the original
-  (if (syntax-original? lookfor)
-    lookfor
-    (let ([enclosing (enclosing-syntaxes-with-source expanded lookfor src)]
-          [syntax-locs (make-hash)])
-      ;; find all syntax locations in original code
-      (let loop ([stx orig])
-        (when (syntax? stx) (hash-set! syntax-locs (syntax-loc stx) stx))
-        (let ([stx (if (syntax? stx) (syntax-e stx) stx)])
-          (when (pair? stx) (loop (car stx)) (loop (cdr stx)))))
+   (let ([enclosing (enclosing-syntaxes-with-source expanded lookfor src)]
+         [syntax-locs (make-hash)])
+     ;; find all syntax locations in original code
+     (let loop ([stx orig])
+       (when (syntax? stx) (hash-set! syntax-locs (syntax-loc stx) stx))
+       (let ([stx (if (syntax? stx) (syntax-e stx) stx)])
+         (when (pair? stx) (loop (car stx)) (loop (cdr stx)))))
+     (or
+      ;; we just might get a lookfor that is already in the original
+      (and (eq? src (syntax-source lookfor))
+           (hash-ref syntax-locs (syntax-loc lookfor) #f))
+           
       ;; look for some enclosing expression
       (and enclosing
            (ormap (lambda (enc) (hash-ref syntax-locs (syntax-loc enc) #f))
diff --git a/collects/typed-scheme/private/tc-app-unit.ss b/collects/typed-scheme/private/tc-app-unit.ss
index 425c5067e8..f9f3e2d737 100644
--- a/collects/typed-scheme/private/tc-app-unit.ss
+++ b/collects/typed-scheme/private/tc-app-unit.ss
@@ -248,7 +248,7 @@
                                        "Polymorphic function could not be applied to arguments:~nExpected: ~a ~nActual: ~a" 
                                        (car msg-doms) argtypes)
                         (tc-error/expr #:return (ret (Un))
-                                       "no polymorphic function domain matched - possible domains were: ~n~a~narguments: were ~n~a"
+                                       "no polymorphic function domain matched - possible domains were: ~n~a~narguments were: ~n~a"
                                        (stringify (map stringify msg-doms) "\n") (stringify argtypes))))]
                  [(and (= (length (car doms*))
                           (length argtypes))
@@ -322,20 +322,25 @@
     (kernel-syntax-case* b #f (reverse)
       [[(v) (#%plain-app reverse n)]
        (free-identifier=? name #'n)
-       (type-annotation #'v)]
+       (begin ;(printf "found annotation: ~a ~a~n~a~n" (syntax-e name) (syntax-e #'v) (type-annotation #'v))
+              (type-annotation #'v))]
       [_ #f]))
   (kernel-syntax-case* 
-   stx #f (reverse)
-   [(let-values (binding ...) body)
-    (cond [(ormap match? (syntax->list #'(binding ...)))]
-          [else (find #'body)])]
-   [(#%plain-app e ...) (ormap find (syntax->list #'(e ...)))]
-   [(if e1 e2 e3) (ormap find (syntax->list #'(e1 e2 e3)))]
-   [(letrec-values ([(v ...) e] ...) b)
-    (ormap find (syntax->list #'(e ... b)))]
-   [(#%plain-lambda (v ...) e)
-    (find #'e)]
-   [_ #f]))
+      stx #f (reverse letrec-syntaxes+values)
+    [(let-values (binding ...) body)
+     (cond [(ormap match? (syntax->list #'(binding ...)))]
+           [else (find #'body)])]
+    [(#%plain-app e ...) (ormap find (syntax->list #'(e ...)))]
+    [(if e1 e2 e3) (ormap find (syntax->list #'(e1 e2 e3)))]
+    [(letrec-values ([(v ...) e] ...) b)
+     (ormap find (syntax->list #'(e ... b)))]
+    [(letrec-syntaxes+values _ ([(v ...) e] ...) b)
+     (ormap find (syntax->list #'(e ... b)))]
+    [(begin . es)
+     (ormap find (syntax->list #'es))]
+    [(#%plain-lambda (v ...) e)
+     (find #'e)]
+    [_ #f]))
 
 (define (matches? stx)
   (let loop ([stx stx] [ress null] [acc*s null])
@@ -449,7 +454,7 @@
           ;(printf "got here 1~n")
           (not (andmap type-annotation (syntax->list #'(val acc ...))))
           (free-identifier=? #'val #'val*)
-          (andmap (lambda (a) (find-annotation #'(if (#%plain-app null? val*) thn els) a))
+          (ormap (lambda (a) (find-annotation #'(if (#%plain-app null? val*) thn els) a))
                   (syntax->list #'(acc ...)))
           ;(printf "got here 2~n")
           #;
@@ -462,11 +467,12 @@
             [_ #f]))
      (let* ([ts1 (tc-expr/t #'actual)]
             [ts1 (generalize ts1)]
-            [ann-ts (map (lambda (a) (find-annotation #'(if (#%plain-app null? val*) thn els) a)) 
-                         (syntax->list #'(acc ...)))]
-            [ts (cons ts1 ann-ts)])                 
-       ;(printf "doing match case actuals:~a ann-ts: ~a~n" 
-       ;           (syntax->datum #'(actuals ...)) ann-ts)
+            [ann-ts (map (lambda (a ac) (or (find-annotation #'(if (#%plain-app null? val*) thn els) a)
+                                            (generalize (tc-expr/t ac))))
+                         (syntax->list #'(acc ...))
+                         (syntax->list #'(actuals ...)))]
+            [ts (cons ts1 ann-ts)]) 
+       ;(printf "doing match case actuals:~a ann-ts: ~a~n" (syntax->datum #'(actuals ...)) ann-ts)
        ;; check that the actual arguments are ok here
        (map tc-expr/check (syntax->list #'(actuals ...)) ann-ts)
        ;(printf "done here ts = ~a~n" ts)
@@ -487,7 +493,7 @@
           ;(printf "special case 1~n")
           (not (andmap type-annotation (syntax->list #'(args ...))))
           (free-identifier=? #'lp #'lp*))
-     (let ([ts (map tc-expr/t (syntax->list #'actuals))])
+     (let ([ts (map (compose generalize tc-expr/t) (syntax->list #'actuals))])
        ;(printf "special case~n")
        (tc/rec-lambda/check form #'(args ...) #'body #'lp ts expected)
        (ret expected))]
diff --git a/collects/typed-scheme/private/tc-lambda-unit.ss b/collects/typed-scheme/private/tc-lambda-unit.ss
index cae44244c2..37237604a3 100644
--- a/collects/typed-scheme/private/tc-lambda-unit.ss
+++ b/collects/typed-scheme/private/tc-lambda-unit.ss
@@ -77,9 +77,13 @@
                  [else (make-arr arg-types t)])]
               [t (int-err "bad match - not a tc-result: ~a" t)]))))]
     [(args* ... . rest)
-     (let ([t (tc/lambda-clause args body)])               
-       (check-below (make-Function (list t)) (make-Function (list (make-arr arg-tys ret-ty rest-ty))))
-       t)]))
+     (begin
+       (unless rest-ty
+         (tc-error "Expected function with ~a arguments and no rest argument,~nbut got function with ~a arguments and a rest argument"
+                   (length arg-tys) (length (syntax->list #'(args* ...)))))
+       (with-lexical-env/extend
+        (list #'rest) (list (-lst rest-ty))
+        (tc/lambda-clause/check #'(args* ...) body arg-tys ret-ty #f)))]))
 
 ;; syntax-list[id] block -> arr
 (define (tc/lambda-clause args body)
@@ -129,7 +133,8 @@
         (match expected          
           [(Mu: _ _) (loop (unfold expected))]
           [(Function: (list (arr: args ret rest _ _))) 
-           (tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args ret rest)]
+           (tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args ret rest)
+           expected]
           [t (let ([t (tc/mono-lambda formals bodies #f)])
                (check-below t expected))]))
       (let loop ([formals (syntax->list formals)] 
@@ -168,16 +173,15 @@
 (define (tc/plambda form formals bodies expected)
   (match expected
     [(Poly-names: ns (and expected* (Function: _)))
-     (with-syntax ()
-       (let* ([tvars (let ([p (syntax-property form 'typechecker:plambda)])
-                       (or (and p (map syntax-e (syntax->list p)))
-                           ns))]
-              [literal-tvars tvars]
-              [new-tvars (map make-F literal-tvars)]
-              [ty (parameterize ([current-tvars (extend-env literal-tvars new-tvars (current-tvars))])
-                    (tc/mono-lambda formals bodies expected*))])
-         ;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty)
-         (ret (make-Poly literal-tvars ty))))]
+      (let* ([tvars (let ([p (syntax-property form 'typechecker:plambda)])
+                      (or (and p (map syntax-e (syntax->list p)))
+                          ns))]
+             [literal-tvars tvars]
+             [new-tvars (map make-F literal-tvars)]
+             [ty (parameterize ([current-tvars (extend-env literal-tvars new-tvars (current-tvars))])
+                   (tc/mono-lambda formals bodies expected*))])
+        ;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty)
+        (ret (make-Poly literal-tvars ty)))]
     [_ (tc-error/expr #:return expected "Expected a value of type ~a, but got a polymorphic function." expected)]))
     
 
diff --git a/collects/typed-scheme/private/tc-let-unit.ss b/collects/typed-scheme/private/tc-let-unit.ss
index 49dd91772f..aec3ad4175 100644
--- a/collects/typed-scheme/private/tc-let-unit.ss
+++ b/collects/typed-scheme/private/tc-let-unit.ss
@@ -8,8 +8,10 @@
          "type-env.ss"
          "parse-type.ss"
          "utils.ss"
+         "type-utils.ss"
          syntax/free-vars
          mzlib/trace
+         scheme/match
          syntax/kerncase
          (for-template 
           scheme/base
@@ -30,7 +32,7 @@
    namess
    ;; the types
    types
-   (for-each (lambda (stx e t) (check-type stx (expr->type e) t))
+   (for-each expr->type
              clauses
              exprs 
              (map list->values-ty types))
@@ -65,10 +67,24 @@
 (define (tc/letrec-values namess exprs body form)
   (tc/letrec-values/internal namess exprs body form #f))
 
+(define (tc-expr/maybe-expected/t e name)
+  (define expecteds
+    (map (lambda (stx) (lookup-type stx (lambda () #f))) name))
+  (define mk (if (and (pair? expecteds) (null? (cdr expecteds)))
+                 car
+                 -values))
+  (define tcr
+    (if
+     (andmap values expecteds)
+     (tc-expr/check e (mk expecteds))
+     (tc-expr e)))
+  (match tcr
+    [(tc-result: t) t]))
+
 (define (tc/letrec-values/internal namess exprs body form expected)
   (let* ([names (map syntax->list (syntax->list namess))]
          [flat-names (apply append names)]
-         [exprs (syntax->list exprs)]           
+         [exprs (syntax->list exprs)]
          ;; the clauses for error reporting
          [clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])])
     (for-each (lambda (names body)
@@ -88,14 +104,28 @@
         ;; if none of the names bound in the letrec are free vars of this rhs
         [(not (ormap (lambda (n) (s:member n flat-names bound-identifier=?)) (free-vars (car exprs))))
          ;; then check this expression separately
-         (let ([t (tc-expr/t (car exprs))])               
+         (let ([t (tc-expr/maybe-expected/t (car exprs) (car names))])
            (with-lexical-env/extend
             (list (car names))
             (list (get-type/infer (car names) t))
             (loop (cdr names) (cdr exprs) (apply append (cdr names)) (cdr clauses))))]
         [else
          ;(for-each (lambda (vs) (for-each (lambda (v) (printf/log "Letrec Var: ~a~n" (syntax-e v))) vs)) names)
-         (do-check tc-expr/t names (map (lambda (l) (map get-type l)) names) form exprs body clauses expected)]))))
+         (do-check (lambda (stx e t)
+                     (match (tc-expr/check e t)
+                       [(tc-result: t) t]))
+                   names (map (lambda (l) (map get-type l)) names) form exprs body clauses expected)]))))
+
+;; this is so match can provide us with a syntax property to
+;; say that this binding is only called in tail position
+(define ((tc-expr-t/maybe-expected expected) e)
+  (kernel-syntax-case e #f
+    [(#%plain-lambda () _)
+     (and expected (syntax-property e 'typechecker:called-in-tail-position))
+     (begin
+       (tc-expr/check e (-> expected))
+       (-> expected))]
+    [_ (tc-expr/t e)]))
 
 (define (tc/let-values/internal namess exprs body form expected)
   (let* (;; a list of each name clause
@@ -103,12 +133,12 @@
          ;; all the trailing expressions - the ones actually bound to the names
          [exprs (syntax->list exprs)]
          ;; the types of the exprs
-         [inferred-types (map tc-expr/t exprs)]
+         [inferred-types (map (tc-expr-t/maybe-expected expected) exprs)]
          ;; the annotated types of the name (possibly using the inferred types)
          [types (map get-type/infer names inferred-types)]
          ;; the clauses for error reporting
          [clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])])
-    (do-check (lambda (x) x) names types form inferred-types body clauses expected)))
+    (do-check check-type names types form inferred-types body clauses expected)))
 
 (define (tc/let-values/check namess exprs body form expected)
   (tc/let-values/internal namess exprs body form expected))
diff --git a/collects/typed-scheme/private/tc-structs.ss b/collects/typed-scheme/private/tc-structs.ss
index e38751c88d..a79b73683c 100644
--- a/collects/typed-scheme/private/tc-structs.ss
+++ b/collects/typed-scheme/private/tc-structs.ss
@@ -92,7 +92,8 @@
                          #:type-wrapper [type-wrapper values]
                          #:mutable [setters? #f]
                          #:proc-ty [proc-ty #f]
-                         #:maker [maker #f])
+                         #:maker [maker #f]
+                         #:constructor-return [cret #f])
   (let* ([name (syntax-e nm)]
          [fld-types (append parent-field-types types)]
          [sty (make-Struct name parent fld-types proc-ty)]
@@ -101,7 +102,8 @@
     (register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters? 
                            #:wrapper wrapper
                            #:type-wrapper type-wrapper
-                           #:maker maker)))
+                           #:maker maker
+                           #:constructor-return cret)))
 
 ;; generate names, and register the approriate types give field types and structure type
 ;; optionally wrap things
@@ -109,7 +111,8 @@
 (define (register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters?
                                #:wrapper [wrapper (lambda (x) x)]
                                #:type-wrapper [type-wrapper values]
-                               #:maker [maker* #f])
+                               #:maker [maker* #f]
+                               #:constructor-return [cret #f])
   ;; create the approriate names that define-struct will bind
   (define-values (maker pred getters setters) (struct-names nm flds setters?))
   ;; the type name that is used in all the types
@@ -117,7 +120,7 @@
   ;; register the type name
   (register-type-name nm (wrapper sty))
   ;; register the various function types
-  (register-type (or maker* maker) (wrapper (->* external-fld-types name)))
+  (register-type (or maker* maker) (wrapper (->* external-fld-types (if cret cret name))))
   (register-types getters
                   (map (lambda (t) (wrapper (->* (list name) t))) external-fld-types/no-parent))
   (when setters?    
@@ -158,7 +161,7 @@
 
 ;; typecheck a non-polymophic struct and register the approriate types
 ;; tc/struct : (U identifier (list identifier identifier)) Listof[identifier] Listof[syntax] -> void
-(define (tc/struct nm/par flds tys [proc-ty #f] #:maker [maker #f])
+(define (tc/struct nm/par flds tys [proc-ty #f] #:maker [maker #f] #:constructor-return [cret #f])
   ;; get the parent info and create some types and type variables
   (define-values (nm parent-name parent name name-tvar) (parse-parent nm/par))
   ;; parse the field types, and determine if the type is recursive
@@ -172,7 +175,8 @@
   (mk/register-sty nm flds parent-name (get-parent-flds parent) types
                    ;; procedure
                    #:proc-ty proc-ty-parsed
-                   #:maker maker))
+                   #:maker maker
+		   #:constructor-return (and cret (parse-type cret))))
 
 ;; register a struct type
 ;; convenience function for built-in structs
diff --git a/collects/typed-scheme/private/tc-toplevel.ss b/collects/typed-scheme/private/tc-toplevel.ss
index 1bef6174ed..1909f9e7f1 100644
--- a/collects/typed-scheme/private/tc-toplevel.ss
+++ b/collects/typed-scheme/private/tc-toplevel.ss
@@ -39,7 +39,7 @@
   (parameterize ([current-orig-stx form])
     (kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal define-type-internal 
                                    define-typed-struct/exec-internal :-internal assert-predicate-internal
-                                   require/typed-internal values :)
+                                   require/typed-internal values)
       ;; forms that are handled in other ways
       [stx 
        (or (syntax-property form 'typechecker:ignore) 
@@ -57,8 +57,9 @@
       ;; define-typed-struct
       [(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...))) (#%plain-app values)))
        (tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)))]
-      [(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...) #:maker m)) (#%plain-app values)))
-       (tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)) #:maker #'m)]
+      [(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...) #:maker m #:constructor-return t)) 
+                                (#%plain-app values)))
+       (tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)) #:maker #'m #:constructor-return #'t)]
       ;; define-typed-struct w/ polymorphism
       [(define-values () (begin (quote-syntax (define-typed-struct-internal (vars ...) nm ([fld : ty] ...))) (#%plain-app values)))
        (tc/poly-struct (syntax->list #'(vars ...)) #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)))]    
@@ -75,6 +76,7 @@
       [(define-values () (begin (quote-syntax (:-internal id ty)) (#%plain-app values)))
        (identifier? #'id)
        (register-type/undefined #'id (parse-type #'ty))]
+            
       
       ;; values definitions
       [(define-values (var ...) expr)
diff --git a/collects/typed-scheme/private/type-annotation.ss b/collects/typed-scheme/private/type-annotation.ss
index 2886db757b..a30d4ff091 100644
--- a/collects/typed-scheme/private/type-annotation.ss
+++ b/collects/typed-scheme/private/type-annotation.ss
@@ -2,7 +2,8 @@
 
 (require "type-rep.ss" "parse-type.ss" "tc-utils.ss" "subtype.ss" "utils.ss" "union.ss" "resolve-type.ss"
          "type-env.ss")
-(require (lib "plt-match.ss"))
+(require (lib "plt-match.ss")
+         mzlib/trace)
 (provide type-annotation
          get-type
          get-type/infer
@@ -67,7 +68,7 @@
       [(type-annotation stx) => (lambda (x) 
                                   (log/ann stx x)
                                   x)]
-      [(not (syntax-original? stx)) 
+      [(not (syntax-original? stx))
        (tc-error "untyped var: ~a" (syntax-e stx))]
       [else
        (tc-error "no type information on variable ~a" (syntax-e stx))])))
diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index a97453abee..1746342bec 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -217,6 +217,7 @@
   (let/ec exit
     (let loop ([t* t])
       (match t*
+        [(Value: '()) (-lst Univ)]
         [(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*]
         [(Pair: t1 t2)
          (let ([t-new (loop t2)])