+(define (check-let dls env x)
+
+ ; acc is a pair of (env . annotated bindings)
+ (define (process-component acc comps)
+ (let*
+ ; create a new env with tvars for each component
+ ; e.g. scc of (x y)
+ ; scc-env = ((x . t0) (y . t1))
+ ([scc-env
+ (fold-left
+ (lambda (acc c)
+ (env-insert acc c (fresh-tvar)))
+ (car acc) comps)]
+ ; typecheck each component
+ [type-results
+ (map
+ (lambda (c)
+ (let ([body (cadr (assoc c (let-bindings x)))])
+ (check dls scc-env body)))
+ comps)]
+ ; collect all the constraints in the scc
+ [cs
+ (fold-left
+ (lambda (acc res c)
+ (constraint-merge
+ (constraint-merge
+ ; unify with tvars from scc-env
+ ; result ~ tvar
+ (~ (env-lookup scc-env c) (cadr res))
+ (car res))
+ acc))
+ '() type-results comps)]
+ ; substitute *only* the bindings in this scc
+ [new-env
+ (map (lambda (x)
+ (if (memv (car x) comps)
+ (cons (car x) (substitute cs (cdr x)))
+ x))
+ scc-env)]
+
+ [annotated-bindings (append (cdr acc) ; the previous annotated bindings
+ (map list
+ comps
+ (map caddr type-results)))])
+ (cons new-env annotated-bindings)))
+ ; takes in the current environment and a scc
+ ; returns new environment with scc's types added in
+ (let* ([components (reverse (sccs (graph (let-bindings x))))]
+ [results (fold-left process-component (cons env '()) components)]
+ [new-env (car results)]
+ [annotated-bindings (cdr results)]
+
+ [body-results (map (lambda (body) (check dls new-env body)) (let-body x))]
+ [let-type (cadr (last body-results))]
+ [cs (fold-left (lambda (acc cs) (constraint-merge acc cs)) '() (map car body-results))]
+
+ [annotated `((let ,annotated-bindings ,@(map caddr body-results)) : ,let-type)])
+ (list cs let-type annotated)))
+
+(define (check-app dls env x)
+ (if (eqv? (car x) (cadr x))
+ ; recursive function (f f)
+ ; TODO: what about ((f a) f)????
+ (let* ([func-type (env-lookup env (car x))]
+ [return-type (fresh-tvar)]
+ [other-func-type `(abs ,func-type ,return-type)]
+ [cs (~ func-type other-func-type)]
+ [resolved-return-type (substitute cs return-type)]
+
+ [annotated `(((,(car x) : ,func-type)
+ (,(cadr x) : ,func-type)) : ,resolved-return-type)])
+ (list cs resolved-return-type annotated)))
+
+ ; regular function
+ (let* ([arg-type-res (check dls env (cadr x))]
+ [arg-type (cadr arg-type-res)]
+ [func-type-res (check dls env (car x))]
+ [func-type (cadr func-type-res)]
+
+ ; f ~ a -> t0
+ [func-c (~
+ (substitute (car arg-type-res) func-type)
+ `(abs ,arg-type ,(fresh-tvar)))]
+ [cs (constraint-merge
+ (constraint-merge func-c (car arg-type-res))
+ (car func-type-res))]
+
+ [resolved-func-type (substitute cs func-type)]
+ [resolved-return-type (caddr resolved-func-type)]
+
+ [annotated `((,(caddr func-type-res)
+ ,(caddr arg-type-res)) : ,resolved-return-type)])
+
+ (if (abs? resolved-func-type)
+ (let ((return-type (substitute cs (caddr resolved-func-type))))
+ (list cs return-type annotated))
+ (error #f "not a function"))))
+
+(define (check-case dls env x)
+
+ (define (check-match switch-type x)
+ (let ([pattern (car x)]
+ [expr (cadr x)])
+ (if (eqv? (ast-type pattern) 'app)
+ ; a pattern match with bindings
+ (let ([sum (assoc (car pattern) (cdr (assoc switch-type dls)))])
+ (unless sum (error #f "can't pattern match ~a with ~a" switch-type pattern))
+ (let* ([names (cdr pattern)]
+ [types (cdr sum)]
+ [new-env (fold-left env-insert env names types)])
+ (check dls new-env expr)))
+ ; a pattern match without bindings
+ (check dls env expr))))
+
+ (let* ([switch-type-res (check dls env (case-switch x))]
+ [switch-type (cadr switch-type-res)]
+
+ [case-expr-type-res (map (lambda (x) (check-match switch-type x)) (case-cases x))]
+ [case-expr-types (map cadr case-expr-type-res)]
+
+ [case-expr-equality-cs (fold-left constraint-merge '()
+ (map (lambda (t) (~ t (car case-expr-types)))
+ (cdr case-expr-types)))]
+
+ [resolved-type (substitute case-expr-equality-cs (car case-expr-types))]
+
+ [annotated `((case (,(case-expr x) : ,switch-type)
+ ,(map (lambda (c e et)
+ `(,c (,e : ,et)))
+ (map car (case-cases x))
+ (map cadr (case-cases x))
+ case-expr-types)) : ,resolved-type)]
+
+ [cs (fold-left constraint-merge '()
+ (cons (car switch-type-res) case-expr-equality-cs))])
+ (list cs resolved-type annotated)))
+
+; returns a list (constraints type annotated)
+(define (check dls env x)
+ (define (make-result cs type)
+ (list cs type `(,x : ,type)))