diff --git a/macrotypes/examples/mlish.rkt b/macrotypes/examples/mlish.rkt
index 7735019..960fc51 100644
--- a/macrotypes/examples/mlish.rkt
+++ b/macrotypes/examples/mlish.rkt
@@ -874,7 +874,9 @@
   [(_ (~and x+tys ([_ (~datum :) ty] ...)) . body)
    #:with Xs (compute-tyvars #'(ty ...))
    ;; TODO is there a way to have λs that refer to ids defined after them?
-   #'(?Λ Xs (ext-stlc:λ x+tys . body))])
+   #:with [f (~?∀ (X ...) (~ext-stlc:→ arg-ty ... (~?∀ (Y ...) body-ty)))]
+   (infer+erase #'(?Λ Xs (ext-stlc:λ x+tys . body)))
+   (⊢ f : (?∀ (X ... Y ...) (→ arg-ty ... body-ty)))])
 
 
 ;; #%app --------------------------------------------------
diff --git a/macrotypes/examples/tests/mlish-tests.rkt b/macrotypes/examples/tests/mlish-tests.rkt
index 75abf81..1dd4434 100644
--- a/macrotypes/examples/tests/mlish-tests.rkt
+++ b/macrotypes/examples/tests/mlish-tests.rkt
@@ -359,13 +359,16 @@
 ;; nested lambdas
 
 (check-type (λ ([x : X]) (λ ([y : X]) y)) : (→/test X (→ X X)))
-(check-not-type (λ ([x : X]) (λ ([y : X]) y)) : (→/test {X} X (→/test {Y} Y Y)))
-(check-type (λ ([x : X]) (λ ([y : Y]) y)) : (→/test {X} X (→/test {Y} Y Y)))
+(check-not-type (λ ([x : X]) (λ ([y : X]) y)) : (→/test X (→ Y Y)))
+(check-type (λ ([x : X]) (λ ([y : Y]) y)) : (→/test X (→ Y Y)))
 (check-not-type (λ ([x : X]) (λ ([y : Y]) x)) : (→/test X (→ X X)))
 
 (check-type 
   ((λ ([x : X]) (λ ([y : Y]) y)) 1)
-  : (→/test Y Y))
+  : (→ Int Int))
+(check-type 
+  ((λ ([x : X]) (λ ([y : Y]) y)) 1)
+  : (→ String String))
 
 ;; TODO?
 ;; - this fails if polymorphic functions are allowed as HO args
@@ -378,7 +381,10 @@
 
 (check-type 
   ((λ ([x : X]) (λ ([y : Y]) (λ ([z : Z]) z))) 1)
-  : (→/test {Y} Y (→/test {Z} Z Z)))
+  : (→/test Int (→ String String)))
+(check-type 
+  ((λ ([x : X]) (λ ([y : Y]) (λ ([z : Z]) z))) 1)
+  : (→/test String (→ Int Int)))
 
 (check-type (inst Cons (→/test X X))
   : (→ (→/test X X) (List (→/test X X)) (List (→/test X X))))
@@ -419,6 +425,8 @@
 (check-type (let ([x (nn4)])
               x)
             : (→/test (Option X)))
+(check-type (λ () (nn4)) : (→/test (→ (Option X))))
+
 
 (define (nn5 -> (→ (Ref (Option X))))
   (λ () (ref (None {X}))))
@@ -430,6 +438,7 @@
   (let ([r (((inst nn5 X)))])
     (λ () (deref r))))
 (check-type (nn6) : (→/test (Option X)))
+(check-type (λ () (nn6)) : (→/test (→ (Option X))))
 
 ;; A is covariant, B is invariant.
 (define-type (Cps A B)
@@ -449,6 +458,7 @@
 (check-type (let ([x (nn8)])
               x)
             : (→/test (Cps (Option A) Int)))
+(check-type (λ () (nn8)) : (→/test (→ (Cps (Option A) Int))))
 
 (define-type (Result A B)
   (Ok A)