+(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)))
+