+(test-types (typecheck '((let ([foo 3]
+ [bar (baz foo)]
+ [baz (lambda (x) x)])
+ bar)))
+ 'Int)
+
+ ; mutual recursion
+(test-types (typecheck '((let ([f (lambda (n) (if (= n 0)
+ 0
+ (+ 1 (g (- n 1)))))]
+ [g (lambda (m) (f m))])
+ (f 10))))
+ 'Int)
+
+(test-types (typecheck '((let ([pow (lambda (p y)
+ (let ([go (lambda (n x)
+ (if (= n 0)
+ x
+ (go (- n 1) (* x y))))])
+ (go p 1)))])
+ (pow 4 2))))
+ 'Int)
+
+ ; ADTs
+
+
+(test-types
+ (typecheck
+ '((data A
+ [foo Int]
+ [bar Bool])
+ (let ([x (foo 42)]
+ [(foo y) x])
+ x)))
+ 'A)
+
+(test-types
+ (typecheck
+ '((data A
+ [foo Int]
+ [bar Bool])
+ (let ([x (foo 42)]
+ [(foo y) x])
+ y)))
+ 'Int)
+
+
+ ; pattern matching
+(test (let-bindings '(let ([(foo x) a]) x))
+ '((x (foo~0 a))))
+
+(test (let-bindings '(let ([x (foo 42)] [(foo y) x]) x))
+ '((x (foo 42))
+ (y (foo~0 x))))
+
+ ; type annotations
+
+(test (annotate-types
+ '((let ([x 42]
+ [y (+ 1 x)])
+ (- y x))))
+
+ '((let ()
+ ((let ((x (42 : Int))
+ (y (((+ : (abs Int (abs Int Int))) (1 : Int) (x : Int)) : Int)))
+ (((- : (abs Int (abs Int Int))) (y : Int) (x : Int)) : Int)) : Int)) : Int))
+
+(test-expr '(+ 1 2) 3)
+(test-expr '(bool->int (= 2 0)) 0)
+(test-expr '((lambda (x) ((lambda (y) (+ x y)) 42)) 100) 142)
+
+(test-expr '(* 10 5) 50)
+
+(test-expr '(let ((x (+ 1 32))