(define (check-case dls env x)
(define (check-match switch-type x)
+
+ (define (get-bindings product-types pattern)
+ (define (go product-type product)
+ (case (ast-type product)
+ ['var (list (cons product product-type))]
+ ; an inner pattern match
+ ['app (let* ([inner-sum (car product)]
+ [inner-sums (cdr (assoc product-type dls))]
+ [inner-product-types (cdr (assoc inner-sum inner-sums))])
+ (get-bindings inner-product-types product))]
+ [else '()]))
+ (flat-map go product-types (cdr pattern)))
+
+
(let ([pattern (car x)]
[expr (cadr x)])
(case (ast-type pattern)
(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)])
+ [product-types (cdr sum)]
+ [new-env (append (get-bindings product-types pattern) env)])
+
(check dls new-env expr)))]
; pattern match with binding and no constructor
['var (check dls (env-insert env pattern switch-type) expr)]
[resolved-type (substitute case-expr-equality-cs (car case-expr-types))]
- [annotated `((case (,(case-switch x) : ,switch-type)
+ [annotated `((case ,(caddr switch-type-res)
,@(map (lambda (c e et)
`(,c ((,e : ,et))))
(map car (case-cases x))