diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.ss b/collects/typed-scheme/typecheck/tc-lambda-unit.ss
index 3fb1baae4e..aaceea3d68 100644
--- a/collects/typed-scheme/typecheck/tc-lambda-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-lambda-unit.ss
@@ -209,7 +209,7 @@
 (define (tc/mono-lambda/type formals bodies expected)
   (define t (make-Function (map lam-result->type (tc/mono-lambda formals bodies expected))))
   (if expected 
-      (check-below t expected)
+      (and (check-below (ret t true-filter) expected) t)
       t))
 
 ;; tc/plambda syntax syntax-list syntax-list type -> Poly
diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss
index 1a1d17c22a..bda76ab6c1 100644
--- a/collects/typed-scheme/typecheck/tc-metafunctions.ss
+++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss
@@ -149,9 +149,15 @@
     [(ValuesDots: (list (Result: ts lfs los) ...) dty dbound)
      (ret ts
           (for/list ([lf lfs]) 
-            (merge-filter-sets
-             (for/list ([x formals] [i (in-naturals)])
-               (apply-filter (split-lfilters lf i) Univ (make-Path null x)))))
+            (or
+             (and (null? formals)
+                  (match lf
+                    [(LFilterSet: lf+ lf-)
+                     (combine (if (memq (make-LBot) lf+) (list (make-Bot)) (list))
+                              (if (memq (make-LBot) lf-) (list (make-Bot)) (list)))]))
+             (merge-filter-sets
+              (for/list ([x formals] [i (in-naturals)])
+                (apply-filter (split-lfilters lf i) Univ (make-Path null x))))))
           (for/list ([lo los])
             (or 
              (for/or ([x formals] [i (in-naturals)])
@@ -163,9 +169,15 @@
     [(Values: (list (Result: ts lfs los) ...))
      (ret ts
           (for/list ([lf lfs]) 
-            (merge-filter-sets
-             (for/list ([x formals] [i (in-naturals)])
-               (apply-filter (split-lfilters lf i) Univ (make-Path null x)))))
+            (or
+             (and (null? formals)
+                  (match lf
+                    [(LFilterSet: lf+ lf-)
+                     (combine (if (memq (make-LBot) lf+) (list (make-Bot)) (list))
+                              (if (memq (make-LBot) lf-) (list (make-Bot)) (list)))]))
+             (merge-filter-sets
+              (for/list ([x formals] [i (in-naturals)])
+                (apply-filter (split-lfilters lf i) Univ (make-Path null x))))))
           (for/list ([lo los])
             (or 
              (for/or ([x formals] [i (in-naturals)])
diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss
index 2a768e0fb0..6f4504c392 100644
--- a/collects/typed-scheme/types/utils.ss
+++ b/collects/typed-scheme/types/utils.ss
@@ -290,7 +290,7 @@
 (define (lookup-fail e) 
   (match (identifier-binding e)
     ['lexical (int-err "untyped lexical variable ~a" (syntax-e e))]
-    [#f (int-err "untyped top-level variable ~a" (syntax-e e))]
+    [#f (tc-error/expr "untyped top-level identifier ~a" (syntax-e e))]
     [(list _ _ nominal-source-mod nominal-source-id _ _ _)
      (let-values ([(x y) (module-path-index-split nominal-source-mod)])
        (cond [(and (not x) (not y))