+ ; recursive types
+
+(test-types (substitute '((t1 (abs t1 t10))) 't1) '(abs t1 t10))
+
+(test-types (typecheck '(let ([bar (lambda (y) y)]
+ [foo (lambda (x) (foo (bar #t)))])
+ foo))
+ '(abs bool a))
+
+(test-types (typecheck '(let ([bar (lambda (y) y)]
+ [foo (lambda (x) (foo (bar #t)))])
+ bar))
+ '(abs a a))
+
+(test-types (typecheck '(let ([foo 3]
+ [bar (+ foo baz)]
+ [baz (- bar 1)])
+ bar))
+ 'int)
+
+(test-types (typecheck '(let ([foo 3]
+ [bar (baz foo)]
+ [baz (lambda (x) x)])
+ baz))
+ '(abs a a))
+
+(test-types (typecheck '(let ([foo 3]
+ [bar (baz foo)]
+ [baz (lambda (x) x)])
+ bar))
+ 'int)
+