diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 0076bd5f..6cf257f6 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 807f5e2d..736ad62d 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/parse-type.ss b/collects/typed-scheme/private/parse-type.ss
index f1999a76..cbc5632b 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/type-annotation.ss b/collects/typed-scheme/private/type-annotation.ss
index 2886db75..a30d4ff0 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 a97453ab..1746342b 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)])