diff --git a/macrotypes/type-constraints.rkt b/macrotypes/type-constraints.rkt
index 31fc7f6..cc72ac3 100644
--- a/macrotypes/type-constraints.rkt
+++ b/macrotypes/type-constraints.rkt
@@ -28,7 +28,16 @@
     (member X Xs* free-identifier=?))
   (add-constraints/var? Xs* X? substs new-cs orig-cs))
 
-(define (add-constraints/var? Xs* var? substs new-cs [orig-cs new-cs])
+;; Variance Type Type -> Boolean
+(define (typecheck?/variance variance a-expected b-actual)
+  (cond
+    [(equal? variance covariant) (typecheck? b-actual a-expected)]
+    [(equal? variance contravariant) (typecheck? b-actual a-expected)]
+    ;; invariant and irrelevant
+    [else (and (typecheck? a-expected b-actual)
+               (typecheck? b-actual a-expected))]))
+
+(define (add-constraints/var? Xs* var? substs new-cs [orig-cs new-cs] [variance covariant]) ;; TODO: variance ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   (define Xs (stx->list Xs*))
   (define Ys (stx-map stx-car substs))
   (define-syntax-class var
@@ -59,7 +68,8 @@
          Xs
          var?
          ;; Add the mapping #'a -> #'b to the substitution,
-         (add-substitution-entry entry substs)
+         (begin (displayln (list (type->str (car entry)) '-> (type->str (cadr entry)) 'with-substs substs))
+                (add-substitution-entry entry substs))
          ;; and substitute that in each of the constraints.
          (cs-substitute-entry entry #'rst)
          orig-cs)])]
@@ -95,7 +105,7 @@
        [else
         (syntax-parse #'[a b]
           [_
-           #:when (typecheck? #'a #'b)
+           #:when (typecheck?/variance variance #'a #'b)
            (add-constraints/var? Xs
                                  var?
                                  substs
@@ -110,6 +120,7 @@
                                  #'((τ1 τ2) ... . rst)
                                  orig-cs)]
           [else
+           (displayln 2)
            (type-error #:src (get-orig #'b)
                        #: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)) ", ")
diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt
index 24e0c91..042f9ac 100644
--- a/turnstile/examples/mlish.rkt
+++ b/turnstile/examples/mlish.rkt
@@ -880,6 +880,9 @@
    [⊢ e_fn ≫ e_fn- ⇒ (~?∀ Xs (~ext-stlc:→ . tyX_args))]
    ;; solve for type variables Xs
    #:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args this-syntax)
+   #:do {(newline)
+         (displayln "Solved argument types")
+         (map displayln (syntax->datum #'[[e_arg- ...] Xs* cs]))}
    ;; instantiate polymorphic function type
    #:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args)
    #:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)
@@ -888,8 +891,20 @@
                  (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
    ;; compute argument types
    #:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))
+   #:do {(newline)
+         (displayln "Computed argument types")
+         (for ([a (in-syntax #'(τ_arg ...))]
+               [in (in-syntax #'(τ_in ...))]
+               [e (in-syntax #'(e_arg ...))])
+           (display 'a=) (displayln (type->str a))
+           (display 'i=) (displayln (type->str in))
+           (display 'e=) (displayln (syntax->datum e))
+           (display 'ck) (displayln (check? a in))
+           (newline))
+         (displayln "----")}
    ;; typecheck args
    [τ_arg τ⊑ τ_in #:for e_arg] ...
+   #:do {(displayln "AAA")}
    #:with τ_out* (if (stx-null? #'(unsolved-X ...))
                      #'τ_out
                      (syntax-parse #'τ_out
@@ -903,6 +918,7 @@
                              (mk-app-poly-infer-error this-syntax #'(τ_in ...) #'(τ_arg ...) #'e_fn)
                              this-syntax)))
                         #'(∀ (unsolved-X ... Y ...) τ_out)]))
+   #:do {(displayln "BBB")}
    --------
    [⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out*]])