diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss
index 8888f0b7..bb9f7b0b 100644
--- a/collects/typed-scheme/infer/infer-unit.ss
+++ b/collects/typed-scheme/infer/infer-unit.ss
@@ -471,7 +471,6 @@
 (define (infer X S T R must-vars [expected #f])
   (with-handlers ([exn:infer? (lambda _ #f)])  
     (let ([cs (cgen/list null X S T)])
-      (printf "cs: ~a~n" cs)
       (if (not expected)
           (subst-gen cs R must-vars)
           (subst-gen (cset-meet cs (cgen null X R expected)) R must-vars)))))
@@ -480,7 +479,6 @@
 (define (infer/vararg X S T T-var R must-vars [expected #f])
   (define new-T (if T-var (extend S T T-var) T))
   (and ((length S) . >= . (length T))
-       (printf "calling infer~n")
        (infer X S new-T R must-vars expected)))
 
 ;; like infer, but dotted-var is the bound on the ...
@@ -507,4 +505,4 @@
 (define (i s t r)
   (infer/simple (list s) (list t) r))
 
-(trace subst-gen cgen)
+;(trace subst-gen cgen)
diff --git a/collects/typed-scheme/infer/restrict.ss b/collects/typed-scheme/infer/restrict.ss
index 587bbe7d..d4ef3cd4 100644
--- a/collects/typed-scheme/infer/restrict.ss
+++ b/collects/typed-scheme/infer/restrict.ss
@@ -18,7 +18,6 @@
     (match l
       [(Union: es) 
        (let ([l (map f es)])
-         (printf "l is ~a~n" l)
          (apply Un l))]))
   (cond
     [(subtype t1 t2) t1] ;; already a subtype          
@@ -34,5 +33,5 @@
     [(not (overlap t1 t2)) (Un)] ;; there's no overlap, so the restriction is empty
     [else t2] ;; t2 and t1 have a complex relationship, so we punt
     ))
-(trace restrict*)
 (define restrict restrict*)
+;(trace restrict*)
diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss
index d7b175b3..aa983616 100644
--- a/collects/typed-scheme/typecheck/tc-app.ss
+++ b/collects/typed-scheme/typecheck/tc-app.ss
@@ -538,7 +538,6 @@
                           (PolyDots: vars
                                      (Function: (list (and arrs (arr: doms rngs rests (and drests #f) '())) ...))))))
       (list (tc-result1: argtys-t) ...))
-     (printf "simple poly case: ~a~n" t)
      (handle-clauses (doms rngs rests arrs) f-stx args-stx
                      ;; only try inference if the argument lengths are appropriate
                      (lambda (dom _ rest a) ((if rest <= =) (length dom) (length argtys)))
diff --git a/collects/typed-scheme/types/remove-intersect.ss b/collects/typed-scheme/types/remove-intersect.ss
index f9420703..02c77acb 100644
--- a/collects/typed-scheme/types/remove-intersect.ss
+++ b/collects/typed-scheme/types/remove-intersect.ss
@@ -63,7 +63,7 @@
          [else #t])])))
 
 
-(trace overlap)
+;(trace overlap)
 
 
 ;(trace restrict)
diff --git a/collects/typed-scheme/types/resolve.ss b/collects/typed-scheme/types/resolve.ss
index 520cc444..a558255b 100644
--- a/collects/typed-scheme/types/resolve.ss
+++ b/collects/typed-scheme/types/resolve.ss
@@ -6,24 +6,31 @@
 	 (utils tc-utils)
          (types utils)
          scheme/match
+         scheme/contract
          mzlib/trace)
 
-(provide resolve-name resolve-app needs-resolving? resolve-once resolve)
+(provide resolve-name resolve-app needs-resolving? resolve)
+(p/c [resolve-once (Type/c . -> . (or/c Type/c #f))])
 
 (define (resolve-name t)
   (match t
-    [(Name: n) (lookup-type-name n)]
+    [(Name: n) (let ([t (lookup-type-name n)])
+                 (if (Type? t) t #f))]
     [_ (int-err "resolve-name: not a name ~a" t)]))
 
 (define (resolve-app rator rands stx)
   (parameterize ([current-orig-stx stx])
     (match rator
-      [(Poly: _ _)
+      [(Poly-unsafe: n _)
+       (unless (= n (length rands))
+         (tc-error "wrong number of arguments to polymorphic type: expected ~a and got ~a"
+                   n (length rands)))
        (instantiate-poly rator rands)]
-      [(Name: _) (resolve-app (resolve-name rator) rands stx)]
+      [(Name: _) (let ([r (resolve-name rator)])
+                   (and r (resolve-app r rands stx)))]
       [(Mu: _ _) (resolve-app (unfold rator) rands)]
       [(App: r r* s) (resolve-app (resolve-app r r* s) rands)]
-      [_ (tc-error "resolve-app: not a proper operator ~a" rator)])))
+      [_ (tc-error "cannot apply a non-polymorphic type: ~a" rator)])))
 
 (define (needs-resolving? t)
   (or (Mu? t) (App? t) (Name? t)))
@@ -36,3 +43,5 @@
 
 (define (resolve t)
   (if (needs-resolving? t) (resolve-once t) t))
+
+;(trace resolve-app)
diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss
index 5a700507..26a08fe7 100644
--- a/collects/typed-scheme/types/subtype.ss
+++ b/collects/typed-scheme/types/subtype.ss
@@ -248,63 +248,22 @@
 	      [(list s (Poly: vs b))
 	       (=> unmatch)
 	       (if (null? (fv b)) (subtype* A0 s b) (unmatch))]
-	      ;; names are compared for equality:
-	      [(list (Name: n) (Name: n*))
-	       (=> unmatch)
-	       (if (free-identifier=? n n*)
-		   A0
-		   (unmatch))]
-	      ;; just unfold the recursive types
-	      [(list _ (? Mu?)) (subtype* A0 s (unfold t))]
-	      [(list (? Mu?) _) (subtype* A0 (unfold s) t)]
+	      ;; rec types, applications and names (that aren't the same
+	      [(list (? needs-resolving? s) other)
+               (let ([s* (resolve-once s)])
+                 (if (Type? s*) ;; needed in case this was a name that hasn't been resolved yet
+                     (subtype* A0 s* other)
+                     (fail! s t)))]
+	      [(list other (? needs-resolving? t))
+               (let ([t* (resolve-once t)])
+                 (if (Type? t*) ;; needed in case this was a name that hasn't been resolved yet
+                     (subtype* A0 other t*)
+                     (fail! s t)))]
 	      ;; for unions, we check the cross-product
 	      [(list (Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)]
 	      [(list s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)]
-	      ;; applications and names are structs too
-	      [(list (App: (Name: n) args stx) other)
-	       (let ([t (lookup-type-name n)])
-		 (unless (Type? t)                     
-			 (fail! s t))
-		 #;(printf "subtype: app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other 
-		 (instantiate-poly t args))
-		 (unless (Poly? t)
-			 (tc-error/stx stx "cannot apply non-polymorphic type ~a" t))                 
-		 (match t [(Poly-unsafe: n _)
-			   (unless (= n (length args))
-				   (tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a"
-						 n (length args)))])
-		 (let ([v (subtype* A0 (instantiate-poly t args) other)])
-		   #;(printf "val: ~a~n"  v)
-		   v))]
-	      [(list other (App: (Name: n) args stx))
-	       (let ([t (lookup-type-name n)])
-		 (unless (Type? t)                     
-			 (fail! s t))
-		 #;(printf "subtype: 2 app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other 
-		 (instantiate-poly t args))
-		 (unless (Poly? t)
-			 (tc-error/stx stx "cannot apply non-polymorphic type ~a" t))                 
-		 (match t [(Poly-unsafe: n _)
-			   (unless (= n (length args))
-				   (tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a"
-						 n (length args)))])
-					;(printf "about to call subtype with: ~a ~a ~n" other (instantiate-poly t args))
-		 (let ([v (subtype* A0 other (instantiate-poly t args))])
-		   #;(printf "2 val: ~a~n"  v)
-		   v))]
-	      [(list (Name: n) other)
-	       (let ([t (lookup-type-name n)])
-		 (if (Type? t)                     
-		     (subtype* A0 t other)
-		     (fail! s t)))]
-              [(list other (Name: n))
-	       (let ([t (lookup-type-name n)])
-		 (if (Type? t)                     
-		     (subtype* A0 other t)
-		     (fail! t s)))]
 	      ;; subtyping on immutable structs is covariant
 	      [(list (Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _))
-               (printf "subtyping on structs: ~a ~a~n" flds flds*)
 	       (subtypes* A0 flds flds*)]
 	      [(list (Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _))
 	       (subtypes* A0 (cons proc flds) (cons proc* flds*))]