diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
index 223f0b6..75f70e0 100644
--- a/tapl/mlish.rkt
+++ b/tapl/mlish.rkt
@@ -163,26 +163,7 @@
      #`(begin
          (define-type-constructor Name
            #:arity = #,(stx-length #'(X ...))
-;           #:other-prop variants #'(X ...) #'((Cons StructName [fld : τ] ...) ...))
            #:extra-info (X ...) (λ (RecName) ('Cons Cons? [acc τ/rec] ...) ...))
-         ;; cant use define-type-constructor because I want expansion to contain all
-         ;; variant info (including possibly recursive references)
-         ;; (define-syntax (Name stx)
-         ;;   (syntax-parse stx
-         ;;     [(_ Y ...)
-         ;;      #'(InternalName Y ... (λ (RecName) ('Cons StructName [fld τ/rec] ...) ...))]))
-         ;; (begin-for-syntax
-         ;;   (define-syntax NameExpander
-         ;;     (pattern-expander
-         ;;       (syntax-parser
-         ;;        [(_ . pat)
-         ;;         #:with expanded-ty (generate-temporary)
-         ;;         #'(~and expanded-ty
-         ;;             (~parse 
-         ;;               ((literal #%plain-app) (~literal InternalName)
-         ;;                arg ...  ((~literal #%plain-lambda) _ variant-info))
-         ;;               #'expanded-ty)
-         ;;             (~parse pat #'(arg ...)))]))))
          (struct StructName (fld ...) #:reflection-name 'Cons #:transparent) ...
          (define-syntax (Cons stx)
            (syntax-parse stx
@@ -256,6 +237,7 @@
               #'(C {τ_solved (... ...)} . args)]))
          ...)]))
 
+(require racket/unsafe/ops)
 ;; match --------------------------------------------------
 (define-syntax (match stx)
   (syntax-parse stx #:datum-literals (with ->)
@@ -267,11 +249,21 @@
              -> e_c_un] ...) ; un = unannotated with expected ty
             #'clauses ; clauses must stay in same order
      ;; len #'clauses maybe > len #'info, due to guards
-;     #:with info (syntax-property #'τ_e 'variants)
      #:with ((~literal #%plain-lambda) (RecName) . info-body)
             (get-extra-info #'τ_e)
      #:with info-unfolded (subst #'τ_e #'RecName #'info-body)
-     #:with ((_ _ Cons? [_ acc τ] ...) ...)
+     #: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
@@ -280,13 +272,11 @@
                   (equal? Cl (syntax->datum #'C))])
                 #'info-unfolded))
              (syntax->datum #'(Clause ...)))
-;;     #:fail-unless (id-set=? #'(Clause ...) #'(Cons ...)) "case clauses not exhaustive"
      ;; #:with ((acc ...) ...) (stx-map 
-     ;;                         (lambda (C fs) 
-     ;;                           (stx-map (lambda (f) (format-id C "~a-~a" C f)) fs)) 
-     ;;                         #'(Cons2 ...) 
-     ;;                         #'((fld ...) ...))
-;;     #:with (Cons? ...) (stx-map (lambda (C) (format-id C "~a?" C)) #'(Cons2 ...))
+     ;;                         (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)) ...)
@@ -308,9 +298,6 @@
             (let ([x- (acc z)] ...) e_c-)] ...))
           : τ_out)]))
 
-#;(define-syntax lifted→ ; wrap → with ∀
-  (syntax-parser
-    [(_ . rst) #'(∀ () (ext-stlc:→ . rst))]))
 (define-syntax → ; wrapping →
   (syntax-parser
     #;[(_ (~and Xs {X:id ...}) . rst)
diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt
index 4d8e1ba..560b992 100644
--- a/tapl/tests/mlish-tests.rkt
+++ b/tapl/tests/mlish-tests.rkt
@@ -25,6 +25,16 @@
   Nil
   (Cons X (List X)))
 
+(typecheck-fail 
+  (match (Cons 1 Nil) with
+   [Nil -> 1])
+  #:with-msg "match: clauses not exhaustive; missing: Cons")
+(typecheck-fail 
+  (match (Cons 1 Nil) with
+   [Cons x xs -> 1])
+  #:with-msg "match: clauses not exhaustive; missing: Nil")
+  
+
 (define (g2 [lst : (List Y)] → (List Y)) lst)
 (check-type g2 : (→ (List Y) (List Y)))
 (typecheck-fail (g2 1) 
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index b22705d..d97d8fb 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -2,7 +2,7 @@
 (require
   (for-syntax (except-in racket extends)
               syntax/parse racket/syntax syntax/stx racket/stxparam
-              syntax/parse/debug syntax/id-set
+              syntax/parse/debug
               "stx-utils.rkt")
   (for-meta 2 racket/base syntax/parse racket/syntax syntax/stx "stx-utils.rkt")
   (for-meta 3 racket/base syntax/parse racket/syntax)
@@ -12,7 +12,7 @@
  (except-out (all-from-out racket/base) #%module-begin)
  (for-syntax (all-defined-out)) (all-defined-out)
  (for-syntax
-  (all-from-out racket syntax/parse racket/syntax syntax/stx syntax/id-set
+  (all-from-out racket syntax/parse racket/syntax syntax/stx
                 "stx-utils.rkt"))
  (for-meta 2 (all-from-out racket/base syntax/parse racket/syntax)))
 
@@ -158,11 +158,6 @@
     (define ty (syntax-property stx tag))
     (if (cons? ty) (car ty) ty))
   
-  ;; fns for working with id sets
-  (define (id-set=? ids1 ids2)
-    (free-id-set=? (immutable-free-id-set (syntax->list ids1))
-                   (immutable-free-id-set (syntax->list ids2))))
-
   (define type-pat "[A-Za-z]+")
   
   ;; - infers type of e
@@ -562,13 +557,9 @@
                       (if (stx-null? #'extra-bvs)
                           #'extra-info
                           (substs #'τs- #'extra-bvs #'extra-info))
-               ;; #:with extra-info-inst (substs #'args #,#'extra-bvs #,#'extra-info)
-               #:with result
-                (assign-type (syntax/loc stx (τ-internal (λ bvs- (#%expression extra-info-inst) . τs-))) #'k_result)
-                #'result]
-                ;; #,(if (syntax-e #'other-key)
-                ;;     #`(syntax-property #'result 'other-key (substs #'args #,#'other-bvs #,#'other-val))
-                ;;     #'#'result)]
+                (assign-type 
+                  (syntax/loc stx (τ-internal (λ bvs- (#%expression extra-info-inst) . τs-))) 
+                  #'k_result)]
              ;; else fail with err msg
              [_
               (type-error #:src stx