diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
index 654a915..20ea4a0 100644
--- a/tapl/mlish.rkt
+++ b/tapl/mlish.rkt
@@ -299,84 +299,113 @@
 
 ;; match --------------------------------------------------
 (define-syntax (match stx)
-  (syntax-parse stx #:datum-literals (with ->)
-    ;; TODO: eliminate redundant expansions
-    [(_ e with . clauses)
-     ;; e is tuple
-     #:with [e- ty_e] (infer+erase #'e)
-     #:when (×? #'ty_e)
-     #:with (~× ty ...) #'ty_e
-     #:with ([x ... -> e_body]) #'clauses
-     #:fail-unless (stx-length=? #'(ty ...) #'(x ...))
-                   "match clause pattern not compatible with given tuple"
-     #:with [(x- ...) e_body- ty_body] (infer/ctx+erase #'([x ty] ...) #'e_body)
-     #:with (acc ...) (for/list ([(a i) (in-indexed (syntax->list #'(x ...)))])
-                        #`(lambda (s) (list-ref s #,(datum->syntax #'here i))))
-     #:with z (generate-temporary)
-     (⊢ (let ([z e-])
-          (let ([x- (acc z)] ...) e_body-))
-          : ty_body)]
-    ;; e is variant
-    [(_ e with . clauses)
-     #:fail-when (null? (syntax->list #'clauses)) "no clauses"
-     #:with [e- τ_e] (infer+erase #'e)
-     #:with (~! [Clause:id x:id ... 
+ (syntax-parse stx #:datum-literals (with)
+   [(_ e with . clauses)
+    #:fail-when (null? (syntax->list #'clauses)) "no clauses"
+    #:with [e- τ_e] (infer+erase #'e)
+    (cond
+     [(×? #'τ_e) ;; e is tuple
+      (syntax-parse #'clauses #:datum-literals (->)
+       [([x ... -> e_body])
+        #:with (~× ty ...) #'τ_e
+        #:fail-unless (stx-length=? #'(ty ...) #'(x ...))
+                      "match clause pattern not compatible with given tuple"
+        #:with [(x- ...) e_body- ty_body] (infer/ctx+erase #'([x ty] ...) #'e_body)
+        #:with (acc ...) (for/list ([(a i) (in-indexed (syntax->list #'(x ...)))])
+                           #`(lambda (s) (list-ref s #,(datum->syntax #'here i))))
+        #:with z (generate-temporary)
+        (⊢ (let ([z e-])
+             (let ([x- (acc z)] ...) e_body-))
+           : ty_body)])]
+     [(List? #'τ_e) ;; e is List
+      (syntax-parse #'clauses #:datum-literals (-> ::)
+       [([(~or (~and (~and xs [x ...]) (~parse rst (generate-temporary)))
+               (~and (~seq (~seq x ::) ... rst:id) (~parse xs #'())))
+          -> e_body] ...)
+        #:fail-unless (stx-ormap (lambda (xx) (and (brack? xx) (zero? (stx-length xx)))) #'(xs ...))
+                      "match: missing empty list case"
+        #:fail-when (and (stx-andmap brack? #'(xs ...))
+                         (= 1 (stx-length #'(xs ...))))
+                    "match: missing non-empty list case"
+        #:with (~List ty) #'τ_e
+        #:with ([(x- ... rst-) e_body- ty_body] ...)
+               (stx-map (lambda (ctx e) (infer/ctx+erase ctx e)) 
+                 #'(([x ty] ... [rst (List ty)]) ...) #'(e_body ...))
+        #:with τ_out (stx-car #'(ty_body ...))
+        #:with (len ...) (stx-map (lambda (p) #`#,(stx-length p)) #'((x ...) ...))
+        #:with (lenop ...) (stx-map (lambda (p) (if (brack? p) #'= #'>=)) #'(xs ...))
+        #:with (pred? ...) (stx-map
+                            (lambda (l lo) #`(λ (lst) (#,lo (length lst) #,l)))
+                            #'(len ...) #'(lenop ...))
+        #:with ((acc1 ...) ...) (stx-map 
+                                    (lambda (xs)
+                                      (for/list ([(x i) (in-indexed (syntax->list xs))])
+                                        #`(lambda (lst) (list-ref lst #,(datum->syntax #'here i)))))
+                                  #'((x ...) ...))
+        #:with (acc2 ...) (stx-map (lambda (l) #`(lambda (lst) (list-tail lst #,l))) #'(len ...))
+        (⊢ (let ([z e-])
+             (cond 
+              [(pred? z)
+               (let ([x- (acc1 z)] ... [rst- (acc2 z)]) e_body-)] ...))
+           : τ_out)])]
+     [else  ;; e is variant
+      (syntax-parse #'clauses #:datum-literals (->)
+       [([Clause:id x:id ... 
              (~optional (~seq #:when e_guard) #:defaults ([e_guard #'(ext-stlc:#%datum . #t)]))
              -> e_c_un] ...) ; un = unannotated with expected ty
-            #'clauses ; clauses must stay in same order
-     ;; len #'clauses maybe > len #'info, due to guards
-     #:with ((~literal #%plain-lambda) (RecName) 
-             ((~literal let-values) ()
-              ((~literal let-values) ()
-               . info-body)))
-             (get-extra-info #'τ_e)
-     #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
-     #:with ((_ ((~literal quote) ConsAll) . _) ...) #'info-body
-     #:fail-unless (set=? (syntax->datum #'(Clause ...))
-                          (syntax->datum #'(ConsAll ...)))
-                   (string-append
-                     "clauses not exhaustive; missing: "
-                     (string-join      
-                         (map symbol->string
-                              (set-subtract 
-                                  (syntax->datum #'(ConsAll ...))
-                                (syntax->datum #'(Clause ...))))
-                       ", "))
-     #:with ((_ ((~literal quote) Cons) Cons? [_ acc τ] ...) ...)
-            (map ; ok to compare symbols since clause names can't be rebound
-             (lambda (Cl) 
-               (stx-findf
-                (syntax-parser
-                 [((~literal #%plain-app) 'C . rst)
-                  (equal? Cl (syntax->datum #'C))])
-                #'info-unfolded))
-             (syntax->datum #'(Clause ...)))
-     ;; this commented block experiments with expanding to unsafe ops
-     ;; #:with ((acc ...) ...) (stx-map 
-     ;;                         (lambda (accs)
-     ;;                          (for/list ([(a i) (in-indexed (syntax->list accs))])
-     ;;                            #`(lambda (s) (unsafe-struct*-ref s #,(datum->syntax #'here i)))))
-     ;;                         #'((acc-fn ...) ...))
-     #:with t_expect (syntax-property stx 'expected-type) ; propagate inferred type
-     #:with (e_c ...) (stx-map (lambda (ec) (add-expected-ty ec #'t_expect)) #'(e_c_un ...))
-     #:with (((x- ...) (e_guard- e_c-) (τ_guard τ_ec)) ...)
-            (stx-map 
-              (λ (bs eg+ec) (infers/ctx+erase bs eg+ec)) 
-              #'(([x : τ] ...) ...) #'((e_guard e_c) ...))
-     #:fail-unless (and (same-types? #'(τ_guard ...))
-                        (Bool? (stx-car #'(τ_guard ...))))
-                   "guard expression(s) must have type bool"
-     #:fail-unless (same-types? #'(τ_ec ...)) 
-                   (string-append "branches have different types, given: "
-                    (string-join (stx-map type->str #'(τ_ec ...)) ", "))
-     #:with τ_out (stx-car #'(τ_ec ...))
-     #:with z (generate-temporary) ; dont duplicate eval of test expr
-     (⊢ (let ([z e-])
-          (cond 
-           [(and (Cons? z) 
-                 (let ([x- (acc z)] ...) e_guard-))
-            (let ([x- (acc z)] ...) e_c-)] ...))
-          : τ_out)]))
+        ;; len #'clauses maybe > len #'info, due to guards
+        #:with ((~literal #%plain-lambda) (RecName) 
+                ((~literal let-values) ()
+                 ((~literal let-values) ()
+                  . info-body)))
+               (get-extra-info #'τ_e)
+        #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
+        #:with ((_ ((~literal quote) ConsAll) . _) ...) #'info-body
+        #:fail-unless (set=? (syntax->datum #'(Clause ...))
+                             (syntax->datum #'(ConsAll ...)))
+                      (string-append
+                       "clauses not exhaustive; missing: "
+                       (string-join      
+                           (map symbol->string
+                                (set-subtract 
+                                    (syntax->datum #'(ConsAll ...))
+                                  (syntax->datum #'(Clause ...))))
+                         ", "))
+        #:with ((_ ((~literal quote) Cons) Cons? [_ acc τ] ...) ...)
+               (map ; ok to compare symbols since clause names can't be rebound
+                (lambda (Cl) 
+                  (stx-findf
+                      (syntax-parser
+                        [((~literal #%plain-app) 'C . rst)
+                         (equal? Cl (syntax->datum #'C))])
+                    #'info-unfolded))
+                (syntax->datum #'(Clause ...)))
+        ;; this commented block experiments with expanding to unsafe ops
+        ;; #:with ((acc ...) ...) (stx-map 
+        ;;                         (lambda (accs)
+        ;;                          (for/list ([(a i) (in-indexed (syntax->list accs))])
+        ;;                            #`(lambda (s) (unsafe-struct*-ref s #,(datum->syntax #'here i)))))
+        ;;                         #'((acc-fn ...) ...))
+        #:with t_expect (syntax-property stx 'expected-type) ; propagate inferred type
+        #:with (e_c ...) (stx-map (lambda (ec) (add-expected-ty ec #'t_expect)) #'(e_c_un ...))
+        #:with (((x- ...) (e_guard- e_c-) (τ_guard τ_ec)) ...)
+               (stx-map 
+                   (λ (bs eg+ec) (infers/ctx+erase bs eg+ec)) 
+                 #'(([x : τ] ...) ...) #'((e_guard e_c) ...))
+        #:fail-unless (and (same-types? #'(τ_guard ...))
+                           (Bool? (stx-car #'(τ_guard ...))))
+                      "guard expression(s) must have type bool"
+        #:fail-unless (same-types? #'(τ_ec ...)) 
+                      (string-append "branches have different types, given: "
+                       (string-join (stx-map type->str #'(τ_ec ...)) ", "))
+        #:with τ_out (stx-car #'(τ_ec ...))
+        #:with z (generate-temporary) ; dont duplicate eval of test expr
+        (⊢ (let ([z e-])
+             (cond 
+              [(and (Cons? z) 
+                    (let ([x- (acc z)] ...) e_guard-))
+               (let ([x- (acc z)] ...) e_c-)] ...))
+           : τ_out)])])]))
 
 (define-syntax → ; wrapping →
   (syntax-parser
diff --git a/tapl/tests/mlish/listpats.mlish b/tapl/tests/mlish/listpats.mlish
new file mode 100644
index 0000000..208793d
--- /dev/null
+++ b/tapl/tests/mlish/listpats.mlish
@@ -0,0 +1,70 @@
+#lang s-exp "../../mlish.rkt"
+(require "../rackunit-typechecking.rkt")
+
+;; pattern matching for built-in lists
+
+(check-type
+  (match (list 1 2) with
+   [[] -> 0]
+   [[x y] -> (+ x y)]) : Int -> 3)
+
+(typecheck-fail
+  (match (list 1 2) with
+   [[x y] -> (+ x y)]) #:with-msg "missing empty list case")
+
+(typecheck-fail
+  (match (list 1 2) with
+   [[] -> 0]) #:with-msg "missing non\\-empty list case")
+
+(check-type
+  (match (list 1 2) with
+   [[] -> 0]
+   [[x y] -> (+ x y)]) : Int -> 3)
+
+(check-type
+  (match (list 1 2) with
+   [[x y] -> (+ x y)]
+   [[] -> 0]) : Int -> 3)
+
+(check-type
+  (match (nil {Int}) with
+   [[x y] -> (+ x y)]
+   [[] -> 0]) : Int -> 0)
+
+(check-type
+  (match (list 1 2 3) with
+   [[] -> (nil {Int})]
+   [x :: rst -> rst]) : (List Int) -> (list 2 3))
+
+(check-type
+  (match (list 1 2 3) with
+   [[] -> (nil {Int})]
+   [x :: y :: rst -> rst]) : (List Int) -> (list 3))
+
+(check-type
+  (match (nil {Int}) with
+   [[] -> (nil {Int})]
+   [x :: y :: rst -> rst]) : (List Int) -> (nil {Int}))
+
+(check-type
+  (match (list 1 2 3) with
+   [[] -> 0]
+   [x :: y :: rst -> (+ x y)]) : Int -> 3)
+
+(check-type
+  (match (list 1 2 3) with
+   [[] -> 0]
+   [[x] -> 2]
+   [x :: rst -> 3]) : Int -> 3)
+
+(check-type
+  (match (list 1) with
+   [[] -> 0]
+   [[x] -> 2]
+   [x :: rst -> 3]) : Int -> 2)
+
+(check-type
+  (match (list 1) with
+   [[] -> 0]
+   [x :: rst -> 3]
+   [[x] -> 2]) : Int -> 3)
diff --git a/tapl/tests/run-mlish-tests1.rkt b/tapl/tests/run-mlish-tests1.rkt
index 4269396..b06448d 100644
--- a/tapl/tests/run-mlish-tests1.rkt
+++ b/tapl/tests/run-mlish-tests1.rkt
@@ -1,6 +1,8 @@
 #lang racket
 (require "mlish-tests.rkt")
 (require "mlish/queens.mlish")
+(require "mlish/listpats.mlish")
+
 ;; (require "mlish/trees.mlish")
 ;; (require "mlish/chameneos.mlish")
 ;; (require "mlish/ack.mlish")
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index 2620646..634adde 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -422,6 +422,9 @@
   (define (brace? stx)
     (define paren-shape/#f (syntax-property stx 'paren-shape))
     (and paren-shape/#f (char=? paren-shape/#f #\{)))
+  (define (brack? stx)
+    (define paren-shape/#f (syntax-property stx 'paren-shape))
+    (and paren-shape/#f (char=? paren-shape/#f #\[)))
   ;; todo: abstract out the common shape of a type constructor,
   ;; i.e., the repeated pattern code in the functions below
   (define (get-extra-info t)