diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
index 6590196..c032ca6 100644
--- a/tapl/mlish.rkt
+++ b/tapl/mlish.rkt
@@ -412,6 +412,9 @@
 (define-typed-syntax liftedλ #:export-as λ
   [(_ (y:id x:id ...) . body)
    (type-error #:src stx #:msg "λ parameters must have type annotations")]
+  [(_ args body)
+   #:with (~∀ () (~ext-stlc:→ arg-ty ... body-ty)) (get-expected-type stx)
+   #`(Λ () (ext-stlc:λ args #,(add-expected-ty #'body #'body-ty)))]
   [(_ . rst)
    #'(Λ () (ext-stlc:λ . rst))])
 
diff --git a/tapl/tests/mlish/inst.mlish b/tapl/tests/mlish/inst.mlish
index c3984be..af8684b 100644
--- a/tapl/tests/mlish/inst.mlish
+++ b/tapl/tests/mlish/inst.mlish
@@ -61,3 +61,14 @@
 (check-type alias-test2 : (→/test B (Read-Result B)))
 (check-type alias-test3 : (→/test B (Result (× B (List Char)) String)))
 (check-type alias-test3 : (→/test B (Read-Result B)))
+
+(define (expect-listof-int [loi : (List Int)] → Int)
+  0)
+
+(check-type (expect-listof-int nil) : Int -> 0)
+
+(define (expect-→listof-int [f : (→ (List Int))] → Int)
+  0)
+
+(check-type (expect-→listof-int (λ () nil)) : Int -> 0)
+