+ ('if
+ (let* ((cond-type-res (check env (cadr x)))
+ (then-type-res (check env (caddr x)))
+ (else-type-res (check env (cadddr x)))
+ (then-eq-else-cs (unify (cadr then-type-res)
+ (cadr else-type-res)))
+ (cs (consolidate
+ (car then-type-res)
+ (consolidate (car else-type-res)
+ then-eq-else-cs)))
+ (return-type (substitute cs (cadr then-type-res))))
+ (when (not (eqv? (cadr cond-type-res) 'bool))
+ (error #f "if condition isn't bool"))
+ (list cs return-type)))
+
+ ('var (list '() (env-lookup env x)))
+ ('let