diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
index f97dffe..de11e4d 100644
--- a/tapl/ext-stlc.rkt
+++ b/tapl/ext-stlc.rkt
@@ -78,7 +78,7 @@
 (define-syntax (begin/tc stx)
   (syntax-parse stx
     [(_ e_unit ... e)
-     #:with ((e_unit- τ_unit) ...) (infers+erase #'(e_unit ...))
+     #:with ([e_unit- τ_unit] ...) (infers+erase #'(e_unit ...))
      #:with (e- τ) (infer+erase #'e)
      #:fail-unless (stx-andmap Unit? #'(τ_unit ...))
                    (string-append
diff --git a/tapl/notes.txt b/tapl/notes.txt
index cb3b138..d947f77 100644
--- a/tapl/notes.txt
+++ b/tapl/notes.txt
@@ -1,3 +1,21 @@
+2015-07-31
+Problem: pattern-expander not being recognized
+Solution: syntax-parse pattern directives must begin with ~ prefix
+
+2015-07-30:
+Problem: How to match against an "expanded" type when I have an unexpanded pat?
+- use the 'orig syntax?
+  - this would probably work but now 'orig is used for more than debugging/msgs
+  - so dont do this
+  - also, wont work because you're only matching part of the type
+- use pattern expanders!
+  - a declared literal in define-type-constructor is defined as *both*:
+    - and macro that applies a temporary id (defined as void)
+    - a  pattern-expander that expands into the expanded form: 
+      ((~literal #%plain-app) (~literal tmp-id) . args)
+
+Note to self: when getting weird macro pattern matching errors, always check if you're accidentally using a pattern variable!
+
 2015-07-28
 Problem: How to handle mixed types, ie combining expanded and unexpanded types.
 Problem: When to eval, ie expand, types into canonical form
diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt
index 8239d24..8deef6e 100644
--- a/tapl/stlc+reco+var.rkt
+++ b/tapl/stlc+reco+var.rkt
@@ -1,13 +1,13 @@
 #lang racket/base
 (require "typecheck.rkt")
 (require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin tup proj let type=?))
-         (except-in "stlc+tup.rkt" #%app begin tup proj let type=?))
+         (except-in "stlc+tup.rkt" #%app begin tup proj let type=? ×))
 (provide (rename-out [stlc:#%app #%app] [stlc:let let] [stlc:begin begin]
                      [define/tc define]))
 (provide (except-out (all-from-out "stlc+tup.rkt")
                      stlc:#%app stlc:let stlc:begin stlc:tup stlc:proj
                      (for-syntax stlc:type=?)))
-(provide tup proj var case)
+(provide tup proj); var case)
 (provide (for-syntax type=?))
 
 
@@ -30,44 +30,65 @@
   ; extend to:
   ; 1) accept strings (ie, record labels)
   (define (type=? τ1 τ2)
+;    (printf "t1 = ~a\n" (syntax->datum τ1))
+;    (printf "t2 = ~a\n" (syntax->datum τ2))
     (syntax-parse (list τ1 τ2)
       [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
       [_ (stlc:type=? τ1 τ2)]))
 
   (current-type=? type=?)
-  (current-typecheck-relation (current-type=?)))
+  (current-typecheck-relation (current-type=?))
+
+  (define (same-types? τs)
+    (define τs-lst (syntax->list τs))
+    (or (null? τs-lst)
+        (andmap (λ (τ) ((current-type=?) (car τs-lst) τ)) (cdr τs-lst)))))
 
 (provide define-type-alias)
 (define-syntax define-type-alias
   (syntax-parser
     [(_ alias:id τ:type)
      ; must eval, otherwise undefined types will be allowed
-     #'(define-syntax alias (syntax-parser [x:id #'τ.norm]))]))
+     ;#'(define-syntax alias (syntax-parser [x:id #'τ.norm]))]))
+     #'(define-syntax alias (syntax-parser [x:id #'τ]))]))
 
-(define-type-constructor : #:arity 2)
+;(define-type-constructor [: str τ] #:lits (:))
+
+; re-define tuples as records
+(define-type-constructor
+  (× [~$ label τ_fld] ...) #:lits (~$)
+  #:declare label str
+  #:declare τ_fld type
+  )
+;  (× τ ...)
+;  #:declare τ type)
 
 ;; records
 (define-syntax (tup stx)
   (syntax-parse stx #:datum-literals (=)
     [(_ [l:str = e] ...)
-     #:with ((e- τ) ...) (infers+erase #'(e ...))
-     (⊢ #'(list (list l e-) ...) #'(× [: l τ] ...))]
-    [(_ e ...)
+     #:with ([e- τ] ...) (infers+erase #'(e ...))
+     (⊢ (list (list l e-) ...) : (× [~$ l τ] ...))]
+    #;[(_ e ...)
      #'(stlc:tup e ...)]))
 (define-syntax (proj stx)
   (syntax-parse stx #:literals (quote)
     [(_ rec l:str ~!)
-     #:with (rec- τ_rec) (infer+erase #'rec)
-     #:fail-unless (×? #'τ_rec) (format "not record type: ~a" (syntax->datum #'τ_rec))
-     #:with (['l_τ:str τ] ...) (stx-map :-args (×-args #'τ_rec))
+     #:with [rec- τ_rec] (infer+erase #'rec)
+;     #:when (printf "inferred type: ~a\n" (syntax->datum #'τ_rec))
+;     #:when (printf "inferred type eval ~a\n" (syntax->datum ((current-type-eval) #'τ_rec)))
+     #:with ('l_τ:str ...) (×-get label from τ_rec)
+     #:with (τ ...) (×-get τ_fld from τ_rec)
+;     #:fail-unless (×? #'τ_rec) (format "not record type: ~a" (syntax->datum #'τ_rec))
+;     #:with (['l_τ:str τ] ...) (stx-map :-args (×-args #'τ_rec))
      #:with (l_match:str τ_match) (str-stx-assoc #'l #'([l_τ τ] ...))
-     (⊢ #'(cadr (assoc l rec)) #'τ_match)]
-    [(_ e ...) #'(stlc:proj e ...)]))
+     (⊢ (cadr (assoc l rec)) : τ_match)]
+    #;[(_ e ...) #'(stlc:proj e ...)]))
 
 
-(define-type-constructor ∨)
+#;(define-type-constructor (∨ [: label τ] ...))
 
-(define-syntax (var stx)
+#;(define-syntax (var stx)
   (syntax-parse stx #:datum-literals (as =) #:literals (quote)
     [(_ l:str = e as τ:type)
      #:when (∨? #'τ.norm)
@@ -76,7 +97,7 @@
      #:with (e- τ_e) (infer+erase #'e)
      #:when (typecheck? #'τ_e #'τ_match)
      (⊢ #'(list l e) #'τ.norm)]))
-(define-syntax (case stx)
+#;(define-syntax (case stx)
   (syntax-parse stx #:datum-literals (of =>) #:literals (quote)
     [(_ e [l:str x => e_l] ...)
      #:fail-when (null? (syntax->list #'(l ...))) "no clauses"
diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt
index 31218c1..1b2c3c4 100644
--- a/tapl/stlc+tup.rkt
+++ b/tapl/stlc+tup.rkt
@@ -14,18 +14,17 @@
 ;; - terms from ext-stlc.rkt
 ;; - tup and proj
 
-(define-type-constructor ×)
+(define-type-constructor (× τ ...) #:declare τ type)
 
 (define-syntax (tup stx)
   (syntax-parse stx
     [(_ e ...)
-     #:with ((e- τ) ...) (infers+erase #'(e ...))
-     (⊢ #'(list e- ...) #'(× τ ...))]))
+     #:with ([e- τ] ...) (infers+erase #'(e ...))
+     (⊢ (list e- ...) : (× τ ...))]))
 (define-syntax (proj stx)
   (syntax-parse stx
-    [(_ tup n:integer)
-     #:with (tup- τ_tup) (infer+erase #'tup)
-     #:fail-unless (×? #'τ_tup) "not tuple type"
-     #:fail-unless (< (syntax-e #'n) (×-num-args #'τ_tup)) "proj index too large"
-     (⊢ #'(list-ref tup n) (×-ref #'τ_tup (syntax-e #'n)))]))
+    [(_ e_tup n:integer)
+     #:with [e_tup- τs_tup] (×-match+erase #'e_tup)
+     #:fail-unless (< (syntax-e #'n) (stx-length #'τs_tup)) "proj index too large"
+     (⊢ (list-ref e_tup- n) : #,(stx-list-ref #'τs_tup (syntax-e #'n)))]))
    
\ No newline at end of file
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
index 125a69e..e59d7fc 100644
--- a/tapl/stlc.rkt
+++ b/tapl/stlc.rkt
@@ -61,6 +61,9 @@
 (define-syntax (app/tc stx)
   (syntax-parse stx
     [(_ e_fn e_arg ...)
+;     #:with [e_fn- τ_fn] (infer+erase #'e_fn)
+;     #:with (τ_in ...) (→-get τ_in from #'τ_fn)
+;     #:with τ_out (→-get τ_out from #'τ_fn)
      #:with [e_fn- (τ_in ... τ_out)] (→-match+erase #'e_fn)
      #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
      #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
diff --git a/tapl/tests/ext-stlc-tests.rkt b/tapl/tests/ext-stlc-tests.rkt
index e7db535..443b03f 100644
--- a/tapl/tests/ext-stlc-tests.rkt
+++ b/tapl/tests/ext-stlc-tests.rkt
@@ -112,9 +112,10 @@
  #:with-msg
  "Arguments to function.+have wrong type.+Given:.+Int.+Expected:.+Bool")
 ;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
-(typecheck-fail (λ ([f : Int]) (f 1 2))
-                #:with-msg
-                "Expected type with pattern: \\(→ τ_in ... τ_out\\), got: Int")
+(typecheck-fail
+ (λ ([f : Int]) (f 1 2))
+ #:with-msg
+ "Expected type of expression f to match pattern \\(→ τ_in ... τ_out\\), got: Int")
 
 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
             : (→ (→ Int Int Int) Int Int Int))
diff --git a/tapl/tests/stlc+reco+var-tests.rkt b/tapl/tests/stlc+reco+var-tests.rkt
index 241a42d..bbf8835 100644
--- a/tapl/tests/stlc+reco+var-tests.rkt
+++ b/tapl/tests/stlc+reco+var-tests.rkt
@@ -12,10 +12,13 @@
 (check-type + : ArithBinOp)
 (check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int))
 
-;; records (ie labeled tuples)
+; records (ie labeled tuples)
 (check-type "Stephen" : String)
+(check-type (tup) : (×))
+(check-type (tup ["name" = "Stephen"]) : (× [~$ "name" String]))
+(check-type (proj (tup ["name" = "Stephen"]) "name") : String ⇒ "Stephen")
 (check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-            (× [: "name" String] [: "phone" Int] [: "male?" Bool]))
+            (× [~$ "name" String] [~$ "phone" Int] [~$ "male?" Bool]))
 (check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
             : String ⇒ "Stephen")
 (check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
@@ -25,157 +28,157 @@
 (check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
             : Bool ⇒ #t)
 (check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-                (× [: "my-name" String] [: "phone" Int] [: "male?" Bool]))
+                (× [~$ "my-name" String] [~$ "phone" Int] [~$ "male?" Bool]))
 (check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-                (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
+                (× [~$ "name" String] [~$ "my-phone" Int] [~$ "male?" Bool]))
 (check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-                (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
+                (× [~$ "name" String] [~$ "phone" Int] [~$ "is-male?" Bool]))
 
 ;; variants
-(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit]))
-(check-not-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit]))
-(typecheck-fail ((λ ([x : (∨ [: "coffee" Unit] [: "tea" Unit])]) x)
-                 (var "coffee" = (void) as (∨ [: "coffee" Unit]))))
-(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit]))
-(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit]))
-            : (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit]))
+;(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit]))
+;(check-not-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit]))
+;(typecheck-fail ((λ ([x : (∨ [: "coffee" Unit] [: "tea" Unit])]) x)
+;                 (var "coffee" = (void) as (∨ [: "coffee" Unit]))))
+;(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit]))
+;(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit]))
+;            : (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit]))
+;
+;(typecheck-fail
+; (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
+;   ["coffee" x => 1])) ; not enough clauses
+;(typecheck-fail
+; (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
+;   ["coffee" x => 1]
+;   ["teaaaaaa" x => 2])) ; wrong clause
+;(typecheck-fail
+; (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
+;   ["coffee" x => 1]
+;   ["tea" x => 2]
+;   ["coke" x => 3])) ; too many clauses
+;(typecheck-fail
+; (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
+;   ["coffee" x => "1"]
+;   ["tea" x => 2])) ; mismatched branch types
+;(check-type
+; (case (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit]))
+;   ["coffee" x => x]
+;   ["tea" x => 2]) : Int ⇒ 1)
+;(define-type-alias Drink (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool]))
+;(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+;(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
+;(check-type
+; (case ((λ ([d : Drink]) d)
+;        (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool])))
+;   ["coffee" x => (+ (+ x x) (+ x x))]
+;   ["tea" x => 2]
+;   ["coke" y => 3])
+; : Int ⇒ 4)
+;
+;(check-type
+; (case ((λ ([d : Drink]) d) (var "coffee" = 1 as Drink))
+;   ["coffee" x => (+ (+ x x) (+ x x))]
+;   ["tea" x => 2]
+;   ["coke" y => 3])
+; : Int ⇒ 4)
 
-(typecheck-fail
- (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
-   ["coffee" x => 1])) ; not enough clauses
-(typecheck-fail
- (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
-   ["coffee" x => 1]
-   ["teaaaaaa" x => 2])) ; wrong clause
-(typecheck-fail
- (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
-   ["coffee" x => 1]
-   ["tea" x => 2]
-   ["coke" x => 3])) ; too many clauses
-(typecheck-fail
- (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
-   ["coffee" x => "1"]
-   ["tea" x => 2])) ; mismatched branch types
-(check-type
- (case (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit]))
-   ["coffee" x => x]
-   ["tea" x => 2]) : Int ⇒ 1)
-(define-type-alias Drink (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool]))
-(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
-(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
-(check-type
- (case ((λ ([d : Drink]) d)
-        (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool])))
-   ["coffee" x => (+ (+ x x) (+ x x))]
-   ["tea" x => 2]
-   ["coke" y => 3])
- : Int ⇒ 4)
-
-(check-type
- (case ((λ ([d : Drink]) d) (var "coffee" = 1 as Drink))
-   ["coffee" x => (+ (+ x x) (+ x x))]
-   ["tea" x => 2]
-   ["coke" y => 3])
- : Int ⇒ 4)
-
-;; previous tests: ------------------------------------------------------------
-;; tests for tuples -----------------------------------------------------------
-(check-type (tup 1 2 3) : (× Int Int Int))
-(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int)))
-(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int)))
-(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int)))
-(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int)))
-(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit)))
-
-(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1)
-(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2")
-(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f)
-(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large
-(typecheck-fail (proj 1 2)) ; not tuple
+;; previous tuple tests: ------------------------------------------------------------
+;; wont work anymore
+;(check-type (tup 1 2 3) : (× Int Int Int))
+;(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int)))
+;(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int)))
+;(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int)))
+;(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int)))
+;(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit)))
+;
+;(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1)
+;(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2")
+;(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f)
+;(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large
+;(typecheck-fail (proj 1 2)) ; not tuple
 
 ;; ext-stlc.rkt tests ---------------------------------------------------------
 ;; should still pass
 
 ;; new literals and base types
-(check-type "one" : String) ; literal now supported
-(check-type #f : Bool) ; literal now supported
-
-(check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type
-
-;; Unit
-(check-type (void) : Unit)
-(check-type void : (→ Unit))
-(typecheck-fail ((λ ([x : Unit]) x) 2))
-(typecheck-fail ((λ ([x : Unit])) void))
-(check-type ((λ ([x : Unit]) x) (void)) : Unit)
-
-;; begin
-(typecheck-fail (begin))
-(check-type (begin 1) : Int)
-(typecheck-fail (begin 1 2 3))
-(check-type (begin (void) 1) : Int ⇒ 1)
-
-;;ascription
-(typecheck-fail (ann 1 : Bool))
-(check-type (ann 1 : Int) : Int ⇒ 1)
-(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
-
-; let
-(check-type (let () (+ 1 1)) : Int ⇒ 2)
-(check-type (let ([x 10]) (+ 1 2)) : Int)
-(typecheck-fail (let ([x #f]) (+ x 1)))
-(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
-(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier
-
-(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
-(typecheck-fail (let* ([x #t] [y (+ x 1)]) 1))
-
-; letrec
-(typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y))
-(typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x))
-
-(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
-
-;; recursive
-(check-type
- (letrec ([(countdown : (→ Int String))
-           (λ ([i : Int])
-             (if (= i 0)
-                 "liftoff"
-                 (countdown (- i 1))))])
-   (countdown 10)) : String ⇒ "liftoff")
-
-;; mutually recursive
-(check-type
- (letrec ([(is-even? : (→ Int Bool))
-           (λ ([n : Int])
-             (or (zero? n)
-                 (is-odd? (sub1 n))))]
-          [(is-odd? : (→ Int Bool))
-           (λ ([n : Int])
-             (and (not (zero? n))
-                  (is-even? (sub1 n))))])
-   (is-odd? 11)) : Bool ⇒ #t)
-
-;; tests from stlc+lit-tests.rkt --------------------------
-; most should pass, some failing may now pass due to added types/forms
-(check-type 1 : Int)
-;(check-not-type 1 : (Int → Int))
-;(typecheck-fail "one") ; literal now supported
-;(typecheck-fail #f) ; literal now supported
-(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
-(check-not-type (λ ([x : Int]) x) : Int)
-(check-type (λ ([x : Int]) x) : (→ Int Int))
-(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
-(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
-(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool now valid type, but arg has wrong type
-;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
-(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
-(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
-            : (→ (→ Int Int Int) Int Int Int))
-(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
-(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
-(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
-(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
-(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
-
+;(check-type "one" : String) ; literal now supported
+;(check-type #f : Bool) ; literal now supported
+;
+;(check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type
+;
+;;; Unit
+;(check-type (void) : Unit)
+;(check-type void : (→ Unit))
+;(typecheck-fail ((λ ([x : Unit]) x) 2))
+;(typecheck-fail ((λ ([x : Unit])) void))
+;(check-type ((λ ([x : Unit]) x) (void)) : Unit)
+;
+;;; begin
+;(typecheck-fail (begin))
+;(check-type (begin 1) : Int)
+;(typecheck-fail (begin 1 2 3))
+;(check-type (begin (void) 1) : Int ⇒ 1)
+;
+;;;ascription
+;(typecheck-fail (ann 1 : Bool))
+;(check-type (ann 1 : Int) : Int ⇒ 1)
+;(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
+;
+;; let
+;(check-type (let () (+ 1 1)) : Int ⇒ 2)
+;(check-type (let ([x 10]) (+ 1 2)) : Int)
+;(typecheck-fail (let ([x #f]) (+ x 1)))
+;(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
+;(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier
+;
+;(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
+;(typecheck-fail (let* ([x #t] [y (+ x 1)]) 1))
+;
+;; letrec
+;(typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y))
+;(typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x))
+;
+;(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
+;
+;;; recursive
+;(check-type
+; (letrec ([(countdown : (→ Int String))
+;           (λ ([i : Int])
+;             (if (= i 0)
+;                 "liftoff"
+;                 (countdown (- i 1))))])
+;   (countdown 10)) : String ⇒ "liftoff")
+;
+;;; mutually recursive
+;(check-type
+; (letrec ([(is-even? : (→ Int Bool))
+;           (λ ([n : Int])
+;             (or (zero? n)
+;                 (is-odd? (sub1 n))))]
+;          [(is-odd? : (→ Int Bool))
+;           (λ ([n : Int])
+;             (and (not (zero? n))
+;                  (is-even? (sub1 n))))])
+;   (is-odd? 11)) : Bool ⇒ #t)
+;
+;;; tests from stlc+lit-tests.rkt --------------------------
+;; most should pass, some failing may now pass due to added types/forms
+;(check-type 1 : Int)
+;;(check-not-type 1 : (Int → Int))
+;;(typecheck-fail "one") ; literal now supported
+;;(typecheck-fail #f) ; literal now supported
+;(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
+;(check-not-type (λ ([x : Int]) x) : Int)
+;(check-type (λ ([x : Int]) x) : (→ Int Int))
+;(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
+;(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+;(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool now valid type, but arg has wrong type
+;;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
+;(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+;(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
+;            : (→ (→ Int Int Int) Int Int Int))
+;(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+;(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+;(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
+;(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+;(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+;
diff --git a/tapl/tests/stlc+tup-tests.rkt b/tapl/tests/stlc+tup-tests.rkt
index e022aec..04882c2 100644
--- a/tapl/tests/stlc+tup-tests.rkt
+++ b/tapl/tests/stlc+tup-tests.rkt
@@ -12,8 +12,11 @@
 (check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1)
 (check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2")
 (check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f)
-(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large
-(typecheck-fail (proj 1 2)) ; not tuple
+(typecheck-fail (proj (tup 1 "2" #f) 3) #:with-msg "index too large")
+(typecheck-fail
+ (proj 1 2)
+ #:with-msg
+ "Expected type of expression 1 to match pattern \\(× τ ...\\), got: Int")
 
 ;; ext-stlc.rkt tests ---------------------------------------------------------
 ;; should still pass
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index 2eae75d..3cec434 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -2,8 +2,10 @@
 (require
   (for-syntax (except-in racket extends)
               syntax/parse racket/syntax syntax/stx
-              "stx-utils.rkt")
+              "stx-utils.rkt"
+              syntax/parse/debug)
   (for-meta 2 racket/base syntax/parse racket/syntax)
+  (for-meta 3 racket/base syntax/parse racket/syntax)
   racket/provide)
 (provide 
  (for-syntax (all-defined-out)) (all-defined-out)
@@ -118,11 +120,13 @@
                           (format "Type error: expected ~a type, got ~a"
                                   (type->str #'τ) (type->str ty))
             #'args]
-           [_ #f])])))
+           [_ #f])]))
+)
 
 (define-syntax define-type-constructor
   (syntax-parser
     [(_ (τ:id . pat)
+        ; lits must have ~ prefix (for syntax-parse compat) for now
         (~optional (~seq #:lits (lit ...)) #:defaults ([(lit 1) null]))
         decls ...
         #;(~optional (~seq (~seq #:decl tvar (~datum as) cls) ...)
@@ -133,15 +137,43 @@
      #:with τ-match+erase (format-id #'τ "~a-match+erase" #'τ)
      #:with pat-class (generate-temporary #'τ) ; syntax-class name
      #:with tycon (generate-temporary #'τ) ; need a runtime id for expansion
+     #:with (lit-tmp ...) (generate-temporaries #'(lit ...))
      #`(begin
-         (define lit void) ...
+         ;; list can't be function, ow it will use typed #%app
+         ;; define lit as macro that expands into #%app,
+         ;; so it will use the #%app here (racket's #%app)
+         (define lit-tmp void) ...
+         (define-syntax lit (syntax-parser [(_ . xs) #'(lit-tmp . xs)])) ...
+         (provide lit ...)
          (provide τ)
          (begin-for-syntax
-           (define-syntax-class pat-class #:literals (lit ...)
+           (define-syntax lit
+             (pattern-expander
+              (syntax-parser
+                [(_ . xs)
+                 ;#:when (displayln "pattern expanding")
+                 #'((~literal #%plain-app) (~literal lit-tmp) . xs)]))) ...
+           (define-syntax-class pat-class
              ;; dont check is-type? here; should already be types
              ;; only check is-type? for user-entered types, eg tycon call
              ;; thus, dont include decls here, only want shape
-             (pattern pat))
+             #;(pattern (~and pre (~do (printf "trying to match: ~a\n"(syntax->datum  #'pre))) pat (~do (displayln "no")))) ; uses "lit" pattern expander
+             (pattern pat)
+             #;(pattern any
+                      #:when (printf "trying to match: ~a\n" (syntax->datum #'any))
+                      #:when (printf "orig: ~a\n" (type->str #'any))
+                      #:when (printf "against pattern: ~a\n" (syntax->datum (quote-syntax pat)))
+                      #:when (displayln #`(#,(stx-cdr (stx-car #'any))))
+                      #:when (pretty-print (debug-parse #`(#,(stx-cdr (stx-car #'any))) pat))
+                      #:with pat #'any) ;#`(#,(stx-cdr (stx-car #'any))))
+             #;(pattern any
+                      #:when (displayln "match failed")
+                      #:when (displayln "pat: ")
+                      #:when (displayln (quote-syntax pat))
+                      #:when (displayln #'any)
+                      #:when (displayln "orig")
+                      #:when (displayln (type->str #'any))
+                      #:with pat #'any))
            (define (τ-match ty)
              (or (match-type ty tycon pat-class)
                  ;; error msg should go in specific macro def?
@@ -167,12 +199,12 @@
                [(_ attr from ty)
                 #:with args (generate-temporary)
                 #:with args.attr (format-id #'args "~a.~a" #'args #'attr)
-                #'(syntax-parse ((current-type-eval) ty)
-                    [((~literal #%plain-type) ((~literal #%plain-app) t . args))
+                #'(syntax-parse ((current-type-eval) #'ty)
+                    [((~literal #%plain-type) ((~literal #%plain-app) (~literal tycon) . args))
                      #:declare args pat-class ; check shape of arguments
-                     #:fail-unless (typecheck? #'t #'tycon) ; check tycons match
-                                   (format "Type error: expected ~a type, got ~a"
-                                           (type->str #'τ) (type->str ty))
+;                     #:fail-unless (typecheck? #'t #'tycon) ; check tycons match
+;                                   (format "Type error: expected ~a type, got ~a"
+;                                           (type->str #'τ) (type->str #'ty))
                      (attribute args.attr)])])))
          (define tycon (λ _ (raise (exn:fail:type:runtime
                                     (format "~a: Cannot use type at run time" 'τ)
@@ -182,12 +214,21 @@
              [(_ . (~and pat !~ args)) ; first check shape
               ; this inner syntax-parse gets the ~! to register
               ; otherwise, apparently #:declare's get subst into pat (before ~!)
-              (syntax-parse #'args
+              (syntax-parse #'args #:literals (lit ...)
                 [pat #,@#'(decls ...) ; then check declarations (eg, valid type)
                  #'(#%type (tycon . args))])]
-             [_ (type-error #:src stx
-                            #:msg "Improper usage of type constructor ~a: ~a, expected pattern ~a"
-                            #'τ stx (quote-syntax (τ . pat)))])))]))
+             [_
+              (type-error #:src stx
+                          #:msg (string-append
+                                 "Improper usage of type constructor ~a: ~a, expected pattern ~a, "
+                                 #;(format
+                                  "where: ~a"
+                                  (string-join
+                                   (stx-map
+                                    (λ (typ clss) (format "~a is a ~a" typ clss))
+                                    #'(ty (... ...)) #'(cls (... ...)))
+                                   ", ")))
+                          #'τ stx (quote-syntax (τ . pat)))])))]))
 
 ;; TODO: refine this to enable specifying arity information
 ;; type constructors currently must have 1+ arguments