diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
index 43a15be..2dc9e59 100644
--- a/tapl/mlish.rkt
+++ b/tapl/mlish.rkt
@@ -71,23 +71,30 @@
        #'τ]
       [(_ . rst) (lookup x #'rst)]
       [() #f]))
-  
-  ;; Returns list of types, for each X in Xs, 
-  ;;   if it's possible to solve for such types from constraints cs
-  ;; else returns #f
-  (define (try-to-solve Xs cs)
-    (define maybe-solved 
-      (filter (lambda (x) x) (stx-map (λ (X) (lookup X cs)) Xs)))
-    (and (stx-length=? Xs maybe-solved)
-         maybe-solved))
+
+  ;; find-unsolved-Xs : (Stx-Listof Id) Constraints -> (Listof Id)
+  ;; finds the free Xs that aren't constrained by cs
+  (define (find-unsolved-Xs Xs cs)
+    (for/list ([X (in-list (stx->list Xs))]
+               #:when (not (lookup X cs)))
+      X))
+
+  ;; lookup-Xs/keep-unsolved : (Stx-Listof Id) Constraints -> (Listof Type-Stx)
+  ;; looks up each X in the constraints, returning the X if it's unconstrained
+  (define (lookup-Xs/keep-unsolved Xs cs)
+    (for/list ([X (in-list (stx->list Xs))])
+      (or (lookup X cs) X)))
 
   ;; solve for Xs by unifying quantified fn type with the concrete types of stx's args
   ;;   stx = the application stx = (#%app e_fn e_arg ...)
   ;;   tyXs = input and output types from fn type
   ;;          ie (typeof e_fn) = (-> . tyXs)
-  ;; returns list of types if success, else throws type error
-  ;; - infers type of arguments from left-to-right
-  ;; - short circuits if done early
+  ;; It infers the types of arguments from left-to-right,
+  ;; and it short circuits if it's done early.
+  ;; It returns list of 3 values if successful, else throws a type error
+  ;;  - a list of the arguments that it expanded
+  ;;  - a list of the the un-constrained type variables
+  ;;  - a list of types to fill in for the Xs
   (define (solve Xs tyXs stx)
     (syntax-parse tyXs
       [(τ_inX ... τ_outX)
@@ -103,20 +110,19 @@
               (for/fold ([as- null] [cs initial-cs])
                         ([a (in-list (syntax->list #'args))]
                          [tyXin (in-list (syntax->list #'(τ_inX ...)))]
-                         #:break (try-to-solve Xs cs))
+                         #:break (empty? (find-unsolved-Xs Xs cs)))
                 (define/with-syntax [a- ty_a] (infer+erase a))
                 (values 
                  (cons #'a- as-)
                  (stx-append cs (compute-constraint (list tyXin #'ty_a))))))
-         (define maybe-solved-tys (try-to-solve Xs cs))
-         
-         (if maybe-solved-tys
-             (list (reverse as-) maybe-solved-tys)
-             (type-error #:src stx
-              #:msg (mk-app-err-msg stx #:expected #'(τ_inX ...) 
-                     #:given (stx-map stx-cadr (infers+erase #'args))
-                     #:note (format "Could not infer instantiation of polymorphic function ~a."
-                                    (syntax->datum (get-orig #'e_fn))))))])]))
+
+         (list (reverse as-) (find-unsolved-Xs Xs cs) (lookup-Xs/keep-unsolved Xs cs))])]))
+
+  (define (raise-app-poly-infer-error stx expected-tys given-tys e_fn)
+    (type-error #:src stx
+     #:msg (mk-app-err-msg stx #:expected expected-tys #:given given-tys
+            #:note (format "Could not infer instantiation of polymorphic function ~a."
+                           (syntax->datum (get-orig e_fn))))))
 
   ;; instantiate polymorphic types
   (define (inst-type tys-solved Xs ty)
@@ -705,7 +711,7 @@
         #'(ext-stlc:#%app e_fn/ty (add-expected e_arg τ_inX) ...)])]
     [else
      ;; ) solve for type variables Xs
-     (define/with-syntax ((e_arg1- ...) tys-solved) (solve #'Xs #'tyX_args stx))
+     (define/with-syntax ((e_arg1- ...) (unsolved-X ...) tys-solved) (solve #'Xs #'tyX_args stx))
      ;; ) instantiate polymorphic function type
      (syntax-parse (inst-types #'tys-solved #'Xs #'tyX_args)
       [(τ_in ... τ_out) ; concrete types
@@ -737,7 +743,14 @@
                                     (equal? (syntax->datum x) (syntax->datum y))))))
                           (set-stx-prop/preserved tyin 'orig (list new-orig)))
                        #'(τ_in ...)))
-       (⊢ (#%app e_fn- e_arg- ...) : τ_out)])])]
+       #:with τ_out* (if (stx-null? #'(unsolved-X ...))
+                         #'τ_out
+                         (syntax-parse #'τ_out
+                           [(~?∀ (Y ...) τ_out)
+                            (unless (→? #'τ_out)
+                              (raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))
+                            #'(∀ (unsolved-X ... Y ...) τ_out)]))
+       (⊢ (#%app e_fn- e_arg- ...) : τ_out*)])])]
   [(_ e_fn . e_args) ; err case; e_fn is not a function
    #:with [e_fn- τ_fn] (infer+erase #'e_fn)
    (type-error #:src stx 
diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt
index 255e1c6..2c00b77 100644
--- a/tapl/tests/mlish-tests.rkt
+++ b/tapl/tests/mlish-tests.rkt
@@ -55,8 +55,7 @@
 (check-type g2 : (→/test (List Y) (List Y)))
 (typecheck-fail (g2 1) 
   #:with-msg 
-  (expected "(List Y)" #:given "Int"
-   #:note "Could not infer instantiation of polymorphic function"))
+  (expected "(List Y)" #:given "Int"))
 
 ;; todo? allow polymorphic nil?
 (check-type (g2 (Nil {Int})) : (List Int) ⇒ (Nil {Int}))
@@ -353,6 +352,107 @@
    (inst (λ ([x : X]) (inst (λ ([y : Y]) y) Int)) Int))
    : (→ Int (→ Int Int)))  
 
+(check-type 
+  ((λ ([x : X]) (λ ([y : Y]) (λ ([z : Z]) z))) 1)
+  : (→/test {Y} Y (→/test {Z} Z Z)))
+
+(check-type (inst Cons (→/test X X))
+  : (→ (→/test X X) (List (→/test X X)) (List (→/test X X))))
+(check-type map : (→/test (→ X Y) (List X) (List Y)))
+
+(check-type (Cons (λ ([x : X]) x) Nil)
+  : (List (→/test {X} X X)))
+
+(define (nn [x : X] -> (→ (× X (→ Y Y))))
+  (λ () (tup x (λ ([x : Y]) x))))
+(define nn-1 (nn 1))
+(check-type (nn-1) : (× Int (→ String String)))
+(check-type (nn-1) : (× Int (→ (List Int) (List Int))))
+
+(define (nn2 [x : X] -> (→ (× X (→ Y Y) (List Z))))
+  (λ () (tup x (λ ([x : Y]) x) Nil)))
+(define nn2-1 (nn2 1))
+(check-type (nn2-1) : (× Int (→ String String) (List (List Int))))
+(check-type (nn2-1) : (× Int (→ (List Int) (List Int)) (List String)))
+;; test inst order
+(check-type ((inst nn2-1 String (List Int))) : (× Int (→ String String) (List (List Int))))
+(check-type ((inst nn2-1 (List Int) String)) : (× Int (→ (List Int) (List Int)) (List String)))
+
+(define-type (Result A B)
+  (Ok A)
+  (Error B))
+
+(define (ok [a : A] → (Result A B))
+  (Ok a))
+(define (error [b : B] → (Result A B))
+  (Error b))
+
+(check-type (if (zero? (random 2))
+                (ok 0)
+                (error "didn't get a zero"))
+            : (Result Int String))
+
+(define result-if-0
+  (λ ([b : (Result A1 B1)] [succeed : (→ A1 (Result A2 B2))] [fail : (→ B1 (Result A2 B2))])
+    (match b with
+      [Ok a -> (succeed a)]
+      [Error b -> (fail b)])))
+(check-type result-if-0
+            : (→/test (Result A1 B1) (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2))
+                      (Result A2 B2)))
+
+(define (result-if-1 [b : (Result A1 B1)]
+                     → (→ (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2))
+                          (Result A2 B2)))
+  (λ ([succeed : (→ A1 (Result A2 B2))] [fail : (→ B1 (Result A2 B2))])
+    (result-if-0 b succeed fail)))
+(check-type result-if-1
+            : (→/test (Result A1 B1) (→ (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2))
+                                        (Result A2 B2))))
+(check-type (inst (result-if-1 (Ok {Int String} 1)) (List Int) (List String))
+            : (→ (→ Int (Result (List Int) (List String)))
+                 (→ String (Result (List Int) (List String)))
+                 (Result (List Int) (List String))))
+(check-type (inst (result-if-1 (Error {Int String} "bad")) (List Int) (List String))
+            : (→ (→ Int (Result (List Int) (List String)))
+                 (→ String (Result (List Int) (List String)))
+                 (Result (List Int) (List String))))
+(check-type ((result-if-1 (Ok {Int String} 1))
+             (λ ([a : Int])    (ok (Cons a Nil)))
+             (λ ([b : String]) (error (Cons b Nil))))
+            : (Result (List Int) (List String)))
+;; same thing, but without the lambda annotations:
+(check-type ((result-if-1 (Ok {Int String} 1))
+             (λ (a) (ok (Cons a Nil)))
+             (λ (b) (error (Cons b Nil))))
+            : (Result (List Int) (List String)))
+
+(define (result-if-2 [b : (Result A1 B1)]
+                     → (→ (→ A1 (Result A2 B2))
+                          (→ (→ B1 (Result A2 B2))
+                             (Result A2 B2))))
+  (λ ([succeed : (→ A1 (Result A2 B2))])
+    (λ ([fail : (→ B1 (Result A2 B2))])
+      (result-if-0 b succeed fail))))
+(check-type result-if-2
+            : (→/test (Result A1 B1) (→ (→ A1 (Result A2 B2))
+                                        (→ (→ B1 (Result A2 B2))
+                                           (Result A2 B2)))))
+(check-type (inst (result-if-2 (Ok {Int String} 1)) (List Int) (List String))
+            : (→/test (→ Int (Result (List Int) (List String)))
+                      (→ (→ String (Result (List Int) (List String)))
+                         (Result (List Int) (List String)))))
+(check-type ((result-if-2 (Ok {Int String} 1))
+             (λ ([a : Int]) (Ok {(List Int) (List String)} (Cons a Nil))))
+            : (→/test (→ String (Result (List Int) (List String)))
+                      (Result (List Int) (List String))))
+(check-type (((result-if-2 (Ok {Int String} 1))
+              ; type annotations are necessary here:
+              (λ ([a : Int]) (Ok {(List Int) (List String)} (Cons a Nil))))
+             ; but not here:
+             (λ (b) (Error (Cons b Nil))))
+            : (Result (List Int) (List String)))
+
 ;; records and automatically-defined accessors and predicates
 (define-type (RecoTest X Y)
   (RT1 [x : X] [y : Y] [z : String])
diff --git a/tapl/tests/mlish/match2.mlish b/tapl/tests/mlish/match2.mlish
index df8c951..85ab5ad 100644
--- a/tapl/tests/mlish/match2.mlish
+++ b/tapl/tests/mlish/match2.mlish
@@ -59,11 +59,10 @@
    [A x -> x]
    [_ -> -1]) : Int -> 1)
 
-;; TODO: better err msg, is actually a type err
 (typecheck-fail
   (match2 (B 1) with
    [B x -> x]) 
-  #:with-msg "Could not infer instantiation of polymorphic function B")
+  #:with-msg (expected "(× X X)" #:given "Int"))
 
 (check-type
   (match2 (B (tup 2 3)) with