diff --git a/tapl/infer.rkt b/tapl/infer.rkt
index 54b0240..5dcb18f 100644
--- a/tapl/infer.rkt
+++ b/tapl/infer.rkt
@@ -6,6 +6,7 @@
 (require (only-in "stlc+cons.rkt" ~List))
 (reuse tup × proj #:from "stlc+tup.rkt")
 (reuse define-type-alias #:from "stlc+reco+var.rkt")
+(require (for-syntax "type-constraints.rkt"))
 (provide hd tl nil?)
 (provide →)
 
@@ -15,8 +16,8 @@
   (syntax-parser
     [(_ (~and Xs {X:id ...}) . rst)
      #:when (brace? #'Xs)
-     #'(∀ (X ...) (ext-stlc:→ . rst))]
-    [(_ . rst) #'(∀ () (ext-stlc:→ . rst))]))
+     (add-orig #'(∀ (X ...) (ext-stlc:→ . rst)) (get-orig this-syntax))]
+    [(_ . rst) (add-orig #'(∀ () (ext-stlc:→ . rst)) (get-orig this-syntax))]))
 
 (define-primop + : (→ Int Int Int))
 (define-primop - : (→ Int Int Int))
@@ -28,34 +29,6 @@
 (define-primop not : (→ Bool Bool))
 (define-primop abs : (→ Int Int))
 
-(begin-for-syntax 
-  (define (compute-constraint τ1-τ2)
-    (syntax-parse τ1-τ2
-      [(X:id τ) #'((X τ))]
-      [((~List τ1) (~List τ2)) (compute-constraint #'(τ1 τ2))]
-      ; should only be monomorphic?
-      [((~∀ () (~ext-stlc:→ τ1 ...)) (~∀ () (~ext-stlc:→ τ2 ...)))
-       (compute-constraints #'((τ1 τ2) ...))]
-      [_ #'()]))
-  (define (compute-constraints τs)
-    ;(printf "constraints: ~a\n" (syntax->datum τs))
-    (stx-appendmap compute-constraint τs))
-
-  (define (solve-constraint x-τ)
-    (syntax-parse x-τ
-      [(X:id τ) #'((X τ))]
-      [_ #'()]))
-  (define (solve-constraints cs)
-    (stx-appendmap compute-constraint cs))
-  
-  (define (lookup x substs)
-    (syntax-parse substs
-      [((y:id τ) . rst)
-       #:when (free-identifier=? #'y x)
-       #'τ]
-      [(_ . rst) (lookup x #'rst)]
-      [() false])))
-
 (define-typed-syntax define
   [(_ x:id e)
    #:with (e- τ) (infer+erase #'e)
@@ -68,7 +41,9 @@
    #:with g (generate-temporary #'f)
    #:with e_ann #'(add-expected e τ_out)
    #'(begin
-       (define-syntax f (make-rename-transformer (⊢ g : (∀ (X ...) (ext-stlc:→ τ ... τ_out)))))
+       (define-syntax f (make-rename-transformer
+                         (⊢ g : #,(add-orig #'(∀ (X ...) (ext-stlc:→ τ ... τ_out))
+                                            #'(→ τ ... τ_out)))))
        (define g (Λ (X ...) (ext-stlc:λ ([x : τ] ...) e_ann))))]
   [(_ (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
    #:with g (generate-temporary #'f)
@@ -86,7 +61,7 @@
                          (syntax->datum #'fn))
    #:with (τ_arg ...) #'given-τ-args
    #:with [λ- τ_λ] (infer+erase #'(ext-stlc:λ ([x : τ_arg] ...) e))
-   (⊢ λ- : (∀ () τ_λ))]
+   (⊢ λ- : #,(add-orig #'(∀ () τ_λ) (get-orig #'τ_λ)))]
   [(~and fn (_ (x:id ...) e) ~!) ; no annotations, couldnt infer from ctx (eg, unapplied lam), try to infer from body
    #:with (xs- e- τ_res) (infer/ctx+erase #'([x : x] ...) #'e)
    #:with env (get-env #'e-)
@@ -100,11 +75,12 @@
    ;; propagate up inferred types of variables
    #:with res (add-env #'(λ xs- e-) #'env)
 ;   #:with [λ- τ_λ] (infer+erase #'(ext-stlc:λ ([x : x] ...) e))
-   (⊢ res : (∀ () (ext-stlc:→ τ_arg ... τ_res)))]
+   (⊢ res : #,(add-orig #'(∀ () (ext-stlc:→ τ_arg ... τ_res))
+                        #`(→ #,@(stx-map get-orig #'(τ_arg ... τ_res)))))]
    ;(⊢ (λ xs- e-) : (∀ () (ext-stlc:→ τ_arg ... τ_res)))]
   [(_ . rst)
    #:with [λ- τ_λ] (infer+erase #'(ext-stlc:λ . rst))
-   (⊢ λ- : (∀ () τ_λ))])
+   (⊢ λ- : #,(add-orig #'(∀ () τ_λ) (get-orig #'τ_λ)))])
 
 (define-typed-syntax #%app
   [(_ e_fn e_arg ...) ; infer args first
@@ -131,9 +107,8 @@
                         (syntax->datum #'(e_arg ...))
                         (stx-map type->str #'(τ_arg ...)))
                    "\n")))
-   #:with cs (compute-constraints #'((τ_inX τ_arg) ...))
-   #:with (τ_solved ...) (stx-map (λ (y) (lookup y #'cs)) #'(X ...))
-   #:with (τ_in ... τ_out) (stx-map (λ (t) (substs #'(τ_solved ...) #'(X ...) t)) #'(τ_inX ... τ_outX))
+   #:with cs (add-constraints #'(X ...) '() #'([τ_inX τ_arg] ...))
+   #:with (τ_in ... τ_out) (inst-types/cs #'(X ...) #'cs #'(τ_inX ... τ_outX))
    ; some code duplication
    #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
                  (type-error #:src stx
@@ -186,14 +161,12 @@
               [else
                (define/with-syntax [e τ] (infer+erase e_arg))
   ;             (displayln #'(e τ))
-               (define/with-syntax (c ...) cs)
-               (define/with-syntax (new-c ...) (compute-constraint #`(#,τ_inX τ)))
-               (values #'(new-c ... c ...) (cons #'[e τ] e+τs))]))])
+               (define cs* (add-constraints #'(X ...) cs #`([#,τ_inX τ])))
+               (values cs* (cons #'[e τ] e+τs))]))])
             (define/with-syntax e+τs/stx e+τs)
             (list cs (reverse (syntax->list #'e+τs/stx))))
    #:with env (stx-flatten (filter (λ (x) x) (stx-map get-env #'(e_arg- ...))))
-   #:with (τ_solved ...) (stx-map (λ (y) (lookup y #'cs)) #'(X ...))
-   #:with (τ_in ... τ_out) (stx-map (λ (t) (substs #'(τ_solved ...) #'(X ...) t)) #'(τ_inX ... τ_outX))
+   #:with (τ_in ... τ_out) (inst-types/cs #'(X ...) #'cs #'(τ_inX ... τ_outX))
    ; some code duplication
    #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
                  (string-append
diff --git a/tapl/tests/infer-tests.rkt b/tapl/tests/infer-tests.rkt
index 3246857..73f304c 100644
--- a/tapl/tests/infer-tests.rkt
+++ b/tapl/tests/infer-tests.rkt
@@ -36,7 +36,7 @@
 ; function polymorphic in list element
 (define {X} (g2 [lst : (List X)] → (List X)) lst)
 (check-type g2 : (→ {X} (List X) (List X)))
-(typecheck-fail (g2 1) #:with-msg "Expected.+arguments with type.+List") ; TODO: more precise err msg
+(typecheck-fail (g2 1) #:with-msg "expected: \\(List X\\)\n *given: Int") ; TODO: more precise err msg
 (check-type (g2 (nil {Int})) : (List Int) ⇒ (nil {Int}))
 (check-type (g2 (nil {Bool})) : (List Bool) ⇒ (nil {Bool}))
 (check-type (g2 (nil {(List Int)})) : (List (List Int)) ⇒ (nil {(List Int)}))
@@ -64,7 +64,7 @@
       (countdown (sub1 x))))
 (check-type (countdown 0) : Int ⇒ 0)
 (check-type (countdown 10) : Int ⇒ 0)
-(typecheck-fail (countdown "10") #:with-msg "Arguments.+have wrong type")
+(typecheck-fail (countdown "10") #:with-msg "expected: Int\n *given: String")
 
 ; list abbrv
 (check-type (list 1 2 3) : (List Int))
@@ -88,7 +88,11 @@
 (check-type (map add1 nil) : (List Int) ⇒ (nil {Int}))
 (check-type (map add1 (list)) : (List Int) ⇒ (nil {Int}))
 (check-type (map add1 (list 1 2 3)) : (List Int) ⇒ (list 2 3 4))
-(typecheck-fail (map add1 (list "1")) #:with-msg "Arguments.+have wrong type")
+(typecheck-fail (map add1 (list "1")) #:with-msg
+                (string-append
+                 "couldn't unify Int and String\n"
+                 " *expected: \\(→ X Y\\), \\(List X\\)\n"
+                 " *given: \\(→ Int Int\\), \\(List String\\)"))
 (check-type (map (λ ([x : Int]) (+ x 2)) (list 1 2 3)) : (List Int) ⇒ (list 3 4 5))
 ; doesnt work yet
 ;; 2015-12-18: dont need annotations on lambdas with concrete type
@@ -209,11 +213,11 @@
 (typecheck-fail
  ((λ ([x : Unit]) x) 2)
  #:with-msg
- "Arguments to function.+have wrong type.+Given:.+Int.+Expected:.+Unit")
+ "expected: Unit\n *given: Int")
 (typecheck-fail
  ((λ ([x : Unit]) x) void)
   #:with-msg
- "Arguments to function.+have wrong type.+Given:.+(→ Unit).+Expected:.+Unit")
+  "expected: Unit\n *given: \\(→ Unit\\)")
 
 (check-type ((λ ([x : Unit]) x) (void)) : Unit)
 
@@ -251,7 +255,7 @@
 (typecheck-fail
  (let ([x #f]) (+ x 1))
  #:with-msg
- "Arguments to function \\+.+have wrong type.+Given:.+Bool.+Int.+Expected:.+Int.+Int")
+ "expected: Int, Int\n *given: Bool, Int")
 (typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))
                 #:with-msg "x: unbound identifier")
 
@@ -259,7 +263,7 @@
 (typecheck-fail
  (let* ([x #t] [y (+ x 1)]) 1)
   #:with-msg
- "Arguments to function \\+.+have wrong type.+Given:.+Bool.+Int.+Expected:.+Int.+Int")
+  "expected: Int, Int\n *given: Bool, Int")
 
 ; letrec
 (typecheck-fail
@@ -332,7 +336,7 @@
 (typecheck-fail
  ((λ ([x : Bool]) x) 1)
  #:with-msg
- "Arguments to function.+have wrong type.+Given:.+Int.+Expected:.+Bool")
+ "expected: Bool\n *given: Int")
 ;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
 (typecheck-fail
  (λ ([f : Int]) (f 1 2))
@@ -347,11 +351,11 @@
 (typecheck-fail
  (+ 1 (λ ([x : Int]) x))
  #:with-msg
- "Arguments to function \\+ have wrong type.+Given:\n  1 : Int.+(→ Int Int).+Expected: 2 arguments with type.+Int\\, Int")
+ "expected: Int, Int\n *given: Int, \\(→ Int Int\\)")
 (typecheck-fail
  (λ ([x : (→ Int Int)]) (+ x x))
   #:with-msg
- "Arguments to function \\+ have wrong type.+Given:.+(→ Int Int).+Expected: 2 arguments with type.+Int\\, Int")
+  "expected: Int, Int\n *given: \\(→ Int Int\\), \\(→ Int Int\\)")
 (typecheck-fail
  ((λ ([x : Int] [y : Int]) y) 1)
  #:with-msg "Wrong number of arguments")