diff --git a/macrotypes/type-constraints.rkt b/macrotypes/type-constraints.rkt
index adaf01e..58cfa8d 100644
--- a/macrotypes/type-constraints.rkt
+++ b/macrotypes/type-constraints.rkt
@@ -140,22 +140,27 @@
         (free-id-table/c identifier? variance? #:immutable #t)
         (flat-named-contract
          "(stx-listof (stx-list/c type? type? variance?))"
-         (stx->list->c (listof (stx->list->c (list/c type? type? (stx->datum->c variance?))))))}
+         (stx->list->c (listof (stx->list->c (list/c type? type? (stx->datum->c variance?))))))
+        (flat-named-contract
+         "(stx-listof (stx-list/c syntax? syntax?))"
+         (stx->list->c (listof (stx->list->c (list/c syntax? syntax?)))))}
        {(free-id-table/c identifier? type? #:immutable #t)}
        (free-id-table/c identifier? type? #:immutable #t))])
 (define (add-constraints/variance Xs X→variance ab+variance*
+                                  orig-cs
                                   [old-solution (make-immutable-free-id-table)])
   (define Xset (immutable-free-id-set (stx->list Xs)))
   (define X? (curry free-id-set-member? Xset))
-  (add-constraints/variance/var? X? X→variance ab+variance* old-solution))
+  (add-constraints/variance/var? X? X→variance ab+variance* old-solution orig-cs))
 
 ;; (-> Any Boolean : (∩ X Id))
 ;; (ImmutableFreeIdTable (∩ X Id) Variance)
 ;; (Stx-Listof (Stx-List Type Type Variance)) ;; caller-τ callee-τ variance
 ;; (ImmutableFreeIdTable (∩ X Id) Type)
+;; (Stx-Listof (Stx-List Stx Stx))
 ;; ->
 ;; (ImmutableFreeIdTable (∩ X Id) Type)
-(define (add-constraints/variance/var? X? X→variance ab+variance* old-solution)
+(define (add-constraints/variance/var? X? X→variance ab+variance* old-solution orig-cs)
   (define-syntax-class X
     (pattern v:id
              #:when (X? #'v)
@@ -164,10 +169,12 @@
   (define (do-error)
     (define/with-syntax [(a b _) . _] ab+variance*)
     (type-error #:src (get-orig #'b)
-                #:msg "couldn't unify ~~a and ~~a"
+                #:msg (format "couldn't unify ~~a and ~~a\n  expected: ~a\n  given: ~a"
+                              (string-join (map type->str (stx-map stx-car orig-cs)) ", ")
+                              (string-join (map type->str (stx-map stx-cadr orig-cs)) ", "))
                 #'a #'b))
   (define (continue new-ab* new-solution)
-    (add-constraints/variance/var? X? X→variance new-ab* new-solution))
+    (add-constraints/variance/var? X? X→variance new-ab* new-solution orig-cs))
   (syntax-parse ab+variance*
     [() old-solution]
     [((caller-τ callee-τ:X a/b-variance) . rest)
diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt
index 2cf7c19..3d318b5 100644
--- a/turnstile/examples/mlish.rkt
+++ b/turnstile/examples/mlish.rkt
@@ -117,7 +117,9 @@
          (if (and (syntax-e #'expected-ty) (stx-null? #'Vs))
              (add-constraints/variance Xs
                                        Xs-variances
-                                       #`([expected-ty τ_outX #,contravariant]))
+                                       #`([expected-ty τ_outX #,contravariant])
+                                       ;; For error reporting only:
+                                       (list (list #'expected-ty #'τ_outX)))
              (make-immutable-free-id-table)))
        (syntax-parse stx
          [(_ e_fn . args)
@@ -135,6 +137,14 @@
                (add-constraints/variance Xs
                                          Xs-variances
                                          #`([ty_a #,ty_in #,covariant])
+                                         ;; For error reporting only:
+                                         (list (list (inst-type/cs/orig
+                                                      Xs (free-id-table-map cs list) ty_in
+                                                      (λ (id1 id2)
+                                                        (equal? (syntax->datum id1)
+                                                                (syntax->datum id2))))
+                                                     #'ty_a))
+                                         ;; current cs
                                          cs))))
           (define solution-as-list (free-id-table-map cs list))
           (list (reverse as-)