diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
index 4c51b3f..76fa21a 100644
--- a/tapl/mlish.rkt
+++ b/tapl/mlish.rkt
@@ -3,9 +3,9 @@
 
 (extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let
           #:rename [~→ ~ext-stlc:→])
-(require (only-in "sysf.rkt" inst ~∀ ∀ Λ))
+(reuse inst ~∀ ∀ ∀? Λ #:from "sysf.rkt")
 (require (only-in "stlc+rec-iso.rkt" case fld unfld μ × ∨ var tup define-type-alias)
-         (prefix-in stlc+rec-iso: (only-in "stlc+rec-iso.rkt" define)))
+         #;(prefix-in stlc+rec-iso: (only-in "stlc+rec-iso.rkt" define)))
 ;(reuse cons [head hd] [tail tl] nil [isnil nil?] List ~List list #:from "stlc+cons.rkt")
 ;(reuse tup × proj #:from "stlc+tup.rkt")
 ;(reuse define-type-alias #:from "stlc+reco+var.rkt")
@@ -27,7 +27,7 @@
       ; should only be monomorphic?
       [((~∀ () (~ext-stlc:→ τ1 ...)) (~∀ () (~ext-stlc:→ τ2 ...)))
        (compute-constraints #'((τ1 τ2) ...))]
-      [_ #:when (displayln τ1-τ2) #'()]))
+      [_ #:when #t #;(printf "shouldnt get here. could not unify: ~a\n" τ1-τ2) #'()]))
   (define (compute-constraints τs)
     ;(printf "constraints: ~a\n" (syntax->datum τs))
     (stx-appendmap compute-constraint τs))
@@ -47,6 +47,44 @@
       [(_ . rst) (lookup x #'rst)]
       [() false])))
 
+(define-typed-syntax define
+  [(_ x:id e)
+   #:with (e- τ) (infer+erase #'e)
+   #:with y (generate-temporary)
+   #'(begin
+       (define-syntax x (make-rename-transformer (⊢ y : τ)))
+       (define y e-))]
+  ; explicit "forall"
+  #;[(_ (~and Xs {X:id ...}) (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
+   #:when (brace? #'Xs)
+   #: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 g (Λ (X ...) (ext-stlc:λ ([x : τ] ...) e_ann))))]
+  [(_ (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
+   #:when (displayln #'f)
+   #:with Ys
+          (let L ([Xs #'()]) ; compute unbound ids; treat as tyvars
+            (with-handlers
+                ([exn:fail:syntax:unbound?
+                  (λ (e)
+                    (define X (stx-car (exn:fail:syntax-exprs e)))
+                    ; X is tainted, so need to launder it
+                    (define Y (datum->syntax #'f (syntax->datum X)))
+                    (L (cons Y Xs)))])
+              ((current-type-eval) #`(∀ #,Xs (ext-stlc:→ τ ... τ_out)))
+              Xs))
+   #:when (displayln #'Ys)
+   #:with g (generate-temporary #'f)
+   #:with e_ann #'(add-expected e τ_out)
+   #`(begin
+      (define-syntax f
+        (make-rename-transformer (⊢ g : (∀ Ys (ext-stlc:→ τ ... τ_out)))))
+      (define g
+        (Λ Ys (ext-stlc:λ ([x : τ] ...) e_ann))))])
+;
+;; internal form used to expand many types at once under the same context
 (define-type-constructor Tmp #:arity >= 0 #:bvs >= 0) ; need a >= 0 arity
 
 (define-syntax (define-type stx)
@@ -135,7 +173,8 @@
               (⊢ (StructName e_arg- ...) : τ_out)]
              [(C . args) #:when (stx-null? #'(X ...)) #'(C {} . args)] ; no tyvars, no annotations
              [(C . args) ; no type annotations, must infer instantiation
-              ;; infer instantiation types from args left-to-right, short-circuit if done early
+              ;; infer instantiation types from args left-to-right,
+              ;; short-circuit if done early, and use result to help infer remaining args
               #:with (~Tmp Ys . τs+) ((current-type-eval) #'(Tmp (X ...) τ ...))
               (let loop ([a (stx-car #'args)] [a-rst (stx-cdr #'args)]
                          [τ+ (stx-car #'τs+)] [τ+rst (stx-cdr #'τs+)]
@@ -173,10 +212,28 @@
      #:with (acc ...) (syntax-property #'τ_e 'accessors)
      (⊢ (let ([x_out (acc e-)] ...) e_out) : τ_out)]))
 
-(define-syntax lifted→ ; wrap → with ∀
+#;(define-syntax lifted→ ; wrap → with ∀
   (syntax-parser
     [(_ . rst) #'(∀ () (ext-stlc:→ . rst))]))
+(define-syntax lifted→ ; wrapping →
+  (syntax-parser
+    #;[(_ (~and Xs {X:id ...}) . rst)
+     #:when (brace? #'Xs)
+     #:when (with-handlers ([exn:fail:syntax:unbound? (λ (e) (displayln (exn:fail:syntax-exprs e)))])
+              ((current-type-eval) #'(ext-stlc:→ . rst)))
+     #'(∀ (X ...) (ext-stlc:→ . rst))]
+    [(_ . rst)
+     (let L ([Xs #'()]) ; compute unbound ids; treat as tyvars
+       (with-handlers ([exn:fail:syntax:unbound?
+                        (λ (e)
+                          (define X (stx-car (exn:fail:syntax-exprs e)))
+                          ; X is tainted, so need to launder it
+                          (define Y (datum->syntax #'rst (syntax->datum X)))
+                          (L (cons Y Xs)))])
+         ((current-type-eval) #`(∀ #,Xs (ext-stlc:→ . rst)))))]))
+     ;#'(∀ () (ext-stlc:→ . rst))
 
+; redefine these to use lifted→
 (define-primop + : (lifted→ Int Int Int))
 (define-primop - : (lifted→ Int Int Int))
 (define-primop void : (lifted→ Unit))
@@ -188,14 +245,62 @@
 (define-primop abs : (lifted→ Int Int))
 
 
-; all λs have type (∀ (X ...) (→ τ_in ... τ_out))
+; all λs have type (∀ (X ...) (→ τ_in ... τ_out)), even monomorphic fns
 (define-typed-syntax liftedλ #:export-as λ #:datum-literals (:)
   [(_ . rst)
    #'(Λ () (ext-stlc:λ . rst))])
 
-(define-typed-syntax new-app #:export-as #%app
+
+#;(define-typed-syntax new-app #:export-as #%app
   [(_ τs f . args)
    #:when (brace? #'τs)
    #'(ext-stlc:#%app (inst f . τs) . args)]
   [(_ f . args)
    #'(ext-stlc:#%app (inst f) . args)])
+
+(define-typed-syntax #%app
+  [(_ e_fn e_arg ...) ; infer args first
+   #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
+   ;#:with [e_fn- ((X ...) ((~ext-stlc:→ τ_inX ... τ_outX)))] (⇑ e_fn as ∀)
+   ;#:with [e_fn- (~∀ (X ...) (~ext-stlc:→ τ_inX ... τ_outX))] (infer+erase #'e_fn)
+   ;; infer type step-by-step to produce better err msg
+   #:with [e_fn- τ_fn] (infer+erase #'e_fn)
+   #:fail-unless (and (∀? #'τ_fn) (syntax-parse #'τ_fn [(~∀ _ (~ext-stlc:→ . args)) #t][_ #f]))
+                 (format "Expected expression ~a to have → type, got: ~a"
+                         (syntax->datum #'e_fn) (type->str #'τ_fn))
+   #:with (~∀ (X ...) (~ext-stlc:→ τ_inX ... τ_outX)) #'τ_fn
+   #:fail-unless (stx-length=? #'(τ_inX ...) #'(e_arg ...)) ; check arity
+                 (string-append
+                  (format "~a (~a:~a) Wrong number of arguments given to function ~a.\n"
+                          (syntax-source stx) (syntax-line stx) (syntax-column stx)
+                          (syntax->datum #'e_fn))
+                  (format "Expected: ~a arguments with types: "
+                          (stx-length #'(τ_inX ...)))
+                  (string-join (stx-map type->str #'(τ_inX ...)) ", " #:after-last "\n")
+                  "Given:\n"
+                  (string-join
+                   (map (λ (e t) (format "  ~a : ~a" e t)) ; indent each line
+                        (syntax->datum #'(e_arg ...))
+                        (stx-map type->str #'(τ_arg ...)))
+                   "\n"))
+   #:with cs (compute-constraints #'((τ_inX τ_arg) ...))
+   #:with (τ_solved ...) (filter (λ (x) x) (stx-map (λ (y) (lookup y #'cs)) #'(X ...)))
+   #:fail-unless (stx-length=? #'(X ...) #'(τ_solved ...))
+                 (format "could not instantiate polymorphic fn ~a" (syntax->datum #'e_fn))
+   #:with (τ_in ... τ_out) (stx-map (λ (t) (substs #'(τ_solved ...) #'(X ...) t)) #'(τ_inX ... τ_outX))
+   ; some code duplication
+   #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
+                 (string-append
+                  (format "~a (~a:~a) Arguments to function ~a have wrong type(s).\n"
+                          (syntax-source stx) (syntax-line stx) (syntax-column stx)
+                          (syntax->datum #'e_fn))
+                  "Given:\n"
+                  (string-join
+                   (map (λ (e t) (format "  ~a : ~a" e t)) ; indent each line
+                        (syntax->datum #'(e_arg ...))
+                        (stx-map type->str #'(τ_arg ...)))
+                   "\n" #:after-last "\n")
+                  (format "Expected: ~a arguments with type(s): "
+                          (stx-length #'(τ_in ...)))
+                  (string-join (stx-map type->str #'(τ_in ...)) ", "))
+   (⊢ (#%app e_fn- e_arg- ...) : τ_out)])
diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt
index 5f4247a..5e07551 100644
--- a/tapl/tests/mlish-tests.rkt
+++ b/tapl/tests/mlish-tests.rkt
@@ -1,6 +1,64 @@
 #lang s-exp "../mlish.rkt"
 (require "rackunit-typechecking.rkt")
 
+(define (recf [x : Int] → Int) (recf x))
+
+;; tests more or less copied from infer-tests.rkt ------------------------------
+;; top-level defines
+(define (f [x : Int] → Int) x)
+(check-type f : (→ Int Int))
+(check-type (f 1) : Int ⇒ 1)
+(typecheck-fail (f (λ ([x : Int]) x)))
+
+(define (g [x : X] → X) x)
+(check-type g : (→ X X))
+
+; (inferred) polymorpic instantiation
+(check-type (g 1) : Int ⇒ 1)
+(check-type (g #f) : Bool ⇒ #f) ; different instantiation
+(check-type (g add1) : (→ Int Int))
+(check-type (g +) : (→ Int Int Int))
+
+; function polymorphic in list element
+(define-type (List X)
+  (Nil)
+  (Cons X (List X)))
+
+(define (g2 [lst : (List X)] → (List X)) lst)
+(check-type g2 : (→ (List X) (List X)))
+(typecheck-fail (g2 1) #:with-msg "Expected.+arguments with type.+(List X)")
+;(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)}))
+;(check-type (g2 (Nil {(→ Int Int)})) : (List (→ Int Int)) ⇒ (Nil {(List (→ Int Int))}))
+;(check-type (g2 (Cons 1 Nil)) : (List Int) ⇒ (Cons 1 Nil))
+;(check-type (g2 (Cons "1" Nil)) : (List String) ⇒ (Cons "1" Nil))
+
+;(define (g3 [lst : (List X)] → X) (hd lst)) ; cant type this fn (what to put for nil case)
+;(check-type g3 : (→ {X} (List X) X))
+;(check-type g3 : (→ {A} (List A) A))
+;(check-not-type g3 : (→ {A B} (List A) B))
+;(typecheck-fail (g3) #:with-msg "Expected.+arguments with type.+List") ; TODO: more precise err msg
+;(check-type (g3 (nil {Int})) : Int) ; runtime fail
+;(check-type (g3 (nil {Bool})) : Bool) ; runtime fail
+;(check-type (g3 (cons 1 nil)) : Int ⇒ 1)
+;(check-type (g3 (cons "1" nil)) : String ⇒ "1")
+
+; recursive fn
+;(define (recf [x : Int] → Int) (recf x))
+;(check-type recf : (→ Int Int))
+;
+;(define (countdown [x : Int] → Int)
+;  (if (zero? x)
+;      0
+;      (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")
+
+;; end infer.rkt tests --------------------------------------------------
+
+;; algebraic data types
 (define-type IntList
   INil
   (ConsI Int IntList))
@@ -17,9 +75,6 @@
    [ConsI x xs -> 2]) : Int ⇒ 2)
 (typecheck-fail (match 1 with [INil -> 1]))
 
-(define-type (List X)
-  (Nil)
-  (Cons X (List X)))
 ;; annotated
 (check-type (Nil {Int}) : (List Int))
 (check-type (Cons {Int} 1 (Nil {Int})) : (List Int))
@@ -236,7 +291,7 @@
  "Arguments to function \\+ have wrong type.+Given:.+(→ Int Int).+Expected: 2 arguments with type.+Int\\, Int")
 (typecheck-fail
  ((λ ([x : Int] [y : Int]) y) 1)
- #:with-msg "Arguments to function.+have.+wrong number of arguments")
+ #:with-msg "Wrong number of arguments given to function")
 
 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)