diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt index f7cb715..255e1c6 100644 --- a/tapl/tests/mlish-tests.rkt +++ b/tapl/tests/mlish-tests.rkt @@ -333,11 +333,26 @@ (λ (y) x)) (check-type tvf6 : (→/test X (→ Y X))) +;; 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 : Y]) x)) : (→/test X (→ X X))) +(check-type + ((λ ([x : X]) (λ ([y : Y]) y)) 1) + : (→/test Y Y)) + +;; TODO? +;; - this fails if polymorphic functions are allowed as HO args +;; - do we want to allow this? +;; - must explicitly instantiate before passing fn +(check-type + ((λ ([x : (→ X (→ Y Y))]) x) + (inst (λ ([x : X]) (inst (λ ([y : Y]) y) Int)) Int)) + : (→ Int (→ Int Int))) + ;; records and automatically-defined accessors and predicates (define-type (RecoTest X Y) (RT1 [x : X] [y : Y] [z : String])