diff --git a/collects/typed-scheme/env/type-env.ss b/collects/typed-scheme/env/type-env.ss
index 444aeebd73..34da01ba0d 100644
--- a/collects/typed-scheme/env/type-env.ss
+++ b/collects/typed-scheme/env/type-env.ss
@@ -3,7 +3,7 @@
 (require (except-in "../utils/utils.ss" extend))
 (require syntax/boundmap
          (utils tc-utils)
-	 (types utils))
+         (types utils))
 
 (provide register-type
          finish-register-type
diff --git a/collects/typed-scheme/env/type-environments.ss b/collects/typed-scheme/env/type-environments.ss
index 1c9bca9503..b62d7d024a 100644
--- a/collects/typed-scheme/env/type-environments.ss
+++ b/collects/typed-scheme/env/type-environments.ss
@@ -19,9 +19,6 @@
          env-keys+vals
          with-dotted-env/extend)
 
-(provide/contract [make-empty-env ((-> any/c any/c any/c) . -> . env?)]
-                  [])
-
 ;; eq? has the type of equal?, and l is an alist (with conses!)
 (define-struct env (eq? l))
 
@@ -76,7 +73,7 @@
 ;; elements are not lists, or all at once, if the elements are lists
 (define (extend/values kss vss env)
   (foldr (lambda (ks vs env) 
-           (cond [(and (list? ks) (list? vs))                                      
+           (cond [(and (list? ks) (list? vs))
                   (extend-env ks vs env)]
                  [(or (list? ks) (list? vs))
                   (int-err "not both lists in extend/values: ~a ~a" ks vs)]
@@ -87,3 +84,5 @@
 (define-syntax with-dotted-env/extend
   (syntax-rules ()
     [(_ i t v . b) (parameterize ([dotted-env (extend/values (list i) (list (cons t v)) (dotted-env))]) . b)]))
+
+(provide/contract [make-empty-env ((-> any/c any/c any/c) . -> . env?)])
diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss
index ef555e6cc6..d86e12a48d 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -300,7 +300,7 @@
        (and (eq? (syntax-e #'Refinement) 'Refinement)
             (identifier? #'p?))
        (match (lookup-type/lexical #'p?)
-              [(and t (Function: (list (arr: (list dom) rng #f #f '() _ _))))
+              [(and t (Function: (list (arr: (list dom) _ #f #f '()))))
                (make-Refinement dom #'p? (syntax-local-certifier))]
               [t (tc-error "cannot declare refinement for non-predicate ~a" t)])]
       [(Instance t)
diff --git a/collects/typed-scheme/typecheck/tc-toplevel.ss b/collects/typed-scheme/typecheck/tc-toplevel.ss
index e881e3e48a..dd771af2b8 100644
--- a/collects/typed-scheme/typecheck/tc-toplevel.ss
+++ b/collects/typed-scheme/typecheck/tc-toplevel.ss
@@ -10,9 +10,9 @@
          (rep type-rep)
          (types utils convenience)
          (private parse-type type-annotation type-contract)
-	 (env type-env init-envs type-name-env type-alias-env lexical-env)
-	 (utils tc-utils mutated-vars)
-	 "provide-handling.ss"
+         (env type-env init-envs type-name-env type-alias-env lexical-env)
+         (utils tc-utils mutated-vars)
+         "provide-handling.ss"
          "def-binding.ss"
          (for-template
           "internal-forms.ss"
@@ -41,9 +41,10 @@
        (list)]
 
       ;; declare-refinement
+      ;; FIXME - this sucks and should die
       [(define-values () (begin (quote-syntax (declare-refinement-internal pred)) (#%plain-app values)))
        (match (lookup-type/lexical #'pred)
-              [(and t (Function: (list (arr: (list dom) rng #f #f '() _ _))))
+              [(and t (Function: (list (arr: (list dom) rng #f #f '()))))
                (register-type #'pred 
                               (make-pred-ty (list dom)
                                             rng
diff --git a/collects/typed-scheme/typecheck/typechecker.ss b/collects/typed-scheme/typecheck/typechecker.ss
index bfa104fe82..524c161bb1 100644
--- a/collects/typed-scheme/typecheck/typechecker.ss
+++ b/collects/typed-scheme/typecheck/typechecker.ss
@@ -13,5 +13,5 @@
 
 (provide-signature-elements typechecker^ tc-expr^)
 
-(define-values/link-units/infer
-  tc-toplevel@ tc-new-if@ tc-lambda@ tc-dots@ tc-new-app@ tc-let@ tc-expr@ check-subforms@)
+(define-values/invoke-unit/infer
+  (link tc-toplevel@ tc-new-if@ tc-lambda@ tc-dots@ tc-new-app@ tc-let@ tc-expr@ check-subforms@))
diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss
index facbcf88ad..8d86e992b0 100644
--- a/collects/typed-scheme/types/utils.ss
+++ b/collects/typed-scheme/types/utils.ss
@@ -29,7 +29,8 @@
          (struct-out DottedBoth)
          just-Dotted?
          tc-error/expr
-         lookup-fail)
+         lookup-fail
+         lookup-type-fail)
 
 
 ;; substitute : Type Name Type -> Type
@@ -38,7 +39,7 @@
   (if (hash-ref (free-vars* target) name #f)
       (type-case (#:Type sb #:LatentFilter (sub-lf sb))
                  target
-		 [#:Union tys (Un (map sb tys))]
+                 [#:Union tys (Un (map sb tys))]
                  [#:F name* (if (eq? name* name) image target)]
                  [#:arr dom rng rest drest kws
                         (begin
@@ -83,7 +84,7 @@
                                        (map sb dom)
                                        ;; We need to recur first, just to expand out any dotted usages of this.
                                        (let ([expanded (sb (car drest))])
-					 (map (lambda (img) (substitute img name expanded)) images)))
+                                         (map (lambda (img) (substitute img name expanded)) images)))
                                       (sb rng)
                                       rimage
                                       #f
@@ -190,25 +191,25 @@
 ;; convenience function for returning the result of typechecking an expression
 (define ret
   (case-lambda [(t) 
-		(make-tc-results
-		 (if (Type? t)
-		     (list (make-tc-result t (make-FilterSet null null) (make-Empty)))
-		     (for/list ([i t])
-			       (make-tc-result i (make-FilterSet null null) (make-Empty))))
-		 #f)]
-	       [(t f)
-		(make-tc-results
-		 (if (Type? t)
-		     (list (make-tc-result t f (make-Empty)))
-		     (for/list ([i t] [f f])
-			       (make-tc-result i f (make-Empty))))
-		 #f)]
-	       [(t f o)
-		(make-tc-results
-		 (if (and (list? t) (list? f) (list? o))
-		     (map make-tc-result t f o)
-		     (list (make-tc-result t f o)))
-		 #f)]))
+                (make-tc-results
+                 (if (Type? t)
+                     (list (make-tc-result t (make-FilterSet null null) (make-Empty)))
+                     (for/list ([i t])
+                               (make-tc-result i (make-FilterSet null null) (make-Empty))))
+                 #f)]
+               [(t f)
+                (make-tc-results
+                 (if (Type? t)
+                     (list (make-tc-result t f (make-Empty)))
+                     (for/list ([i t] [f f])
+                               (make-tc-result i f (make-Empty))))
+                 #f)]
+               [(t f o)
+                (make-tc-results
+                 (if (and (list? t) (list? f) (list? o))
+                     (map make-tc-result t f o)
+                     (list (make-tc-result t f o)))
+                 #f)]))
 
 (p/c
  [ret    
@@ -254,4 +255,16 @@
   return)
 
 ;; error for unbound variables
-(define (lookup-fail e) (tc-error/expr "unbound identifier ~a" e))
+(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))]
+    [(list _ _ nominal-source-mod nominal-source-id _ _ _)
+     (let-values ([(x y) (module-path-index-split nominal-source-mod)])
+       (cond [(and (not x) (not y))
+              (tc-error/expr "untyped identifier ~a" (syntax-e e))]
+             [else 
+              (tc-error/expr "untyped identifier ~a imported from module <~a>" (syntax-e e) x)]))]))
+
+(define (lookup-type-fail i)
+  (tc-error/expr "~a is not bound as a type" (syntax-e i)))