diff --git a/tapl/exist.rkt b/tapl/exist.rkt
index ebc9f91..4254371 100644
--- a/tapl/exist.rkt
+++ b/tapl/exist.rkt
@@ -1,12 +1,13 @@
 #lang racket/base
 (require "typecheck.rkt")
 (require (except-in "stlc+reco+var.rkt" #%app λ let type=?)
-         (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ let type=?))
-         (prefix-in sysf: (only-in "sysf.rkt" type=?)))
+         (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ let #;type=?))
+         (only-in "stlc+rec-iso.rkt" type=?))
 (provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let])
-         (for-syntax type=?))
+         #;(for-syntax type=?))
 (provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app stlc:λ stlc:let
-                     (for-syntax stlc:type=?)))
+                     #;(for-syntax stlc:type=?))
+         (all-from-out "stlc+rec-iso.rkt"))
 (provide ∃ pack open)
 
 ;; existential types
@@ -18,25 +19,43 @@
 ;; - terms from stlc+reco+var.rkt
 ;; - pack and open
 
-(begin-for-syntax
+#;(begin-for-syntax
   (define (type=? t1 t2)
     (or (stlc:type=? t1 t2)
         (sysf:type=? t1 t2)))
   (current-type=? type=?)
   (current-typecheck-relation type=?))
 
-;; TODO: disambiguate expanded representation of ∃, ok to use lambda in this calculus
-(define-type-constructor (∃ [[X]] τ_body))
-;(provide ∃)
-;(define-syntax (∃ stx)
-;  (syntax-parse stx
-;    [(_ (tv:id) body)
-;     (syntax/loc stx (#%plain-lambda (tv) body))]))
+
+#;(define-type-constructor (∃ [[X]] τ_body))
+; this is exactly the same as μ
+(define-syntax ∃
+  (syntax-parser
+    [(_ (tv:id) τ_body)
+     #:with ((tv-) τ_body- k) (infer/ctx+erase #'([tv : #%type]) #'τ_body)
+     #:when (#%type? #'k)
+     (mk-type #'(λ (tv-) τ_body-))]))
+(begin-for-syntax
+  (define (infer∃+erase e)
+    (syntax-parse (infer+erase e) #:context e
+      [(e- τ_e)
+       #:with ((~literal #%plain-lambda) (tv) τ) #'τ_e
+       #'(e- (tv τ))]))
+  (define-syntax ~∃*
+    (pattern-expander
+     (syntax-parser
+       [(_ (tv:id) τ)
+        #'(~or
+           ((~literal #%plain-lambda) (tv) τ)
+           (~and any (~do
+                      (type-error
+                       #:src #'any
+                       #:msg "Expected ∃ type, got: ~a" #'any))))]))))
 
 (define-syntax (pack stx)
   (syntax-parse stx
     [(_ (τ:type e) as ∃τ:type)
-     #:with (~∃ [[τ_abstract]] τ_body) #'∃τ.norm
+     #:with (~∃* (τ_abstract) τ_body) #'∃τ.norm
 ;     #:with (#%plain-lambda (τ_abstract:id) τ_body) #'∃τ.norm
      #:with [e- τ_e] (infer+erase #'e)
      #:when (typecheck? #'τ_e  (subst #'τ.norm #'τ_abstract #'τ_body))
@@ -45,7 +64,7 @@
 (define-syntax (open stx)
   (syntax-parse stx #:datum-literals (<=)
     [(_ ([(tv:id x:id) <= e_packed]) e)
-     #:with [e_packed- (~∃ [[τ_abstract]] τ_body)] (infer+erase #'e_packed)
+     #:with [e_packed- (τ_abstract τ_body)] (infer∃+erase #'e_packed)
 ;     #:with [e_packed- τ_packed] (infer+erase #'e_packed)
 ;     #:with (#%plain-lambda (τ_abstract:id) τ_body) #'τ_packed ; existential
      ;; The subst below appears to be a hack, but it's not really.
@@ -91,7 +110,6 @@
      ;; ------------------------------
      ;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
      ;;
-     #:with [tvs- (x-) (e-) (τ_e)]
-            (infer #'(e) #:ctx #`([x : #,(subst #'tv #'τ_abstract #'τ_body)])
-                         #:tvs #'(tv))
+     #:with [_ (x-) (e-) (τ_e)]
+            (infer #'(e) #:tvctx #'([tv : #%type]) #:ctx #`([x : #,(subst #'tv #'τ_abstract #'τ_body)]))
      (⊢ (let ([x- e_packed-]) e-) : τ_e)]))
\ No newline at end of file
diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
index ebb4fa2..abb2bc0 100644
--- a/tapl/ext-stlc.rkt
+++ b/tapl/ext-stlc.rkt
@@ -74,7 +74,10 @@
 ;     #:fail-unless (Bool? #'τ_tst) (format "given non-Bool test: ~a\n" (syntax->datum #'e_tst))
      #:with (e1- τ1) (infer+erase #'e1)
      #:with (e2- τ2) (infer+erase #'e2)
-     #:when ((current-type=?) #'τ1 #'τ2)
+     #:fail-unless (or ((current-typecheck-relation) #'τ1 #'τ2)
+                       ((current-typecheck-relation) #'τ2 #'τ1))
+                   (format "branches must have the same type: given ~a and ~a"
+                           (type->str #'τ1) (type->str #'τ2))
      (⊢ (if e_tst- e1- e2-) : τ1)]))
 
 (define-base-type Unit)
@@ -83,24 +86,25 @@
 (define-syntax (begin/tc stx)
   (syntax-parse stx
     [(_ e_unit ... e)
-     #:with ([e_unit- τ_unit] ...) (infers+erase #'(e_unit ...))
+     #:with (e_unit- ...) (stx-map inferUnit+erase #'(e_unit ...))
+;     #:with ([e_unit- τ_unit] ...) (infers+erase #'(e_unit ...))
+;     #:fail-unless (stx-andmap Unit? #'(τ_unit ...))
+;                   (string-append
+;                    "all begin expressions except the last one should have type Unit\n"
+;                    (string-join
+;                     (stx-map
+;                      (λ (e τ) (format "~a : ~a" (syntax->datum e) (syntax->datum τ)))
+;                      #'(e_unit ...) #'(τ_unit ...))
+;                     "\n")
+;                    "\n")
      #:with (e- τ) (infer+erase #'e)
-     #:fail-unless (stx-andmap Unit? #'(τ_unit ...))
-                   (string-append
-                    "all begin expressions except the last one should have type Unit\n"
-                    (string-join
-                     (stx-map
-                      (λ (e τ) (format "~a : ~a" (syntax->datum e) (syntax->datum τ)))
-                      #'(e_unit ...) #'(τ_unit ...))
-                     "\n")
-                    "\n")
      (⊢ (begin e_unit- ... e-) : τ)]))
 
 (define-syntax (ann stx)
   (syntax-parse stx #:datum-literals (:)
-    [(_ e : ascribed-τ)
+    [(_ e : ascribed-τ:type)
      #:with (e- τ) (infer+erase #'e)
-     #:fail-unless (typecheck? #'τ #'ascribed-τ)
+     #:fail-unless (typecheck? #'τ #'ascribed-τ.norm)
                    (format "~a does not have type ~a\n"
                            (syntax->datum #'e) (syntax->datum #'ascribed-τ))
      (⊢ e- : ascribed-τ)]))
@@ -123,7 +127,7 @@
     [(_ ([b:typed-binding e] ...) e_body)
      #:with ((x- ...) (e- ... e_body-) (τ ... τ_body))
             (infers/type-ctxt+erase #'(b ...) #'(e ... e_body))
-     #:fail-unless (typechecks? #'(b.τ ...) #;(type-evals #'(b.τ ...)) #'(τ ...))
+     #:fail-unless (typechecks? #'(b.τ ...) #'(τ ...))
                    (string-append
                     "type check fail, args have wrong type:\n"
                     (string-join
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
index 8bb25f0..c0875c3 100644
--- a/tapl/fomega.rkt
+++ b/tapl/fomega.rkt
@@ -1,7 +1,8 @@
 #lang racket/base
 (require "typecheck.rkt")
 (require (except-in "sysf.rkt" #%app λ Int #%datum → Λ inst ∀  + type-eval)
-         (prefix-in sysf: (only-in "sysf.rkt" #%app λ Int → ∀ type-eval)))
+         (prefix-in sysf: (only-in "sysf.rkt" #%app λ Int → ∀ type-eval))
+         (only-in "stlc+reco+var.rkt" same-types?))
 (provide (rename-out [app/tc #%app] [λ/tc λ] [datum/tc #%datum]))
 (provide (except-out (all-from-out "sysf.rkt")
                      sysf:Int sysf:→ sysf:∀
@@ -21,8 +22,7 @@
 (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 #'τ]))]))
 
 (begin-for-syntax
   ;; extend type-eval to handle tyapp
@@ -49,7 +49,7 @@
   (current-type-eval type-eval))
 
 (define-base-type ★)
-(define-type-constructor ⇒)
+(define-type-constructor (⇒ k_in ... k_out))
 
 ;; for now, handle kind checking in the types themselves
 ;; TODO: move kind checking to a common place (like #%app)?
@@ -59,8 +59,8 @@
 ;; so I dont have to manually add kinds to all types
 (define-base-type Str)
 (provide String)
-(define-syntax String (syntax-parser [x:id (⊢ #'Str #'★)]))
-(define-syntax Int (syntax-parser [x:id (⊢ #'sysf:Int #'★)]))
+(define-syntax String (syntax-parser [x:id (⊢ Str : ★)]))
+(define-syntax Int (syntax-parser [x:id (⊢ sysf:Int : ★)]))
 
 ;; → in Fω is not first-class, can't pass it around
 (define-syntax (→ stx)
@@ -69,20 +69,24 @@
      #:with ([τ- k] ... [τ_res- k_res]) (infers+erase #'(τ ... τ_res))
      #:when (typecheck? #'k_res #'★)
      #:when (same-types? #'(k ... k_res))
-     (⊢ #'(sysf:→ τ- ... τ_res-) #'★)]))
+     (⊢ (sysf:→ (#%plain-type τ-) ... (#%plain-type τ_res-)) : ★)]))
 
 (define-syntax (∀ stx)
   (syntax-parse stx
     [(∀ (b:typed-binding ...) τ)
-     #:with (tvs- τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
+     #:with ((tv- ...) τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
      #:when (typecheck? #'k #'★)
-     (⊢ #'(#%plain-lambda tvs- b.τ ... τ-) #;#'(sysf:∀ tvs- τ-) #'★)]))
+     (⊢ (#%type
+         (λ (tv- ...)
+          (let-syntax ([tv- (syntax-parser [tv-:id #'(#%type tv-)])] ...)
+           b.τ ... τ-))) #;(sysf:∀ #:bind tvs- τ-) : ★)]))
 
 (define-syntax (Λ stx)
   (syntax-parse stx
     [(_ (b:typed-binding ...) e)
      #:with ((tv- ...) e- τ) (infer/type-ctxt+erase #'(b ...) #'e)
-     (⊢ #'e- #'(∀ ([tv- : b.τ] ...) τ))]))
+     #:when (displayln #'(∀ ([tv- : b.τ] ...) τ))
+     (⊢ e- : (∀ ([tv- : b.τ] ...) τ))]))
 (define-syntax (inst stx)
   (syntax-parse stx
     [(_ e τ:type ...)
@@ -90,7 +94,7 @@
      #:with (e- ∀τ) (infer+erase #'e)
      #:with ((~literal #%plain-lambda) (tv ...) k_tv ... τ_body) #'∀τ
      #:when (typechecks? #'(k ...) #'(k_tv ...))
-     (⊢ #'e- (substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
+     (⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
 
 ;; TODO: merge with regular λ and app?
 (define-syntax (tyλ stx)
@@ -98,47 +102,63 @@
     [(_ (b:typed-binding ...) τ)
      #:with (tvs- τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
      ;; b.τ's here are actually kinds
-     (⊢ #'(λ tvs- τ-) #'(⇒ b.τ ... k))]))
+     (⊢ (λ tvs- τ-) : (⇒ b.τ ... k))]))
 
 (define-syntax (tyapp stx)
   (syntax-parse stx
     [(_ τ_fn τ_arg ...)
-     #:with [τ_fn- k_fn] (infer+erase #'τ_fn)
-     #:fail-unless (⇒? #'k_fn)
-                   (format "Kind error: Attempting to apply a non-tyλ with kind ~a\n"
-                           (syntax->datum #'τ_fn) (syntax->datum #'k_fn))
-     #:with ((~literal #%plain-app) _ k ... k_res) #'k_fn
+     #:with [τ_fn- (~⇒* k_in ... k_out)] (infer+erase #'τ_fn)
+;     #:fail-unless (⇒? #'k_fn)
+;                   (format "Kind error: Attempting to apply a non-tyλ with kind ~a\n"
+;                           (syntax->datum #'τ_fn) (syntax->datum #'k_fn))
+;     #:with ((~literal #%plain-app) _ k ... k_res) #'k_fn
      #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...))
-     #:fail-unless (stx-length=? #'(k_arg ...) #'(k ...))
+     #:fail-unless (typechecks? #'(k_arg ...) #'(k_in ...))
                    (string-append
-                    (format
-                     "Wrong number of args given to tyλ ~a:\ngiven: "
-                     (syntax->datum #'τ_fn))
+                    (format "~a (~a:~a) Arguments to function ~a have wrong kinds(s), "
+                            (syntax-source stx) (syntax-line stx) (syntax-column stx)
+                            (syntax->datum #'τ_fn))
+                    "or wrong number of arguments:\nGiven:\n"
                     (string-join
-                     (map
-                      (λ (t k) (format "~a : ~a" t k))
-                      (syntax->datum #'(τ_arg ...))
-                      (syntax->datum #`#,(stx-map get-orig #'(k_arg ...))))
-                     ", ")
-                    (format "\nexpected: ~a argument(s)." (stx-length #'(k ...))))
-     #:fail-unless (typechecks? #'(k_arg ...) #'(k ...))
-                   (string-append
-                    (format
-                     "Arguments to tyλ ~a have wrong type:\ngiven: "
-                     (syntax->datum #'τ_fn))
-                    (string-join
-                     (map
-                      (λ (t k) (format "~a : ~a" t k))
-                      (syntax->datum #'(τ_arg ...))
-                      (syntax->datum #`#,(stx-map get-orig #'(k_arg ...))))
-                     ", ")
-                    "\nexpected arguments with type: "
-                    (string-join
-                     (map ~a (syntax->datum #`#,(stx-map get-orig #'(k ...))))
-                     ", "))
-      ;; cant do type-subst here bc τ_fn might be a (forall) tyvar
-      ;#:with τ_res ((current-type-eval) #'(tyapply τ_fn- τ_arg- ...))
-     (⊢ #'(#%app τ_fn- τ_arg- ...) #'k_res)]))
+                     (map (λ (e t) (format "  ~a : ~a" e t)) ; indent each line
+                          (syntax->datum #'(τ_arg ...))
+                          (stx-map type->str #'(k_arg ...)))
+                     "\n" #:after-last "\n")
+                    (format "Expected: ~a arguments with kind(s): "
+                            (stx-length #'(k_in ...)))
+                    (string-join (stx-map type->str #'(k_in ...)) ", "))
+     (⊢ (#%app τ_fn- τ_arg- ...) : k_out)]))
+;
+;     #:fail-unless (stx-length=? #'(k_arg ...) #'(k ...))
+;                   (string-append
+;                    (format
+;                     "Wrong number of args given to tyλ ~a:\ngiven: "
+;                     (syntax->datum #'τ_fn))
+;                    (string-join
+;                     (map
+;                      (λ (t k) (format "~a : ~a" t k))
+;                      (syntax->datum #'(τ_arg ...))
+;                      (syntax->datum #`#,(stx-map get-orig #'(k_arg ...))))
+;                     ", ")
+;                    (format "\nexpected: ~a argument(s)." (stx-length #'(k ...))))
+;     #:fail-unless (typechecks? #'(k_arg ...) #'(k ...))
+;                   (string-append
+;                    (format
+;                     "Arguments to tyλ ~a have wrong type:\ngiven: "
+;                     (syntax->datum #'τ_fn))
+;                    (string-join
+;                     (map
+;                      (λ (t k) (format "~a : ~a" t k))
+;                      (syntax->datum #'(τ_arg ...))
+;                      (syntax->datum #`#,(stx-map get-orig #'(k_arg ...))))
+;                     ", ")
+;                    "\nexpected arguments with type: "
+;                    (string-join
+;                     (map ~a (syntax->datum #`#,(stx-map get-orig #'(k ...))))
+;                     ", "))
+;      ;; cant do type-subst here bc τ_fn might be a (forall) tyvar
+;      ;#:with τ_res ((current-type-eval) #'(tyapply τ_fn- τ_arg- ...))
+;     (⊢ (#%app τ_fn- τ_arg- ...) : k_res)]))
 
 ;; must override #%app and λ and primops to use new →
 ;; TODO: parameterize →?
@@ -150,52 +170,69 @@
     [(_ (b:typed-binding ...) e)
      #:when (andmap ★? (stx-map (λ (t) (typeof (expand/df t))) #'(b.τ ...)))
      #:with (xs- e- τ_res) (infer/type-ctxt+erase #'(b ...) #'e)
-     (⊢ #'(λ xs- e-) #'(→ b.τ ... τ_res))]))
+     (⊢ (λ xs- e-) : (→ b.τ ... τ_res))]))
 
 (define-syntax (app/tc stx)
   (syntax-parse stx
     [(_ e_fn e_arg ...)
-     #:with [e_fn- τ_fn] (infer+erase #'e_fn)
-     ;; this is sysf:→?, it's not defined in fomega so import without prefix
-     #:fail-unless (→? #'τ_fn)
-                   (format "Type error: Attempting to apply a non-function ~a with type ~a\n"
-                           (syntax->datum #'e_fn) (syntax->datum #'τ_fn))
-     #:with ((~literal #%plain-app) _ τ ... τ_res) #'τ_fn
+     #:with [e_fn- (~→* τ_in ... τ_out)] (infer+erase #'e_fn)
      #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
-     #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
+     #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
                    (string-append
-                    (format
-                     "Wrong number of args given to function ~a:\ngiven: "
-                     (syntax->datum #'e_fn))
+                    (format "~a (~a:~a) Arguments to function ~a have wrong type(s), "
+                            (syntax-source stx) (syntax-line stx) (syntax-column stx)
+                            (syntax->datum #'e_fn))
+                    "or wrong number of arguments:\nGiven:\n"
                     (string-join
-                     (map
-                      (λ (e t) (format "~a : ~a" e t))
-                      (syntax->datum #'(e_arg ...))
-                      (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
-                     ", ")
-                    (format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
-     #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
-                   (string-append
-                    (format
-                     "Arguments to function ~a have wrong type:\ngiven: "
-                     (syntax->datum #'e_fn))
-                    (string-join
-                     (map
-                      (λ (e t) (format "~a : ~a" e t))
-                      (syntax->datum #'(e_arg ...))
-                      (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
-                     ", ")
-                    "\nexpected arguments with type: "
-                    (string-join
-                     (map ~a (syntax->datum #`#,(stx-map get-orig #'(τ ...))))
-                     ", "))
-     (⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))
+                     (map (λ (e t) (format "  ~a : ~a" e t)) ; indent each line
+                          (syntax->datum #'(e_arg ...))
+                          (stx-map type->str #'(τ_arg ...)))
+                     "\n" #:after-last "\n")
+                    (format "Expected: ~a arguments with type(s): "
+                            (stx-length #'(τ_in ...)))
+                    (string-join (stx-map type->str #'(τ_in ...)) ", "))
+     (⊢ (#%app e_fn- e_arg- ...) : τ_out)]))
+;     #:with [e_fn- τ_fn] (infer+erase #'e_fn)
+;     ;; this is sysf:→?, it's not defined in fomega so import without prefix
+;     #:fail-unless (→? #'τ_fn)
+;                   (format "Type error: Attempting to apply a non-function ~a with type ~a\n"
+;                           (syntax->datum #'e_fn) (syntax->datum #'τ_fn))
+;     #:with ((~literal #%plain-app) _ τ ... τ_res) #'τ_fn
+;     #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
+;     #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
+;                   (string-append
+;                    (format
+;                     "Wrong number of args given to function ~a:\ngiven: "
+;                     (syntax->datum #'e_fn))
+;                    (string-join
+;                     (map
+;                      (λ (e t) (format "~a : ~a" e t))
+;                      (syntax->datum #'(e_arg ...))
+;                      (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
+;                     ", ")
+;                    (format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
+;     #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
+;                   (string-append
+;                    (format
+;                     "Arguments to function ~a have wrong type:\ngiven: "
+;                     (syntax->datum #'e_fn))
+;                    (string-join
+;                     (map
+;                      (λ (e t) (format "~a : ~a" e t))
+;                      (syntax->datum #'(e_arg ...))
+;                      (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
+;                     ", ")
+;                    "\nexpected arguments with type: "
+;                    (string-join
+;                     (map ~a (syntax->datum #`#,(stx-map get-orig #'(τ ...))))
+;                     ", "))
+;     (⊢ (#%app e_fn- e_arg- ...) : τ_res)]))
 
 ;; must override #%datum to use new kinded-Int, etc
 (define-syntax (datum/tc stx)
   (syntax-parse stx
-    [(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)]
-    [(_ . s:str) (⊢ (syntax/loc stx (#%datum . s)) #'String)]
+    [(_ . n:integer) (⊢ (#%datum . n) : Int)]
+    [(_ . s:str) (⊢ (#%datum . s) : String)]
     [(_ . x)
      #:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
      #'(#%datum . x)]))
\ No newline at end of file
diff --git a/tapl/notes.txt b/tapl/notes.txt
index d947f77..51b6d3a 100644
--- a/tapl/notes.txt
+++ b/tapl/notes.txt
@@ -1,3 +1,25 @@
+2015-08-13
+Requirements for define-type-constructor syntax:
+- identifier types, like Int
+- basic tuples, like arrow
+  - arity
+- nested tuples, like records
+- binding forms, like forall
+
+Problem: 
+Types must be expanded, to check that they are valid, catch unbound ids, etc.
+But should I attach the expanded type to a term, or the original surface stx?
+- maybe this is just repeating the same thing I wrote below?
+- Related question: fully expand types before calling type=? or typecheck?
+Answer: must only compare fully expanded forms, otherwise these will not work
+- define-type-alias
+Rules:
+- all user-written types must be expanded and checked
+  - check for invalid types, unbound ids
+- use expanded types (when available) to create new types
+- expand all types before attaching
+- assume types are expanded in type=? and typechecks
+
 2015-07-31
 Problem: pattern-expander not being recognized
 Solution: syntax-parse pattern directives must begin with ~ prefix
diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt
index c6672d1..1b46515 100644
--- a/tapl/stlc+box.rkt
+++ b/tapl/stlc+box.rkt
@@ -13,7 +13,8 @@
 ;; Terms:
 ;; - terms from stlc+cons.rkt
 
-(define-type-constructor (Ref τ) #:declare τ type)
+;(define-type-constructor (Ref τ) #:declare τ type)
+(define-basic-checked-stx Ref #:arity = 1)
 
 (define-syntax (ref stx)
   (syntax-parse stx
@@ -23,16 +24,14 @@
 (define-syntax (deref stx)
   (syntax-parse stx
     [(_ e)
+;     #:with (e- (~Ref* τ)) (infer+erase #'e) ; alternate pattern; worse err msg
      #:with (e- (τ)) (inferRef+erase #'e)
-;     #:with (e- ref-τ) (infer+erase #'e)
-;     #:with τ (Ref-get τ from ref-τ)
      (⊢ (unbox e-) : τ)]))
 (define-syntax (:= stx)
   (syntax-parse stx
     [(_ e_ref e)
      #:with (e_ref- (τ1)) (inferRef+erase #'e_ref)
-;     #:with (e_ref- ref-τ) (infer+erase #'e_ref)
-;     #:with τ1 (Ref-get τ from ref-τ)
+;     #:with (e_ref- (~Ref* τ1)) (infer+erase #'e_ref) ; alt pattern; worse err msg
      #:with (e- τ2) (infer+erase #'e)
      #:when (typecheck? #'τ1 #'τ2)
      (⊢ (set-box! e_ref- e-) : Unit)]))
\ No newline at end of file
diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt
index 9326136..98c713f 100644
--- a/tapl/stlc+cons.rkt
+++ b/tapl/stlc+cons.rkt
@@ -15,7 +15,8 @@
 
 ;; TODO: enable HO use of list primitives
 
-(define-type-constructor (List τ) #:declare τ type)
+;(define-type-constructor (List τ) #:declare τ type)
+(define-basic-checked-stx List #:arity = 1)
 
 (define-syntax (nil stx)
   (syntax-parse stx
@@ -28,7 +29,7 @@
   (syntax-parse stx
     [(_ e1 e2)
      #:with (e1- τ1) (infer+erase #'e1)
-     #:with (e2- (~List τ2)) (infer+erase #'e2)
+     #:with (e2- (τ2)) (inferList+erase #'e2)
 ;     #:with (e2- τ-lst) (infer+erase #'e2)
 ;     #:with τ2 (List-get τ from τ-lst)
      #:when (typecheck? #'τ1 #'τ2)
diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt
index f834342..4eab5bc 100644
--- a/tapl/stlc+lit.rkt
+++ b/tapl/stlc+lit.rkt
@@ -16,6 +16,8 @@
 
 (define-base-type Int)
 
+;(define-base-type Int)
+
 (define-primop + : (→ Int Int Int))
 
 (define-syntax (datum/tc stx)
diff --git a/tapl/stlc+rec-iso.rkt b/tapl/stlc+rec-iso.rkt
index 0b01ec4..5f262d1 100644
--- a/tapl/stlc+rec-iso.rkt
+++ b/tapl/stlc+rec-iso.rkt
@@ -17,17 +17,25 @@
 ;; - terms from stlc+reco+var.rkt
 ;; - fld/unfld
 
-(define-type-constructor
+#;(define-type-constructor
   (μ [[tv]] τ_body))
-; can't enforce this because bound ids wont have #%type tag
-  ;#:declare τ_body type)
-#;(define-syntax (μ stx)
-  (syntax-parse stx
+(define-syntax μ
+  (syntax-parser
     [(_ (tv:id) τ_body)
-     #'(#%type
-        (λ (tv)
-          (let-syntax ([tv (syntax-parser [tv:id #'(#%type tv)])])
-            τ_body)))]))
+     #:with ((tv-) τ_body- k) (infer/ctx+erase #'([tv : #%type]) #'τ_body)
+     #:when (#%type? #'k)
+     (mk-type #'(λ (tv-) τ_body-))]))
+(begin-for-syntax
+  (define-syntax ~μ*
+    (pattern-expander
+     (syntax-parser
+       [(_ (tv:id) τ)
+        #'(~or
+           ((~literal #%plain-lambda) (tv) τ)
+         (~and any (~do
+                    (type-error
+                     #:src #'any
+                     #:msg "Expected μ type, got: ~a" #'any))))]))))
 
 (begin-for-syntax
   ;; extend to handle μ
@@ -48,7 +56,7 @@
 (define-syntax (unfld stx)
   (syntax-parse stx
     [(_ τ:ann e)
-     #:with (~μ [[tv]] τ_body) #'τ.norm
+     #:with (~μ* (tv) τ_body) #'τ.norm
 ;     #:with ((~literal #%plain-lambda) (tv:id) τ_body) #'τ.norm
      #:with [e- τ_e] (infer+erase #'e)
      #:when (typecheck? #'τ_e #'τ.norm)
@@ -56,7 +64,7 @@
 (define-syntax (fld stx)
   (syntax-parse stx
     [(_ τ:ann e)
-     #:with (~μ [[tv]] τ_body) #'τ.norm
+     #:with (~μ* (tv) τ_body) #'τ.norm
 ;     #:with ((~literal #%plain-type) ((~literal #%plain-lambda) (tv:id) τ_body)) #'τ.norm
      #:with [e- τ_e] (infer+erase #'e)
      #:when (typecheck? #'τ_e (subst #'τ.norm #'tv #'τ_body))
diff --git a/tapl/stlc+reco+sub.rkt b/tapl/stlc+reco+sub.rkt
index 1215835..eea9ded 100644
--- a/tapl/stlc+reco+sub.rkt
+++ b/tapl/stlc+reco+sub.rkt
@@ -28,11 +28,12 @@
 (begin-for-syntax
   (define (sub? τ1 τ2)
     (or
-     (syntax-parse (list τ1 τ2) #:literals (× ∨ quote)
-       [(tup1 tup2)
-        #:when (and (×? #'tup1) (×? #'tup2))
-        #:with (['k:str τk] ...) (stx-map :-args (×-args #'tup1))
-        #:with (['l:str τl] ...) (stx-map :-args (×-args #'tup2))
+     (syntax-parse (list τ1 τ2) #:literals (quote)
+       [((~× [: 'k τk] ...) (~× [: 'l τl] ...))
+;       [(tup1 tup2)
+;        #:when (and (×? #'tup1) (×? #'tup2))
+;        #:with (['k:str τk] ...) (stx-map :-args (×-args #'tup1))
+;        #:with (['l:str τl] ...) (stx-map :-args (×-args #'tup2))
         #:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
                         (stx-map syntax-e (syntax->list #'(k ...))))
         (stx-andmap
@@ -41,10 +42,11 @@
             #:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...))
             ((current-sub?) #'τk_match #'τl)])
          #'([l τl] ...))]
-       [(var1 var2)
-        #:when (and (∨? #'var1) (∨? #'var2))
-        #:with (['k:str τk] ...) (stx-map :-args (∨-args #'var1))
-        #:with (['l:str τl] ...) (stx-map :-args (∨-args #'var2))
+       [((~∨ [<> 'k τk] ...) (~∨ [<> 'l τl] ...))
+;       [(var1 var2)
+;        #:when (and (∨? #'var1) (∨? #'var2))
+;        #:with (['k:str τk] ...) (stx-map :-args (∨-args #'var1))
+;        #:with (['l:str τl] ...) (stx-map :-args (∨-args #'var2))
         #:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
                         (stx-map syntax-e (syntax->list #'(k ...))))
         (stx-andmap
diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt
index 88cbdec..7715ae8 100644
--- a/tapl/stlc+reco+var.rkt
+++ b/tapl/stlc+reco+var.rkt
@@ -1,14 +1,15 @@
 #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=? × ~×))
+(require (only-in racket/bool symbol=?))
+(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin let #;type=? × infer×+erase))
+         (except-in "stlc+tup.rkt" #%app begin tup proj let #;type=? × infer×+erase))
 (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 (for-syntax type=?))
+                     stlc:#%app stlc:let stlc:begin stlc:×
+                     (for-syntax #;stlc:type=? stlc:infer×+erase)))
+(provide tup proj × var case ∨)
+(provide (for-syntax #;type=? same-types?))
 
 
 ;; Simply-Typed Lambda Calculus, plus records and variants
@@ -29,15 +30,15 @@
 (begin-for-syntax
   ; extend to:
   ; 1) accept strings (ie, record labels)
-  (define (type=? τ1 τ2)
+  #;(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-type=? type=?)
+  ;(current-typecheck-relation (current-type=?))
 
   (define (same-types? τs)
     (define τs-lst (syntax->list τs))
@@ -50,12 +51,23 @@
     [(_ 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 #'τ]))]))
+     #'(define-syntax alias (syntax-parser [x:id #'τ.norm]))]))
 
 ;(define-type-constructor [: str τ] #:lits (:))
 
 ; re-define tuples as records
-(define-type-constructor
+(define-syntax ×
+  (syntax-parser #:datum-literals (:)
+    [(_ [label:id : τ:type] ...)
+     #:with (valid-τ ...) (stx-map mk-type #'(('label τ.norm) ...))
+     #`(stlc:× valid-τ ...)]))
+(define-for-syntax (infer×+erase e)
+  (syntax-parse (stlc:infer×+erase e) #:context e
+    [(e- τ_e)
+     #:with (((~literal #%plain-app) (quote l) τ) ...) #'τ_e
+     #'(e- ((l τ) ...))]))
+
+#;(define-type-constructor
   ;(× [~× label τ_fld] ...) #:lits (~×)
   (× [: label τ_fld] ...) #:lits (:)
   #:declare label str
@@ -67,46 +79,109 @@
 ;; records
 (define-syntax (tup stx)
   (syntax-parse stx #:datum-literals (=)
-    [(_ [l:str = e] ...)
+    [(_ [l:id = e] ...)
      #:with ([e- τ] ...) (infers+erase #'(e ...))
      ;(⊢ (list (list l e-) ...) : (× [~× l τ] ...))]
-     (⊢ (list (list l e-) ...) : (× [: l τ] ...))]
+     (⊢ (list (list 'l e-) ...) : (× [l : τ] ...))]
     #;[(_ e ...)
      #'(stlc:tup e ...)]))
 (define-syntax (proj stx)
   (syntax-parse stx #:literals (quote)
-    [(_ e_rec l:str)
-     #:with (e_rec- (~× [: 'l_τ τ] ...)) (infer+erase #'e_rec)
+    [(_ e_rec l:id)
+;     #:with (e_rec- (~×* [: 'l_τ τ] ...)) (infer+erase #'e_rec)
+     #:with (e_rec- ([l_τ τ] ...)) (infer×+erase #'e_rec)
 ;     #:with [rec- τ_rec] (infer+erase #'e_rec) ; match method #2: get
 ;     #:with ('l_τ:str ...) (×-get label from τ_rec)
 ;     #:with (τ ...) (×-get τ_fld from τ_rec)
-     #:with (l_match:str τ_match) (str-stx-assoc #'l #'([l_τ τ] ...))
-     (⊢ (cadr (assoc l e_rec-)) : τ_match)]
+     #:with (_ τ_match) (stx-assoc #'l #'([l_τ τ] ...))
+     (⊢ (cadr (assoc 'l e_rec-)) : τ_match)]
     #;[(_ e ...) #'(stlc:proj e ...)]))
 
+(define-basic-checked-stx ∨/internal)
 
-(define-type-constructor
+; re-define tuples as records
+(define-syntax ∨
+  (syntax-parser #:datum-literals (:)
+    [(_ (~and [label:id : τ:type] x) ...)
+     #:when (> (stx-length #'(x ...)) 0)
+     #:with (valid-τ ...) (stx-map mk-type #'(('label τ.norm) ...))
+     #'(∨/internal valid-τ ...)]
+    [any
+     (type-error #:src #'any
+                 #:msg (string-append
+                        "Improper usage of type constructor ∨: ~a, expected (∨ [label:id : τ:type] ...+)")
+                 #'any)]))
+(begin-for-syntax
+  (define (infer∨+erase e)
+    (syntax-parse (infer+erase e) #:context e
+      [(e- τ_e)
+       #:fail-unless (∨/internal? #'τ_e)
+       (format
+        "~a (~a:~a): Expected expression ~a to have ∨ type, got: ~a"
+        (syntax-source e) (syntax-line e) (syntax-column e)
+        (syntax->datum e) (type->str #'τ_e))
+       #:with (~∨/internal ((~literal #%plain-app) (quote l) τ) ...) #'τ_e
+       #'(e- ((l τ) ...))]))
+  (define-syntax ~∨*
+    (pattern-expander
+     (syntax-parser #:datum-literals (:)
+      [(_ [l : τ_l] (~and ddd (~literal ...)))
+       #'(~or (~∨/internal ((~literal #%plain-app) (quote l) τ_l) ddd)
+              (~and any (~do (type-error
+                              #:src #'any
+                              #:msg "Expected ∨ type, got: ~a" #'any))))]))))
+
+#;(define-type-constructor
   (∨ [<> label τ_var] ...) #:lits (<>)
   #:declare label str
   #:declare τ_var type)
 
 (define-syntax (var stx)
+  (syntax-parse stx #:datum-literals (as =)
+    [(_ l:id = e as τ:type)
+;     #:when (∨? #'τ.norm)
+;     #:with (['l_τ:str τ_l] ...) (stx-map :-args (∨-args #'τ.norm))
+     #:with (~∨* [l_τ : τ_l] ...) #'τ.norm
+;     #:with ('l_τ:str ...) (∨-get label from τ)
+;     #:with (τ_l ...) (∨-get τ_var from τ)
+     #:with (_ τ_match) (stx-assoc #'l #'((l_τ τ_l) ...))
+     #:with (e- τ_e) (infer+erase #'e)
+     #:when (typecheck? #'τ_e #'τ_match)
+     (⊢ (list 'l e) : τ)]))
+(define-syntax (case stx)
+  (syntax-parse stx #:datum-literals (of =>)
+    [(_ e [l:id x:id => e_l] ...)
+     #:fail-when (null? (syntax->list #'(l ...))) "no clauses"
+;     #:with (e- (~∨* [<> 'l_x τ_x] ...)) (infer+erase #'e)
+     #:with (e- ([l_x τ_x] ...)) (infer∨+erase #'e)
+;     #:with ('l_x:str ...) (∨-get label from τ_e)
+;     #:with (τ_x ...) (∨-get τ_var from τ_e)
+     #:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
+     #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"
+     #:with (((x-) e_l- τ_el) ...)
+            (stx-map (λ (bs e) (infer/type-ctxt+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...))
+     #:fail-unless (same-types? #'(τ_el ...)) "branches have different types"
+     (⊢ (let ([l_e (car e-)])
+          (cond [(symbol=? l_e 'l) (let ([x- (cadr e-)]) e_l-)] ...))
+        : #,(stx-car #'(τ_el ...)))]))
+
+#;(define-syntax (var stx)
   (syntax-parse stx #:datum-literals (as =) #:literals (quote)
     [(_ l:str = e as τ:type)
 ;     #:when (∨? #'τ.norm)
 ;     #:with (['l_τ:str τ_l] ...) (stx-map :-args (∨-args #'τ.norm))
-     #:with (~∨ [<> 'l_τ τ_l] ...) #'τ.norm
+     #:with (~∨* [<> 'l_τ τ_l] ...) #'τ.norm
 ;     #:with ('l_τ:str ...) (∨-get label from τ)
 ;     #:with (τ_l ...) (∨-get τ_var from τ)
      #:with (l_match:str τ_match) (str-stx-assoc #'l #'((l_τ τ_l) ...))
      #:with (e- τ_e) (infer+erase #'e)
      #:when (typecheck? #'τ_e #'τ_match)
      (⊢ (list l e) : τ)]))
-(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"
-     #:with (e- (~∨ [<> 'l_x τ_x] ...)) (infer+erase #'e)
+     #:with (e- (~∨* [<> 'l_x τ_x] ...)) (infer+erase #'e)
 ;     #:with ('l_x:str ...) (∨-get label from τ_e)
 ;     #:with (τ_x ...) (∨-get τ_var from τ_e)
      #:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
index c3ad21c..b6240de 100644
--- a/tapl/stlc+sub.rkt
+++ b/tapl/stlc+sub.rkt
@@ -31,26 +31,26 @@
 
 (define-syntax (datum/tc stx)
   (syntax-parse stx
-    [(_ . n:nat) (⊢ (syntax/loc stx (#%datum . n)) #'Nat)]
-    [(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)]
-    [(_ . n:number) (⊢ (syntax/loc stx (#%datum . n)) #'Num)]
+    [(_ . n:nat) (⊢ (#%datum . n) : Nat)]
+    [(_ . n:integer) (⊢ (#%datum . n) : Int)]
+    [(_ . n:number) (⊢ (#%datum . n) : Num)]
     [(_ . x) #'(stlc:#%datum . x)]))
 
 (begin-for-syntax
   (define (sub? τ1 τ2)
+    ; only need this because recursive calls made with unexpanded types
+    (define τ1 ((current-type-eval) t1))
+    (define τ2 ((current-type-eval) t2))
 ;    (printf "t1 = ~a\n" (syntax->datum τ1))
 ;    (printf "t2 = ~a\n" (syntax->datum τ2))
     (or ((current-type=?) τ1 τ2)
-        (syntax-parse (list τ1 τ2) #:literals (Nat Int Num Top)
-          [(_ Top) #t]
-          [(Nat τ) ((current-sub?) #'Int #'τ)]
-          [(Int τ) ((current-sub?) #'Num #'τ)]
-          [(τ Num) ((current-sub?) #'τ #'Int)]
-          [(τ Int) ((current-sub?) #'τ #'Nat)]
-          [(arr1 arr2)
-           #:when (and (→? #'arr1) (→? #'arr2))
-           #:with (s1 ... s2) (→-args #'arr1)
-           #:with (t1 ... t2) (→-args #'arr2)
+        (syntax-parse (list τ1 τ2)
+          [(_ ~Top) #t]
+          [(~Nat τ) ((current-sub?) #'Int #'τ)]
+          [(~Int τ) ((current-sub?) #'Num #'τ)]
+          [(τ ~Num) ((current-sub?) #'τ #'Int)]
+          [(τ ~Int) ((current-sub?) #'τ #'Nat)]
+          [((~→ s1 ... s2) (~→ t1 ... t2))
            (and (subs? #'(t1 ...) #'(s1 ...))
                 ((current-sub?) #'s2 #'t2))]
           [_ #f])))
diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt
index a143203..9601110 100644
--- a/tapl/stlc+tup.rkt
+++ b/tapl/stlc+tup.rkt
@@ -14,7 +14,8 @@
 ;; - terms from ext-stlc.rkt
 ;; - tup and proj
 
-(define-type-constructor (× τ ...) #:declare τ type)
+(define-basic-checked-stx ×)
+;(define-type-constructor (× τ ...) #:declare τ type)
 
 (define-syntax (tup stx)
   (syntax-parse stx
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
index c18860a..52eda68 100644
--- a/tapl/stlc.rkt
+++ b/tapl/stlc.rkt
@@ -21,9 +21,8 @@
   ;;   - may require some caution when mixing expanded and unexpanded types to
   ;;     create other types
   (define (type-eval τ)
-    (if (plain-type? τ) ; don't expand if already expanded
-        τ 
-        (add-orig #`(#%plain-type #,(expand/df τ)) τ)))
+    (or (plain-type? τ) ; don't expand if already expanded
+        (add-orig (expand/df τ) τ)))
   
   (current-type-eval type-eval)
 
@@ -48,7 +47,9 @@
   (define current-type=? (make-parameter type=?))
   (current-typecheck-relation type=?))
 
-(define-type-constructor (→ τ_in ... τ_out)
+(define-basic-checked-stx → #:arity >= 1)
+
+#;(define-type-constructor (→ τ_in ... τ_out)
   #:declare τ_in type
   #:declare τ_out type)
 
@@ -62,11 +63,11 @@
   (syntax-parse stx
     [(_ e_fn e_arg ...)
      ;; 2015-08-06: there are currently three alternative tycon matching syntaxes
-     #:with [e_fn- (~→ τ_in ... τ_out)] (infer+erase #'e_fn) ; #1 (external) pattern expander
+;     #:with [e_fn- (~→* τ_in ... τ_out)] (infer→+erase #'e_fn) ; #1 (external) pattern expander
      ;#:with [e_fn- τ_fn] (infer+erase #'e_fn) ; #2 get, via (internal) pattern expander
      ;#:with (τ_in ...) (→-get τ_in from #'τ_fn)
      ;#:with τ_out (→-get τ_out from #'τ_fn)
-     ;#:with [e_fn- (τ_in ... τ_out)] (infer→+erase #'e_fn) ; #3 work directly on term
+     #:with [e_fn- (τ_in ... τ_out)] (infer→+erase #'e_fn) ; #3 work directly on term -- better err msg
      #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
      #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
                    (string-append
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
index b0fd6f7..7b35095 100644
--- a/tapl/stx-utils.rkt
+++ b/tapl/stx-utils.rkt
@@ -2,7 +2,7 @@
 (require syntax/stx racket/list)
 (provide (all-defined-out))
 
-(define (stx-cadr stx) (car (stx-cdr stx)))
+(define (stx-cadr stx) (stx-car (stx-cdr stx)))
 
 (define (stx-andmap f . stx-lsts)
   (apply andmap f (map syntax->list stx-lsts)))
@@ -23,6 +23,8 @@
   (member (datum->syntax v) (map datum->syntax (syntax->list stx)) string=?))
 (define (str-stx-assoc v stx)
   (assoc v (map syntax->list (syntax->list stx)) stx-str=?))
+(define (stx-assoc v stx) ; v = id
+  (assoc v (map syntax->list (syntax->list stx)) free-identifier=?))
 
 (define (stx-length stx) (length (syntax->list stx)))
 (define (stx-length=? stx1 stx2)
diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt
index 2e0c347..35c34b3 100644
--- a/tapl/sysf.rkt
+++ b/tapl/sysf.rkt
@@ -20,12 +20,13 @@
 ;; - Λ and inst
 
 ;; dont use define-type-constructor, instead define explicit macro
-(provide ∀)
-(define-syntax (∀ stx)
+;(provide ∀)
+#;(define-syntax (∀ stx)
   (syntax-parse stx
     [(_ (x:id ...) body) ; cannot use :type annotation on body bc of unbound vars
      ;; use #%plain-lambda to avoid insertion of #%expression
      (syntax/loc stx (#%plain-lambda (x ...) body))]))
+(define-type-constructor (∀ [[x ...]] body))
 
 (begin-for-syntax
   ;; extend to handle ∀
@@ -44,11 +45,12 @@
 (define-syntax (Λ stx)
   (syntax-parse stx
     [(_ (tv:id ...) e)
-     #:with (tvs- e- τ) (infer/tvs+erase #'e #'(tv ...))
-     (⊢ #'e- #'(∀ tvs- τ))]))
+     #:with ((tv- ...) e- τ) (infer/tvs+erase #'e #'(tv ...))
+     (⊢ e- : (∀ #:bind (tv- ...) τ))]))
 (define-syntax (inst stx)
   (syntax-parse stx
     [(_ e τ:type ...)
-     #:with (e- ∀τ) (infer+erase #'e)
-     #:with ((~literal #%plain-lambda) (tv ...) τ_body) #'∀τ
-     (⊢ #'e- (substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
\ No newline at end of file
+     #:with (e- (~∀* [[tv ...]] τ_body)) (infer+erase #'e)
+;     #:with (e- ∀τ) (infer+erase #'e)
+;     #:with ((~literal #%plain-lambda) (tv ...) τ_body) #'∀τ
+     (⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
\ No newline at end of file
diff --git a/tapl/tests/exist-tests.rkt b/tapl/tests/exist-tests.rkt
index ce5e142..4ddbf0d 100644
--- a/tapl/tests/exist-tests.rkt
+++ b/tapl/tests/exist-tests.rkt
@@ -1,99 +1,99 @@
 #lang s-exp "../exist.rkt"
 (require "rackunit-typechecking.rkt")
 
-(check-type (pack (Int 0) as (∃ [[X]] X)) : (∃ [[X]] X))
-(check-type (pack (Int 0) as (∃ [[X]] X)) : (∃ [[Y]] Y))
-(typecheck-fail (pack (Int 0) as (∃ [[X]] Y)))
-(check-type (pack (Bool #t) as (∃ [[X]] X)) : (∃ [[X]] X))
-(typecheck-fail (pack (Int #t) as (∃ [[X]] X)))
+(check-type (pack (Int 0) as (∃ (X) X)) : (∃ (X) X))
+(check-type (pack (Int 0) as (∃ (X) X)) : (∃ (Y) Y))
+(typecheck-fail (pack (Int 0) as (∃ (X) Y)))
+(check-type (pack (Bool #t) as (∃ (X) X)) : (∃ (X) X))
+(typecheck-fail (pack (Int #t) as (∃ (X) X)))
 
 ; cant typecheck bc X has local scope, and no X elimination form
-;(check-type (open ([(X x) <= (pack (Int 0) as (∃ [[X]] X))]) x) : X) 
+;(check-type (open ([(X x) <= (pack (Int 0) as (∃ (X) X))]) x) : X) 
 
 (check-type 0 : Int)
 (check-type (+ 0 1) : Int ⇒ 1)
 (check-type ((λ ([x : Int]) (+ x 1)) 0) : Int ⇒ 1)
-(typecheck-fail (open ([(X x) <= (pack (Int 0) as (∃ [[X]] X))]) (+ x 1))) ; can't use as Int
+(typecheck-fail (open ([(X x) <= (pack (Int 0) as (∃ (X) X))]) (+ x 1))) ; can't use as Int
 
-(check-type (λ ([x : (∃ [[X]] X)]) x) : (→ (∃ [[X]] X) (∃ [[Y]] Y)))
-(check-type ((λ ([x : (∃ [[X]] X)]) x) (pack (Int 0) as (∃ [[Z]] Z)))
-            : (∃ [[X]] X) ⇒ 0)
-(check-type ((λ ([x : (∃ [[X]] X)]) x) (pack (Bool #t) as (∃ [[Z]] Z)))
-            : (∃ [[X]] X) ⇒ #t)
+(check-type (λ ([x : (∃ (X) X)]) x) : (→ (∃ (X) X) (∃ (Y) Y)))
+(check-type ((λ ([x : (∃ (X) X)]) x) (pack (Int 0) as (∃ (Z) Z)))
+            : (∃ (X) X) ⇒ 0)
+(check-type ((λ ([x : (∃ (X) X)]) x) (pack (Bool #t) as (∃ (Z) Z)))
+            : (∃ (X) X) ⇒ #t)
 
 ;; example where the two binding X's are conflated, see exist.rkt for explanation
-(check-type (open ([(X x) <= (pack (Int 0) as (∃ [[X]] X))]) ((λ ([y : X]) 1) x))
+(check-type (open ([(X x) <= (pack (Int 0) as (∃ (X) X))]) ((λ ([y : X]) 1) x))
             : Int ⇒ 1)
             
 (check-type
- (pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
-       as (∃ [[X]] (× [: "a" X] [: "f" (→ X X)])))
- : (∃ [[X]] (× [: "a" X] [: "f" (→ X X)])))
+ (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
+       as (∃ (X) (× [a : X] [f : (→ X X)])))
+ : (∃ (X) (× [a : X] [f : (→ X X)])))
 
 (define p4
-  (pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
-        as (∃ [[X]] (× [: "a" X] [: "f" (→ X Int)]))))
-(check-type p4 : (∃ [[X]] (× [: "a" X] [: "f" (→ X Int)])))
+  (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
+        as (∃ (X) (× [a : X] [f : (→ X Int)]))))
+(check-type p4 : (∃ (X) (× [a : X] [f : (→ X Int)])))
 
-(check-not-type (open ([(X x) <= p4]) (proj x "a")) : Int) ; type is X, not Int
+(check-not-type (open ([(X x) <= p4]) (proj x a)) : Int) ; type is X, not Int
 ; type is (→ X X), not (→ Int Int)
-(check-not-type (open ([(X x) <= p4]) (proj x "f")) : (→ Int Int))
-(typecheck-fail (open ([(X x) <= p4]) (+ 1 (proj x "a"))))
-(check-type (open ([(X x) <= p4]) ((proj x "f") (proj x "a"))) : Int ⇒ 6)
-(check-type (open ([(X x) <= p4]) ((λ ([y : X]) ((proj x "f") y)) (proj x "a"))) : Int ⇒ 6)
+(check-not-type (open ([(X x) <= p4]) (proj x f)) : (→ Int Int))
+(typecheck-fail (open ([(X x) <= p4]) (+ 1 (proj x a))))
+(check-type (open ([(X x) <= p4]) ((proj x f) (proj x a))) : Int ⇒ 6)
+(check-type (open ([(X x) <= p4]) ((λ ([y : X]) ((proj x f) y)) (proj x a))) : Int ⇒ 6)
 
 (check-type
- (open ([(X x) <= (pack (Int 0) as (∃ [[Y]] Y))])
+ (open ([(X x) <= (pack (Int 0) as (∃ (Y) Y))])
        ((λ ([y : X]) 1) x))
  : Int ⇒ 1)
 
 (check-type
- (pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
-       as (∃ [[X]] (× [: "a" Int] [: "f" (→ Int Int)])))
- : (∃ [[X]] (× [: "a" Int] [: "f" (→ Int Int)])))
+ (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
+       as (∃ (X) (× [a : Int] [f : (→ Int Int)])))
+ : (∃ (X) (× [a : Int] [f : (→ Int Int)])))
 
 (typecheck-fail
- (pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
-       as (∃ [[X]] (× [: "a" Int] [: "f" (→ Bool Int)]))))
+ (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
+       as (∃ (X) (× [a : Int] [f : (→ Bool Int)]))))
 
 (typecheck-fail
- (pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
-       as (∃ [[X]] (× [: "a" X] [: "f" (→ X Bool)]))))
+ (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
+       as (∃ (X) (× [a : X] [f : (→ X Bool)]))))
 
 (check-type
- (pack (Bool (tup ["a" = #t] ["f" = (λ ([x : Bool]) (if x 1 2))]))
-       as (∃ [[X]] (× [: "a" X] [: "f" (→ X Int)])))
- : (∃ [[X]] (× [: "a" X] [: "f" (→ X Int)])))
+ (pack (Bool (tup [a = #t] [f = (λ ([x : Bool]) (if x 1 2))]))
+       as (∃ (X) (× [a : X] [f : (→ X Int)])))
+ : (∃ (X) (× [a : X] [f : (→ X Int)])))
 
 (define counterADT
-  (pack (Int (tup ["new" = 1]
-                  ["get" = (λ ([i : Int]) i)]
-                  ["inc" = (λ ([i : Int]) (+ i 1))]))
-        as (∃ [[Counter]] (× [: "new" Counter]
-                           [: "get" (→ Counter Int)]
-                           [: "inc" (→ Counter Counter)]))))
+  (pack (Int (tup [new = 1]
+                  [get = (λ ([i : Int]) i)]
+                  [inc = (λ ([i : Int]) (+ i 1))]))
+        as (∃ (Counter) (× [new : Counter]
+                           [get : (→ Counter Int)]
+                           [inc : (→ Counter Counter)]))))
 (check-type counterADT :
-            (∃ [[Counter]] (× [: "new" Counter]
-                            [: "get" (→ Counter Int)]
-                            [: "inc" (→ Counter Counter)])))
+            (∃ (Counter) (× [new : Counter]
+                            [get : (→ Counter Int)]
+                            [inc : (→ Counter Counter)])))
 (check-type
  (open ([(Counter counter) <= counterADT])
-       ((proj counter "get") ((proj counter "inc") (proj counter "new"))))
+       ((proj counter get) ((proj counter inc) (proj counter new))))
  : Int ⇒ 2)
 
  (check-type
   (open ([(Counter counter) <= counterADT])
-        (let ([inc (proj counter "inc")]
-              [get (proj counter "get")])
+        (let ([inc (proj counter inc)]
+              [get (proj counter get)])
           (let ([add3 (λ ([c : Counter]) (inc (inc (inc c))))])
-            (get (add3 (proj counter "new"))))))
+            (get (add3 (proj counter new))))))
   : Int ⇒ 4)
 
 (check-type
  (open ([(Counter counter) <= counterADT])
-       (let ([get (proj counter "get")]
-             [inc (proj counter "inc")]
-             [new (λ () (proj counter "new"))])
+       (let ([get (proj counter get)]
+             [inc (proj counter inc)]
+             [new (λ () (proj counter new))])
          (letrec ([(is-even? : (→ Int Bool))
                    (λ ([n : Int])
                      (or (zero? n)
@@ -103,38 +103,38 @@
                      (and (not (zero? n))
                           (is-even? (sub1 n))))])
            (open ([(FlipFlop flipflop) <=
-                   (pack (Counter (tup ["new" = (new)]
-                                       ["read" = (λ ([c : Counter]) (is-even? (get c)))]
-                                       ["toggle" = (λ ([c : Counter]) (inc c))]
-                                       ["reset" = (λ ([c : Counter]) (new))]))
-                         as (∃ [[FlipFlop]] (× [: "new" FlipFlop]
-                                             [: "read" (→ FlipFlop Bool)]
-                                             [: "toggle" (→ FlipFlop FlipFlop)]
-                                             [: "reset" (→ FlipFlop FlipFlop)])))])
-                 (let ([read (proj flipflop "read")]
-                       [togg (proj flipflop "toggle")])
-                   (read (togg (togg (togg (togg (proj flipflop "new")))))))))))
+                   (pack (Counter (tup [new = (new)]
+                                       [read = (λ ([c : Counter]) (is-even? (get c)))]
+                                       [toggle = (λ ([c : Counter]) (inc c))]
+                                       [reset = (λ ([c : Counter]) (new))]))
+                         as (∃ (FlipFlop) (× [new : FlipFlop]
+                                             [read : (→ FlipFlop Bool)]
+                                             [toggle : (→ FlipFlop FlipFlop)]
+                                             [reset : (→ FlipFlop FlipFlop)])))])
+                 (let ([read (proj flipflop read)]
+                       [togg (proj flipflop toggle)])
+                   (read (togg (togg (togg (togg (proj flipflop new)))))))))))
  : Bool ⇒ #f)
 
 (define counterADT2
-  (pack ((× [: "x" Int])
-         (tup ["new" = (tup ["x" = 1])]
-              ["get" = (λ ([i : (× [: "x" Int])]) (proj i "x"))]
-              ["inc" = (λ ([i : (× [: "x" Int])]) (tup ["x" = (+ 1 (proj i "x"))]))]))
-        as (∃ [[Counter]] (× [: "new" Counter]
-                           [: "get" (→ Counter Int)]
-                           [: "inc" (→ Counter Counter)]))))
+  (pack ((× [x : Int])
+         (tup [new = (tup [x = 1])]
+              [get = (λ ([i : (× [x : Int])]) (proj i x))]
+              [inc = (λ ([i : (× [x : Int])]) (tup [x = (+ 1 (proj i x))]))]))
+        as (∃ (Counter) (× [new : Counter]
+                           [get : (→ Counter Int)]
+                           [inc : (→ Counter Counter)]))))
 (check-type counterADT2 :
-            (∃ [[Counter]] (× [: "new" Counter]
-                            [: "get" (→ Counter Int)]
-                            [: "inc" (→ Counter Counter)])))
+            (∃ (Counter) (× [new : Counter]
+                            [get : (→ Counter Int)]
+                            [inc : (→ Counter Counter)])))
 
 ;; same as above, but with different internal counter representation
 (check-type
  (open ([(Counter counter) <= counterADT2])
-       (let ([get (proj counter "get")]
-             [inc (proj counter "inc")]
-             [new (λ () (proj counter "new"))])
+       (let ([get (proj counter get)]
+             [inc (proj counter inc)]
+             [new (λ () (proj counter new))])
          (letrec ([(is-even? : (→ Int Bool))
                    (λ ([n : Int])
                      (or (zero? n)
@@ -144,19 +144,29 @@
                      (and (not (zero? n))
                           (is-even? (sub1 n))))])
            (open ([(FlipFlop flipflop) <=
-                   (pack (Counter (tup ["new" = (new)]
-                                       ["read" = (λ ([c : Counter]) (is-even? (get c)))]
-                                       ["toggle" = (λ ([c : Counter]) (inc c))]
-                                       ["reset" = (λ ([c : Counter]) (new))]))
-                         as (∃ [[FlipFlop]] (× [: "new" FlipFlop]
-                                             [: "read" (→ FlipFlop Bool)]
-                                             [: "toggle" (→ FlipFlop FlipFlop)]
-                                             [: "reset" (→ FlipFlop FlipFlop)])))])
-                 (let ([read (proj flipflop "read")]
-                       [togg (proj flipflop "toggle")])
-                   (read (togg (togg (togg (togg (proj flipflop "new")))))))))))
+                   (pack (Counter (tup [new = (new)]
+                                       [read = (λ ([c : Counter]) (is-even? (get c)))]
+                                       [toggle = (λ ([c : Counter]) (inc c))]
+                                       [reset = (λ ([c : Counter]) (new))]))
+                         as (∃ (FlipFlop) (× [new : FlipFlop]
+                                             [read : (→ FlipFlop Bool)]
+                                             [toggle : (→ FlipFlop FlipFlop)]
+                                             [reset : (→ FlipFlop FlipFlop)])))])
+                 (let ([read (proj flipflop read)]
+                       [togg (proj flipflop toggle)])
+                   (read (togg (togg (togg (togg (proj flipflop new)))))))))))
  : Bool ⇒ #f)
 
+;; err cases
+(typecheck-fail
+ (pack (Int 1) as Int)
+ #:with-msg
+ "Expected type of expression to match pattern \\(∃ \\(\\(X)) τ_body), got: Int")
+(typecheck-fail
+ (open ([(X x) <= 2]) 3)
+ #:with-msg
+ "Expected type of expression to match pattern \\(∃ \\(\\(X)) τ_body), got: Int")
+
 ;; previous tets from stlc+reco+var-tests.rkt ---------------------------------
 ;; define-type-alias
 (define-type-alias Integer Int)
@@ -171,68 +181,68 @@
 
 ;; records (ie labeled tuples)
 (check-type "Stephen" : String)
-(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-            (× [: "name" String] [: "phone" Int] [: "male?" Bool]))
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(check-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+            (× [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")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
             : String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone)
             : Int ⇒ 781)
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
+(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]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-                (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-                (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [my-name : String] [phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [name : String] [my-phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [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
+ (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
+ (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
+ (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
+ (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]))
+ (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])
+        (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])
+ (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: ------------------------------------------------------------
diff --git a/tapl/tests/ext-stlc-tests.rkt b/tapl/tests/ext-stlc-tests.rkt
index 995d713..7acfc3a 100644
--- a/tapl/tests/ext-stlc-tests.rkt
+++ b/tapl/tests/ext-stlc-tests.rkt
@@ -29,7 +29,7 @@
 (typecheck-fail (begin) #:with-msg "expected more terms")
 (typecheck-fail
  (begin 1 2 3)
- #:with-msg "all begin expressions except the last one should have type Unit")
+ #:with-msg "Expected expression 1 to have type Unit, got: Int")
 
 (check-type (begin (void) 1) : Int ⇒ 1)
 (check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int)
@@ -42,6 +42,11 @@
 (check-type (ann 1 : Int) : Int ⇒ 1)
 (check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
 (typecheck-fail (ann 1 : Bool) #:with-msg "ann: 1 does not have type Bool")
+;ann errs
+(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
+(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
+(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
+(typecheck-fail (ann Int : Int) #:with-msg "does not have type Int")
 
 ; let
 (check-type (let () (+ 1 1)) : Int ⇒ 2)
@@ -60,7 +65,6 @@
   #:with-msg
  "Arguments to function \\+.+have wrong type.+Given:.+Bool.+Int.+Expected:.+Int.+Int")
 
-
 ; letrec
 (typecheck-fail
  (letrec ([(x : Int) #f] [(y : Int) 1]) y)
@@ -95,12 +99,29 @@
    (is-odd? 11)) : Bool ⇒ #t)
 
 ;; check some more err msgs
-(typecheck-fail (and "1" #f) #:with-msg "Expected type of.+to be Bool")
-(typecheck-fail (and #t "2") #:with-msg "Expected type of.+to be Bool")
-(typecheck-fail (or "1" #f) #:with-msg "Expected type of.+to be Bool")
-(typecheck-fail (or #t "2") #:with-msg "Expected type of.+to be Bool")
-(typecheck-fail (if "true" 1 2) #:with-msg "Expected type of.+to be Bool")
-
+(typecheck-fail
+ (and "1" #f)
+ #:with-msg "Expected expression \"1\" to have type Bool, got: String")
+(typecheck-fail
+ (and #t "2")
+ #:with-msg
+ "Expected expression \"2\" to have type Bool, got: String")
+(typecheck-fail
+ (or "1" #f)
+ #:with-msg
+ "Expected expression \"1\" to have type Bool, got: String")
+(typecheck-fail
+ (or #t "2")
+ #:with-msg
+ "Expected expression \"2\" to have type Bool, got: String")
+(typecheck-fail
+ (if "true" 1 2)
+ #:with-msg
+ "Expected expression \"true\" to have type Bool, got: String")
+(typecheck-fail
+ (if #t 1 "2")
+ #:with-msg 
+ "branches must have the same type: given Int and String")
 
 ;; tests from stlc+lit-tests.rkt --------------------------
 ; most should pass, some failing may now pass due to added types/forms
@@ -122,7 +143,7 @@
 (typecheck-fail
  (λ ([f : Int]) (f 1 2))
  #:with-msg
- "Expected type of expression to match pattern \\(→ τ_in ... τ_out\\), got: Int")
+ "Expected expression f to have → type, 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/fomega-tests.rkt b/tapl/tests/fomega-tests.rkt
index 8be99f4..b610da3 100644
--- a/tapl/tests/fomega-tests.rkt
+++ b/tapl/tests/fomega-tests.rkt
@@ -1,188 +1,191 @@
 #lang s-exp "../fomega.rkt"
 (require "rackunit-typechecking.rkt")
 
-(check-type Int : ★)
-(check-type String : ★)
-(typecheck-fail →)
-(check-type (→ Int Int) : ★)
-(typecheck-fail (→ →))
-(check-type 1 : Int)
+;(check-type Int : ★)
+;(check-type String : ★)
+;(typecheck-fail →)
+;(check-type (→ Int Int) : ★)
+;(typecheck-fail (→ →))
+;(typecheck-fail (→ 1))
+;(check-type 1 : Int)
+;
+;(check-type (∀ ([t : ★]) (→ t t)) : ★)
+;(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
 
-(check-type (∀ ([t : ★]) (→ t t)) : ★)
-(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
+(Λ ([X : ★]) (λ ([x : X]) x))
 
-(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
-            : (∀ ([X : ★]) (→ X X )))
-(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (⇒ ★ ★)]) (λ ([x : X]) x))))
+#;(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
+            : (∀ ([X : ★]) (→ X X)))
+;(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (⇒ ★ ★)]) (λ ([x : X]) x))))
 
-(check-type (tyλ ([t : ★]) t) : (⇒ ★ ★))
-(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★))
-(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★)))
-(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★)))
-(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
-(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★))
-
-(check-type (tyapp (tyλ ([t : ★]) t) Int) : ★)
-(check-type (λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) : (→ Int Int))
-(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
-(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
-(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
-(typecheck-fail ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
-
-;; partial-apply →
-(check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)
-            : (⇒ ★ ★))
-; f's type must have kind ★
-(typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f))
-(check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) :
-            (∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String))))
-(check-type (inst
-             (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
-             (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
-            : (→ (→ Int String) (→ Int String)))
-;; applied f too early
-(typecheck-fail (inst
-                 (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
-                 (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)))
-(check-type ((inst
-              (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
-              (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
-             (λ ([x : Int]) "int")) : (→ Int String))
-(check-type (((inst
-               (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
-              (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
-              (λ ([x : Int]) "int")) 1) : String ⇒ "int")
-
-; tapl examples, p441
-(define-type-alias Id (tyλ ([X : ★]) X))
-(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
-(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int))
-(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int))
-(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int (tyapp Id String)) Int))
-(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) (tyapp Id String)) Int))
-(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) String) Int))
-(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (→ Int String) Int))
-(check-type (λ ([f : (→ Int String)]) 1) : (→ (tyapp Id (→ Int String)) Int))
-(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (→ Int String)) Int))
-(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int))
-
-; tapl examples, p451
-(define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
-
-(check-type Pair : (⇒ ★ ★ ★))
-
-(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
-;; parametric pair constructor
-(check-type
- (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
- : (∀ ([X : ★][Y : ★]) (→ X Y (tyapp Pair X Y))))
-; concrete Pair Int String constructor
-(check-type
- (inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
-       Int String)
- : (→ Int String (tyapp Pair Int String)))
-; Pair Int String value
-(check-type
- ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
-       Int String) 1 "1")
- : (tyapp Pair Int String))
-; fst: parametric
-(check-type
- (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
- : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) X)))
-; fst: concrete Pair Int String accessor
-(check-type
- (inst
-  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
-  Int String)
- : (→ (tyapp Pair Int String) Int))
-; apply fst
-(check-type
- ((inst
-   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
-   Int String)
-  ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
-         Int String) 1 "1"))
- : Int ⇒ 1)
-; snd
-(check-type
- (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
- : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) Y)))
-(check-type
- (inst
-  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
-  Int String)
- : (→ (tyapp Pair Int String) String))
-(check-type
- ((inst
-   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
-   Int String)
-  ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
-         Int String) 1 "1"))
- : String ⇒ "1")
-
-;;; sysf tests wont work, unless augmented with kinds
-(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
-
-(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
-(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
-(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
-
-(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
-
-(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
-
-(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
-
-(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
-(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
-; first inst should be discarded
-(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
-; second inst is discarded
-(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
-
-;; polymorphic arguments
-(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
-(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
-(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
-(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
-(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
-(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
-(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
-(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
-(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
-(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
-(check-type
- (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
-(check-type
- ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
- : Int ⇒ 10)
-(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
-(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
-(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
-             (Λ ([s : ★]) (λ ([y : s]) y)))
-             : Int ⇒ 10)
-
-
-;; previous tests -------------------------------------------------------------
-(check-type 1 : Int)
-(check-not-type 1 : (→ Int Int))
-(typecheck-fail #f) ; unsupported literal
-(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 is not valid type
-(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not 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 (tyλ ([t : ★]) t) : (⇒ ★ ★))
+;(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★))
+;(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★)))
+;(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★)))
+;(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
+;(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★))
+;
+;(check-type (tyapp (tyλ ([t : ★]) t) Int) : ★)
+;(check-type (λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) : (→ Int Int))
+;(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
+;(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
+;(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
+;(typecheck-fail ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
+;
+;;; partial-apply →
+;(check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)
+;            : (⇒ ★ ★))
+;; f's type must have kind ★
+;(typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f))
+;(check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) :
+;            (∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String))))
+;(check-type (inst
+;             (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+;             (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+;            : (→ (→ Int String) (→ Int String)))
+;;; applied f too early
+;(typecheck-fail (inst
+;                 (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
+;                 (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)))
+;(check-type ((inst
+;              (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+;              (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+;             (λ ([x : Int]) "int")) : (→ Int String))
+;(check-type (((inst
+;               (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+;              (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+;              (λ ([x : Int]) "int")) 1) : String ⇒ "int")
+;
+;; tapl examples, p441
+;(define-type-alias Id (tyλ ([X : ★]) X))
+;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
+;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int))
+;(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int))
+;(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int (tyapp Id String)) Int))
+;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) (tyapp Id String)) Int))
+;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) String) Int))
+;(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (→ Int String) Int))
+;(check-type (λ ([f : (→ Int String)]) 1) : (→ (tyapp Id (→ Int String)) Int))
+;(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (→ Int String)) Int))
+;(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int))
+;
+;; tapl examples, p451
+;(define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
+;
+;(check-type Pair : (⇒ ★ ★ ★))
+;
+;(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
+;;; parametric pair constructor
+;(check-type
+; (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+; : (∀ ([X : ★][Y : ★]) (→ X Y (tyapp Pair X Y))))
+;; concrete Pair Int String constructor
+;(check-type
+; (inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+;       Int String)
+; : (→ Int String (tyapp Pair Int String)))
+;; Pair Int String value
+;(check-type
+; ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+;       Int String) 1 "1")
+; : (tyapp Pair Int String))
+;; fst: parametric
+;(check-type
+; (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+; : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) X)))
+;; fst: concrete Pair Int String accessor
+;(check-type
+; (inst
+;  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+;  Int String)
+; : (→ (tyapp Pair Int String) Int))
+;; apply fst
+;(check-type
+; ((inst
+;   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+;   Int String)
+;  ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+;         Int String) 1 "1"))
+; : Int ⇒ 1)
+;; snd
+;(check-type
+; (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+; : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) Y)))
+;(check-type
+; (inst
+;  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+;  Int String)
+; : (→ (tyapp Pair Int String) String))
+;(check-type
+; ((inst
+;   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+;   Int String)
+;  ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+;         Int String) 1 "1"))
+; : String ⇒ "1")
+;
+;;;; sysf tests wont work, unless augmented with kinds
+;(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+;
+;(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
+;(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
+;(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
+;
+;(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+;            : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
+;
+;(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+;            : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
+;
+;(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+;            : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
+;
+;(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
+;(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
+;; first inst should be discarded
+;(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
+;; second inst is discarded
+;(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
+;
+;;; polymorphic arguments
+;(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
+;(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
+;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
+;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
+;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
+;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
+;(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
+;(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
+;(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
+;(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
+;(check-type
+; (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
+;(check-type
+; ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
+; : Int ⇒ 10)
+;(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
+;(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
+;(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
+;             (Λ ([s : ★]) (λ ([y : s]) y)))
+;             : Int ⇒ 10)
+;
+;
+;;; previous tests -------------------------------------------------------------
+;(check-type 1 : Int)
+;(check-not-type 1 : (→ Int Int))
+;(typecheck-fail #f) ; unsupported literal
+;(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 is not valid type
+;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not 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/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt
index 5125606..76474dd 100644
--- a/tapl/tests/rackunit-typechecking.rkt
+++ b/tapl/tests/rackunit-typechecking.rkt
@@ -3,7 +3,7 @@
 (provide (all-defined-out))
 
 (define-syntax (check-type stx)
-  (syntax-parse stx #:datum-literals (:)
+  (syntax-parse stx #:datum-literals (: ⇒)
     [(_ e : τ ⇒ v) #'(check-type-and-result e : τ ⇒ v)]
     [(_ e : τ-expected:type)
      #:with τ (typeof (expand/df #'e))
diff --git a/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
index 0a3e91e..8618c91 100644
--- a/tapl/tests/run-all-tests.rkt
+++ b/tapl/tests/run-all-tests.rkt
@@ -11,16 +11,16 @@
 
 (require "stlc+rec-iso-tests.rkt")
 
-;(require "exist-tests.rkt")
+(require "exist-tests.rkt")
 
 ;; subtyping
-;(require "stlc+sub-tests.rkt")
+(require "stlc+sub-tests.rkt")
 ;(require "stlc+reco+sub-tests.rkt")
-;(require "fsub-tests.rkt")
+;;(require "fsub-tests.rkt")
 ;
 ;;; system F
 ;(require "sysf-tests.rkt")
-;
+
 ;;; F_omega
 ;(require "fomega-tests.rkt")
 ;(require "fomega2-tests.rkt")
\ No newline at end of file
diff --git a/tapl/tests/stlc+box-tests.rkt b/tapl/tests/stlc+box-tests.rkt
index 742ce76..a80fce4 100644
--- a/tapl/tests/stlc+box-tests.rkt
+++ b/tapl/tests/stlc+box-tests.rkt
@@ -13,8 +13,24 @@
 (check-type ((λ ([b : (Ref Int)]) (deref b)) (ref 10)) : Int ⇒ 10)
 (check-type ((λ ([b : (Ref Int)]) (begin (begin (:= b 20) (deref b)))) (ref 10)) : Int ⇒ 20)
 
-(typecheck-fail (λ ([lst : (Ref Int Int)]) lst)) ; type constructor wrong arity
-(typecheck-fail (λ ([lst : (Ref)]) lst)) ; type constructor wrong arity
+;; Ref err msgs
+; wrong arity
+(typecheck-fail
+ (λ ([lst : (Ref Int Int)]) lst)
+ #:with-msg
+ "Improper usage of type constructor Ref: \\(Ref Int Int), expected pattern \\(Ref τ)")
+(typecheck-fail
+ (λ ([lst : (Ref)]) lst)
+ #:with-msg
+ "Improper usage of type constructor Ref: \\(Ref), expected pattern \\(Ref τ)")
+(typecheck-fail
+ (deref 1)
+ #:with-msg
+ "Expected type of expression.+to match pattern \\(Ref τ), got: Int")
+(typecheck-fail
+ (:= 1 1)
+ #:with-msg
+ "Expected type of expression.+to match pattern \\(Ref τ), got: Int")
 
 ;; previous tests: ------------------------------------------------------------
 (typecheck-fail (cons 1 2))
@@ -49,69 +65,69 @@
 (check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int))
 
 (check-type "Stephen" : String)
-(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-            (× [: "name" String] [: "phone" Int] [: "male?" Bool]))
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(check-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+            (× [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")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
             : String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone)
             : Int ⇒ 781)
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
+(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]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-                (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-                (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [my-name : String] [phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [name : String] [my-phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [name : String] [phone : Int] [is-male? : Bool]))
 
 
-(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
+ (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
+ (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
+ (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
+ (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]))
+ (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])
+        (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])
+ (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: ------------------------------------------------------------
diff --git a/tapl/tests/stlc+cons-tests.rkt b/tapl/tests/stlc+cons-tests.rkt
index 3221af6..6d64eb8 100644
--- a/tapl/tests/stlc+cons-tests.rkt
+++ b/tapl/tests/stlc+cons-tests.rkt
@@ -34,6 +34,12 @@
 (check-type ((head fn-lst) 25) : Int ⇒ 35)
 (check-type (tail fn-lst) : (List (→ Int Int)) ⇒ (nil {(→ Int Int)}))
 
+; more list errors
+(typecheck-fail
+ (cons 1 1)
+ #:with-msg
+ "Expected type of expression to match pattern \\(List τ), got: Int")
+
 ;; previous tests: ------------------------------------------------------------
 ;; define-type-alias
 (define-type-alias Integer Int)
@@ -47,69 +53,69 @@
 
 ;; records (ie labeled tuples)
 (check-type "Stephen" : String)
-(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-            (× [: "name" String] [: "phone" Int] [: "male?" Bool]))
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(check-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+            (× [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")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
             : String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone)
             : Int ⇒ 781)
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
+(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]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-                (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-                (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [my-name : String] [phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [name : String] [my-phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [name : String] [phone : Int] [is-male? : Bool]))
 
 
-(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
+ (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]
+ (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
+ (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
+ (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]))
+ (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])
+        (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])
+ (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: ------------------------------------------------------------
diff --git a/tapl/tests/stlc+lit-tests.rkt b/tapl/tests/stlc+lit-tests.rkt
index a30a4d8..3a24e78 100644
--- a/tapl/tests/stlc+lit-tests.rkt
+++ b/tapl/tests/stlc+lit-tests.rkt
@@ -13,27 +13,27 @@
 
 (typecheck-fail
  (λ ([x : →]) x)
- #:with-msg "Improper usage of type constructor →: →, expected pattern")
+ #:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments")
 (typecheck-fail
  (λ ([x : (→ →)]) x)
- #:with-msg "Improper usage of type constructor →: →, expected pattern")
+ #:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments")
 (typecheck-fail
  (λ ([x : (→)]) x)
- #:with-msg "Improper usage of type constructor →: \\(→\\), expected pattern")
+ #:with-msg "Improper usage of type constructor →: \\(→), expected >= 1 arguments")
 
 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
 
 (typecheck-fail ((λ ([x : Bool]) x) 1)
-                #:with-msg "not a valid type: Bool")
+                #:with-msg "Bool: unbound identifier")
 (typecheck-fail (λ ([x : (→ Bool Bool)]) x)
-                #:with-msg "not a valid type: Bool")
+                #:with-msg "Bool: unbound identifier")
 (typecheck-fail (λ ([x : Bool]) x)
-                #:with-msg "not a valid type: Bool")
+                #:with-msg "Bool: unbound identifier")
 (typecheck-fail
  (λ ([f : Int]) (f 1 2))
  #:with-msg
- "Expected type of expression to match pattern \\(→ τ_in ... τ_out\\), got: Int")
+ "Expected expression f to have → type, 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+rec-iso-tests.rkt b/tapl/tests/stlc+rec-iso-tests.rkt
index c97fbbc..29beedf 100644
--- a/tapl/tests/stlc+rec-iso-tests.rkt
+++ b/tapl/tests/stlc+rec-iso-tests.rkt
@@ -1,15 +1,15 @@
 #lang s-exp "../stlc+rec-iso.rkt"
 (require "rackunit-typechecking.rkt")
 
-(define-type-alias IntList (μ [[X]] (∨ [<> "nil" Unit] [<> "cons" (× Int X)])))
-(define-type-alias ILBody (∨ [<> "nil" Unit] [<> "cons" (× Int IntList)]))
+(define-type-alias IntList (μ (X) (∨ [nil : Unit] [cons : (× Int X)])))
+(define-type-alias ILBody (∨ [nil : Unit] [cons : (× Int IntList)]))
 
 ;; nil
-(define nil (fld {IntList} (var "nil" = (void) as ILBody)))
+(define nil (fld {IntList} (var nil = (void) as ILBody)))
 (check-type nil : IntList)
 
 ;; cons
-(define cons (λ ([n : Int] [lst : IntList]) (fld {IntList} (var "cons" = (tup n lst) as ILBody))))
+(define cons (λ ([n : Int] [lst : IntList]) (fld {IntList} (var cons = (tup n lst) as ILBody))))
 (check-type cons : (→ Int IntList IntList))
 (check-type (cons 1 nil) : IntList)
 (typecheck-fail (cons 1 2))
@@ -19,8 +19,8 @@
 (define isnil
   (λ ([lst : IntList])
     (case (unfld {IntList} lst)
-      ["nil" n => #t]
-      ["cons" p => #f])))
+      [nil n => #t]
+      [cons p => #f])))
 (check-type isnil : (→ IntList Bool))
 (check-type (isnil nil) : Bool ⇒ #t)
 (check-type (isnil (cons 1 nil)) : Bool ⇒ #f)
@@ -33,8 +33,8 @@
 (define hd
   (λ ([lst : IntList])
     (case (unfld {IntList} lst)
-      ["nil" n => 0]
-      ["cons" p => (proj p 0)])))
+      [nil n => 0]
+      [cons p => (proj p 0)])))
 (check-type hd : (→ IntList Int))
 (check-type (hd nil) : Int ⇒ 0)
 (typecheck-fail (hd 1))
@@ -44,14 +44,24 @@
 (define tl
   (λ ([lst : IntList])
     (case (unfld {IntList} lst)
-      ["nil" n => lst]
-      ["cons" p => (proj p 1)])))
+      [nil n => lst]
+      [cons p => (proj p 1)])))
 (check-type tl : (→ IntList IntList))
 (check-type (tl nil) : IntList ⇒ nil)
 (check-type (tl (cons 1 nil)) : IntList ⇒ nil)
 (check-type (tl (cons 1 (cons 2 nil))) : IntList ⇒ (cons 2 nil))
 (typecheck-fail (tl 1))
 
+;; some typecheck failure msgs
+(typecheck-fail
+ (fld {Int} 1)
+ #:with-msg
+ "Expected type of expression to match pattern \\(μ \\(\\(tv)) τ_body), got: Int")
+(typecheck-fail
+ (unfld {Int} 1)
+ #:with-msg
+ "Expected type of expression to match pattern \\(μ \\(\\(tv)) τ_body), got: Int")
+
 ;; previous stlc+var tests ----------------------------------------------------
 ;; define-type-alias
 (define-type-alias Integer Int)
@@ -85,50 +95,50 @@
 ;                (× [: "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
+ (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
+ (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
+ (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
+ (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]))
+ (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])
+        (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])
+ (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: ------------------------------------------------------------
diff --git a/tapl/tests/stlc+reco+sub-tests.rkt b/tapl/tests/stlc+reco+sub-tests.rkt
index 9072fc1..6d4325a 100644
--- a/tapl/tests/stlc+reco+sub-tests.rkt
+++ b/tapl/tests/stlc+reco+sub-tests.rkt
@@ -4,10 +4,10 @@
 ;; record subtyping tests
 (check-type "coffee" : String)
 (check-type (tup ["coffee" = 3]) : (× [: "coffee" Int])) ; element subtyping
-(check-type (var "coffee" = 3 as (∨ [: "coffee" Nat])) : (∨ [: "coffee" Int])) ; element subtyping
+(check-type (var "coffee" = 3 as (∨ [<> "coffee" Nat])) : (∨ [<> "coffee" Int])) ; element subtyping
 (check-type (tup ["coffee" = 3]) : (× [: "coffee" Nat]))
 (check-type (tup ["coffee" = 3]) : (× [: "coffee" Top]))
-(check-type (var "coffee" = 3 as (∨ [: "coffee" Int])) : (∨ [: "coffee" Top])) ; element subtyping (twice)
+(check-type (var "coffee" = 3 as (∨ [<> "coffee" Int])) : (∨ [<> "coffee" Top])) ; element subtyping (twice)
 (check-type (tup ["coffee" = 3]) : (× [: "coffee" Num]))
 (check-not-type (tup ["coffee" = -3]) : (× [: "coffee" Nat]))
 (check-type (tup ["coffee" = -3]) : (× [: "coffee" Num]))
diff --git a/tapl/tests/stlc+reco+var-tests.rkt b/tapl/tests/stlc+reco+var-tests.rkt
index 2c630d4..622245e 100644
--- a/tapl/tests/stlc+reco+var-tests.rkt
+++ b/tapl/tests/stlc+reco+var-tests.rkt
@@ -15,78 +15,119 @@
 ; 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]))
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(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]))
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
             : String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
             : String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone)
             : Int ⇒ 781)
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
+(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]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-                (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-                (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [my-name : String] [phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [name : String] [my-phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [name : String] [phone : Int] [is-male? : Bool]))
+
+;; record errors
+(typecheck-fail
+ (proj 1 "a")
+ #:with-msg
+ "expected identifier")
+(typecheck-fail
+ (proj 1 a)
+ #:with-msg
+ "Expected expression 1 to have × type, got: Int")
 
 ;; 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])) : (∨ [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])))
                 #:with-msg "Arguments to function.+have wrong type")
-(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] [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])
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+   [coffee x => 1])
  #:with-msg "wrong number of case clauses")
 (typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
-   ["coffee" x => 1]
-   ["teaaaaaa" x => 2])
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+   [coffee x => 1]
+   [teaaaaaa x => 2])
  #:with-msg "case clauses not exhaustive")
 (typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
-   ["coffee" x => 1]
-   ["tea" x => 2]
-   ["coke" x => 3])
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+   [coffee x => 1]
+   [tea x => 2]
+   [coke x => 3])
  #:with-msg "wrong number of case clauses")
 (typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
-   ["coffee" x => "1"]
-   ["tea" x => 2])
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+   [coffee x => "1"]
+   [tea x => 2])
  #:with-msg "branches have different 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]))
+ (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])
+        (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])
+ (case ((λ ([d : Drink]) d) (var coffee = 1 as Drink))
+   [coffee x => (+ (+ x x) (+ x x))]
+   [tea x => 2]
+   [coke y => 3])
  : Int ⇒ 4)
 
+;; variant errors
+(typecheck-fail
+ (var name = "Steve" as Int)
+ #:with-msg
+ "Expected ∨ type, got: Int")
+(typecheck-fail
+ (case 1 [racket x => 1])
+ #:with-msg
+ "Expected expression 1 to have ∨ type, got: Int")
+(typecheck-fail
+ (λ ([x : (∨)]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨), expected \\(∨ [label:id : τ:type] ...+)")
+(typecheck-fail
+ (λ ([x : (∨ 1)]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ 1\\), expected \\(∨ [label:id : τ:type] ...+)")
+(typecheck-fail
+ (λ ([x : (∨ [1 2])]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ (1 2)), expected \\(∨ [label:id : τ:type] ...+)")
+(typecheck-fail
+ (λ ([x : (∨ [a 2])]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ (a 2)), expected \\(∨ [label:id : τ:type] ...+)")
+(typecheck-fail
+ (λ ([x : (∨ [a Int])]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ (a Int)), expected \\(∨ [label:id : τ:type] ...+)")
+(typecheck-fail
+ (λ ([x : (∨ [1 : Int])]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ (1 : Int)), expected \\(∨ [label:id : τ:type] ...+)")
+(typecheck-fail
+ (λ ([x : (∨ [a : 1])]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ (a : 1)), expected \\(∨ [label:id : τ:type] ...+)")
+
 ;; previous tuple tests: ------------------------------------------------------------
 ;; wont work anymore
 ;;(check-type (tup 1 2 3) : (× Int Int Int))
diff --git a/tapl/tests/stlc+tup-tests.rkt b/tapl/tests/stlc+tup-tests.rkt
index 10c3529..4f38f09 100644
--- a/tapl/tests/stlc+tup-tests.rkt
+++ b/tapl/tests/stlc+tup-tests.rkt
@@ -17,7 +17,7 @@
 (typecheck-fail
  (proj 1 2)
  #:with-msg
- "Expected type of expression 1 to match pattern \\(× τ ...\\), got: Int")
+ "Expected expression 1 to have × type, got: Int")
 
 ;; ext-stlc.rkt tests ---------------------------------------------------------
 ;; should still pass
diff --git a/tapl/tests/sysf-tests.rkt b/tapl/tests/sysf-tests.rkt
index 748cb60..d76da29 100644
--- a/tapl/tests/sysf-tests.rkt
+++ b/tapl/tests/sysf-tests.rkt
@@ -1,20 +1,20 @@
 #lang s-exp "../sysf.rkt"
 (require "rackunit-typechecking.rkt")
 
-(check-type (Λ (X) (λ ([x : X]) x)) : (∀ (X) (→ X X)))
+(check-type (Λ (X) (λ ([x : X]) x)) : (∀ [[X]] (→ X X)))
 
-(check-type (Λ (X) (λ ([t : X] [f : X]) t)) : (∀ (X) (→ X X X))) ; true
-(check-type (Λ (X) (λ ([t : X] [f : X]) f)) : (∀ (X) (→ X X X))) ; false
-(check-type (Λ (X) (λ ([t : X] [f : X]) f)) : (∀ (Y) (→ Y Y Y))) ; false, alpha equiv
+(check-type (Λ (X) (λ ([t : X] [f : X]) t)) : (∀ [[X]] (→ X X X))) ; true
+(check-type (Λ (X) (λ ([t : X] [f : X]) f)) : (∀ [[X]] (→ X X X))) ; false
+(check-type (Λ (X) (λ ([t : X] [f : X]) f)) : (∀ [[Y]] (→ Y Y Y))) ; false, alpha equiv
 
 (check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ (t1) (∀ (t2) (→ t1 (→ t2 t2)))))
+            : (∀ [[t1]] (∀ [[t2]] (→ t1 (→ t2 t2)))))
 
 (check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ (t3) (∀ (t4) (→ t3 (→ t4 t4)))))
+            : (∀ [[t3]] (∀ [[t4]] (→ t3 (→ t4 t4)))))
 
 (check-not-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ (t4) (∀ (t3) (→ t3 (→ t4 t4)))))
+            : (∀ [[t4]] (∀ [[t3]] (→ t3 (→ t4 t4)))))
 
 (check-type (inst (Λ (t) (λ ([x : t]) x)) Int) : (→ Int Int))
 (check-type (inst (Λ (t) 1) (→ Int Int)) : Int)
@@ -23,30 +23,36 @@
 ; second inst is discarded
 (check-type (inst (inst (Λ (t1) (Λ (t2) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
 
-;;; polymorphic arguments
-(check-type (Λ (t) (λ ([x : t]) x)) : (∀ (t) (→ t t)))
-(check-type (Λ (t) (λ ([x : t]) x)) : (∀ (s) (→ s s)))
-(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (s) (∀ (t) (→ t t))))
-(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (t) (→ t t))))
-(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (s) (→ s s))))
-(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (u) (→ u u))))
-(check-type (λ ([x : (∀ (t) (→ t t))]) x) : (→ (∀ (s) (→ s s)) (∀ (u) (→ u u))))
-(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
-(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
-(check-type ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) : (∀ (u) (→ u u)))
+;; inst err
+(typecheck-fail
+ (inst 1 Int)
+ #:with-msg
+ "Expected type of expression to match pattern \\(∀ \\(\\(x ...)) body), got: Int")
+
+;; polymorphic arguments
+(check-type (Λ (t) (λ ([x : t]) x)) : (∀ [[t]] (→ t t)))
+(check-type (Λ (t) (λ ([x : t]) x)) : (∀ [[s]] (→ s s)))
+(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ [[s]] (∀ [[t]] (→ t t))))
+(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ [[r]] (∀ [[t]] (→ t t))))
+(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ [[r]] (∀ [[s]] (→ s s))))
+(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ [[r]] (∀ [[u]] (→ u u))))
+(check-type (λ ([x : (∀ [[t]] (→ t t))]) x) : (→ (∀ [[s]] (→ s s)) (∀ [[u]] (→ u u))))
+(typecheck-fail ((λ ([x : (∀ [[t]] (→ t t))]) x) (λ ([x : Int]) x)))
+(typecheck-fail ((λ ([x : (∀ [[t]] (→ t t))]) x) 1))
+(check-type ((λ ([x : (∀ [[t]] (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) : (∀ [[u]] (→ u u)))
 (check-type
- (inst ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) : (→ Int Int))
+ (inst ((λ ([x : (∀ [[t]] (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) : (→ Int Int))
 (check-type
- ((inst ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) 10)
+ ((inst ((λ ([x : (∀ [[t]] (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) 10)
  : Int ⇒ 10)
-(check-type (λ ([x : (∀ (t) (→ t t))]) (inst x Int)) : (→ (∀ (t) (→ t t)) (→ Int Int)))
-(check-type (λ ([x : (∀ (t) (→ t t))]) ((inst x Int) 10)) : (→ (∀ (t) (→ t t)) Int))
-(check-type ((λ ([x : (∀ (t) (→ t t))]) ((inst x Int) 10))
+(check-type (λ ([x : (∀ [[t]] (→ t t))]) (inst x Int)) : (→ (∀ [[t]] (→ t t)) (→ Int Int)))
+(check-type (λ ([x : (∀ [[t]] (→ t t))]) ((inst x Int) 10)) : (→ (∀ [[t]] (→ t t)) Int))
+(check-type ((λ ([x : (∀ [[t]] (→ t t))]) ((inst x Int) 10))
              (Λ (s) (λ ([y : s]) y)))
              : Int ⇒ 10)
 
 
-;;; previous tests -------------------------------------------------------------
+;; previous tests -------------------------------------------------------------
 (check-type 1 : Int)
 (check-not-type 1 : (→ Int Int))
 (typecheck-fail "one") ; unsupported literal
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index aa917cd..ee7629d 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -10,7 +10,8 @@
 (provide 
  (for-syntax (all-defined-out)) (all-defined-out)
  (for-syntax
-  (all-from-out racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt")))
+  (all-from-out racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt"))
+ (for-meta 2 (all-from-out racket/base syntax/parse)))
 
 ;; type checking functions/forms
 
@@ -54,59 +55,141 @@
                             (regexp-replace pre-pat name ""))))
                    (all-from-out base-lang))))]))
                  
-;; when combining #%type's with #%plain-type's, eg when inferring type for λ
-;; (call this mixed type) we create a type that still needs expansion, ie eval
-;; With the #%type and #%plain-type distinction, mixed types can be evaled
-;; and the #%plain-type will wrappers will simply go away
-(define-syntax #%type (syntax-parser [(_ τ) #'τ]))       ; surface stx
-(define-syntax #%plain-type (syntax-parser [(_ τ) #'τ])) ; expanded representation
 
-(define-syntax (define-base-type stx)
-  (syntax-parse stx
-    [(_ τ:id)
-     #:with τ? (format-id #'τ "~a?" #'τ)
-     #:with τ-internal (generate-temporary #'τ)
-     #:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
-     #:with τ-cls (generate-temporary #'τ)
-     #'(begin
-         (provide τ (for-syntax τ? inferτ+erase))
-         (define τ-internal
-           (λ () (raise (exn:fail:type:runtime
-                         (format "~a: Cannot use type at run time" 'τ)
-                         (current-continuation-marks)))))
-         (define-syntax (τ stx)
-           (syntax-parse stx
-             [x:id (add-orig #'(#%type (τ-internal)) #'τ)]))
-         (begin-for-syntax
-           ; expanded form of τ
-           (define-syntax-class τ-cls
-             (pattern ((~literal #%plain-type) ((~literal #%plain-app) ty))))
-           (define (τ? t)
-             (syntax-parse ((current-type-eval) t)
-               [expanded-type
-                #:declare expanded-type τ-cls
-                (typecheck? #'expanded-type.ty #'τ-internal)]))
-           (define (inferτ+erase e)
-             (syntax-parse (infer+erase e) #:context e
-               [(e- expanded-type)
-                #:declare expanded-type τ-cls
-                #:fail-unless (typecheck? #'expanded-type.ty #'τ-internal)
-                              (format
-                               "~a (~a:~a): Expected type of expression ~v to be ~a, got: ~a"
-                               (syntax-source e) (syntax-line e) (syntax-column e)
-                               (syntax->datum e) (type->str #'τ) (type->str #'expanded-type))
-                #'e-]))))]))
+
+;; type assignment
+(begin-for-syntax
+  ;; macro for nicer syntax
+  (define-syntax (⊢ stx)
+    (syntax-parse stx #:datum-literals (:)
+      [(_ e : τ) #'(assign-type #'e #`τ)]
+      [(_ e τ) #'(⊢ e : τ)]))
+       
+  ;; assign-type Type -> Syntax
+  ;; Attaches type τ to (expanded) expression e.
+  ;; must eval here, to catch unbound types
+  (define (assign-type e τ #:tag [tag 'type])
+    (syntax-property e tag (syntax-local-introduce ((current-type-eval) τ))))
+  
+  ;; typeof : Syntax -> Type or #f
+  ;; Retrieves type of given stx, or #f if input has not been assigned a type.
+  (define (typeof stx #:tag [tag 'type]) (syntax-property stx tag))
+  
+  ;; infers the type and erases types in an expression
+  (define (infer+erase e)
+    (define e+ (expand/df e))
+    (list e+ (typeof e+)))
+  ;; infers the types and erases types in multiple expressions
+  (define (infers+erase es)
+    (stx-map infer+erase es))
+
+  ;; This is the main "infer" function. All others are defined in terms of this.
+  ;; It should be named infer+erase but leaving it for now for backward compat.
+  ;; NOTE: differs slightly from infer/type-ctxt+erase in that types are not
+  ;; expanded before wrapping in lambda
+  ;; - This caused one problem in fomega2.rkt #%app, but I just had to expand
+  ;; the types before typechecking, which is acceptable
+  (define (infer es #:ctx [ctx null] #:tvctx [tvctx null] #:tag [tag 'type])
+    (syntax-parse ctx #:datum-literals (:)
+      [([x : τ] ...) ; dont expand yet bc τ may have references to tvs
+       #:with ([tv : k] ...) tvctx
+       #:with (e ...) es
+       #:with
+       ; old expander pattern
+       #;((~literal #%plain-lambda) tvs+
+        ((~literal #%expression)
+         ((~literal #%plain-lambda) xs+
+          ((~literal letrec-syntaxes+values) stxs1 ()
+            ((~literal letrec-syntaxes+values) stxs2 ()
+              ((~literal #%expression) e+) ...)))))
+       ; new expander pattern
+       ((~literal #%plain-lambda) tvs+
+        ((~literal let-values) () ((~literal let-values) ()
+         ((~literal #%expression)
+          ((~literal #%plain-lambda) xs+
+           ((~literal let-values) () ((~literal let-values) ()
+            ((~literal #%expression) e+) ...)))))))
+       (expand/df
+        #`(λ (tv ...)
+            (let-syntax ([tv (make-rename-transformer (assign-type #'tv #'k #:tag '#,tag))] ...)
+              (λ (x ...)
+                (let-syntax ([x (make-rename-transformer (assign-type #'x #'τ #:tag '#,tag))] ...)
+                  (#%expression e) ...)))))
+       (list #'tvs+ #'xs+ #'(e+ ...)
+             (stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
+      [([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvctx tvctx)]))
+
+  ;; fns derived from infer ---------------------------------------------------
+  ;; some are syntactic shortcuts, some are for backwards compat
+
+  ;; shorter name
+  (define (infer/ctx+erase ctx e)
+    (syntax-parse (infer (list e) #:ctx ctx)
+      [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
+  ;; infers type and erases types in a single expression,
+  ;; in the context of the given bindings and their types
+  (define (infer/type-ctxt+erase x+τs e)
+    (syntax-parse (infer (list e) #:ctx x+τs)
+      [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
+  ;; infers type and erases types in multiple expressions,
+  ;; in the context of (one set of) given bindings and their tpyes
+  (define (infers/type-ctxt+erase ctxt es)
+    (stx-cdr (infer es #:ctx ctxt)))
+  ;; infers and erases types in an expression, in the context of given type vars
+  #;(define (infer/tvs+erase e tvs)
+    (syntax-parse (infer (list e) #:tvs tvs)
+      [(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
+
+  ; type parameters, for type checker aspects that require extension
+  (define current-typecheck-relation (make-parameter #f))
+  (define (typecheck? t1 t2)
+    ((current-typecheck-relation) t1 t2)) ;((current-type-eval) t1) ((current-type-eval) t2)))
+  (define (typechecks? τs1 τs2)
+    (and (= (stx-length τs1) (stx-length τs2))
+         (stx-andmap typecheck? τs1 τs2)))
+  
+  (define current-type-eval (make-parameter #f))
+  (define (type-evals τs) #`#,(stx-map (current-type-eval) τs))
+
+  ; get rid of this?
+  (define current-promote (make-parameter (λ (x) x)))
+
+  ;; term expansion
+  ;; expand/df : Syntax -> Syntax
+  ;; Local expands the given syntax object. 
+  ;; The result always has a type (ie, a 'type stx-prop).
+  ;; Note: 
+  ;; local-expand must expand all the way down, ie stop-ids == null
+  ;; If stop-ids is #f, then subexpressions won't get expanded and thus won't
+  ;; get assigned a type.
+  (define (expand/df e)
+    (local-expand e 'expression null))
+
+  (struct exn:fail:type:check exn:fail:user ())
+
+  ;; type-error #:src Syntax #:msg String Syntax ...
+  ;; usage:
+  ;; type-error #:src src-stx
+  ;;            #:msg msg-string msg-args ...
+  (define-syntax-rule (type-error #:src stx-src #:msg msg args ...)
+    (raise
+     (exn:fail:type:check
+      (format (string-append "TYPE-ERROR: ~a (~a:~a): " msg) 
+              (syntax-source stx-src) (syntax-line stx-src) (syntax-column stx-src) 
+              (type->str args) ...)
+      (current-continuation-marks)))))
 
 (begin-for-syntax
   ;; type validation
   ;; only check outer wrapper; tycons are responsible for verifying their own args
-  (define (is-type? τ)
+  (define (#%type? t) (typecheck? t #'#%type))
+  #;(define (is-type? τ)
     (or (plain-type? τ)
         ; partial expand to reveal #%type wrapper
         (syntax-parse (local-expand τ 'expression (list #'#%type))
           [((~literal #%type) _) #t] [_ #f])))
   (define (plain-type? τ)
-    (syntax-parse τ [((~literal #%plain-type) _) #t] [_ #f]))
+    (and (typeof τ) (typecheck? (typeof τ) #'#%type) τ))
 
   ; surface type syntax is saved as the value of the 'orig property
   (define (add-orig stx orig)
@@ -127,7 +210,7 @@
   ;; - type
   ;; - type constructor identifier
   ;; - syntax-class representing shape of arguments to tycon
-  (define-syntax (match-type stx)
+  #;(define-syntax (match-type stx)
     (syntax-parse stx
       [(_ ty tycon cls)
        #'(syntax-parse ((current-type-eval) ty)
@@ -148,22 +231,186 @@
     (define paren-shape/#f (syntax-property stx 'paren-shape))
     (and paren-shape/#f (char=? paren-shape/#f #\[)))
   (define-syntax-class bound-vars
-    (pattern (~and stx [[x:id ...]])
-             #:when (and (bracket? #'stx)
-                         (bracket? (stx-car #'stx)))))
+    (pattern
+     (~and stx [[x:id ...]]
+           #;[[(~and x:id (~not (~literal ...))) ... (~optional (~literal ...))]])
+     #:when (and (bracket? #'stx)
+                 (bracket? (stx-car #'stx)))))
   (begin-for-syntax
     (define (bracket? stx)
       (define paren-shape/#f (syntax-property stx 'paren-shape))
       (and paren-shape/#f (char=? paren-shape/#f #\[)))
     (define-syntax-class bound-vars
-      (pattern (~and stx [[x:id ...]])
-               #:when (and (bracket? #'stx)
-                           (bracket? (stx-car #'stx)))))))
+      (pattern
+       (~and stx [[x:id ...]]
+             #;[[(~and x:id (~not (~literal ...))) ... (~optional (~literal ...))]])
+       #:when (and (bracket? #'stx)
+                   (bracket? (stx-car #'stx)))))))
 
-(define-syntax define-type-constructor
+(begin-for-syntax
+  (define (mk-? id) (format-id id "~a?" id)))
+
+(define #%type void)
+(define-for-syntax (mk-type t) (assign-type t #'#%type))
+
+#;(define-syntax (define-base-type stx)
+  (syntax-parse stx
+    [(_ τ:id)
+     #:with τ? (format-id #'τ "~a?" #'τ)
+     #:with τ-internal (generate-temporary #'τ)
+     #:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
+     #:with τ-cls (generate-temporary #'τ)
+     #:with τ-expander (format-id #'τ "~~~a" #'τ)
+     #'(begin
+         (provide τ (for-syntax τ? inferτ+erase τ-expander))
+         (define τ-internal
+           (λ () (raise (exn:fail:type:runtime
+                         (format "~a: Cannot use type at run time" 'τ)
+                         (current-continuation-marks)))))
+         (define-syntax (τ stx)
+           (syntax-parse stx
+             [x:id (add-orig #'(#%type (τ-internal)) #'τ)]))
+         (begin-for-syntax
+           ; expanded form of τ
+           (define-syntax-class τ-cls
+             (pattern ((~literal #%plain-type) ((~literal #%plain-app) ty))))
+           (define (τ? t)
+             (syntax-parse ((current-type-eval) t)
+               [expanded-type
+                #:declare expanded-type τ-cls
+                (typecheck? #'expanded-type.ty #'τ-internal)]))
+           ; base type pattern expanders should be identifier macros but
+           ; parsing them is ambiguous, so handle and pass through other args
+           (define-syntax τ-expander
+             (pattern-expander
+              (syntax-parser
+                [ty:id #'((~literal #%plain-type)
+                          ((~literal #%plain-app)
+                           (~literal τ-internal)))]
+                [(_ . rst)
+                 #'(((~literal #%plain-type)
+                     ((~literal #%plain-app)
+                      (~literal τ-internal))) . rst)])))
+           (define (inferτ+erase e)
+             (syntax-parse (infer+erase e) #:context e
+               [(e- expanded-type)
+                #:declare expanded-type τ-cls
+                #:fail-unless (typecheck? #'expanded-type.ty #'τ-internal)
+                              (format
+                               "~a (~a:~a): Expected type of expression ~v to be ~a, got: ~a"
+                               (syntax-source e) (syntax-line e) (syntax-column e)
+                               (syntax->datum e) (type->str #'τ) (type->str #'expanded-type))
+                #'e-]))))]))
+
+(define-syntax define-basic-checked-id-stx
   (syntax-parser
-    [(_ (τ:id (~optional (~and bvs-pat:bound-vars bvs-test)
-                         #:defaults ([bvs-pat.stx #'[[]]]))
+    [(_ τ:id)
+     #:with τ? (format-id #'τ "~a?" #'τ)
+     #:with τ-internal (generate-temporary #'τ)
+     #:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
+     #:with τ-cls (generate-temporary #'τ)
+     #:with τ-expander (format-id #'τ "~~~a" #'τ)
+     #'(begin
+         (provide τ (for-syntax τ? τ-expander))
+         (begin-for-syntax
+           (define (τ? t) (typecheck? t #'τ-internal))
+           (define (inferτ+erase e)
+             (syntax-parse (infer+erase e) #:context e
+               [(e- e_τ)
+                #:fail-unless (τ? #'e_τ)
+                (format
+                 "~a (~a:~a): Expected expression ~v to have type ~a, got: ~a"
+                 (syntax-source e) (syntax-line e) (syntax-column e)
+                 (syntax->datum e) (type->str #'τ) (type->str #'e_τ))
+                #'e-]))
+           (define-syntax τ-expander
+             (pattern-expander
+              (syntax-parser
+                [ty:id #'(~literal τ-internal)]
+                [(_ . rst)
+                 #'((~literal τ-internal) . rst)]))))
+         (define τ-internal
+           (λ () (raise (exn:fail:type:runtime
+                         (format "~a: Cannot use type at run time" 'τ)
+                         (current-continuation-marks)))))
+         (define-syntax τ
+           (syntax-parser
+             [(~var _ id) (add-orig (assign-type #'τ-internal #'#%type) #'τ)])))]))
+
+(define-syntax define-base-type (syntax-parser [(_ τ:id) #'(define-basic-checked-id-stx τ)]))
+
+(define-syntax (define-basic-checked-stx stx)
+  (syntax-parse stx
+    [(_ τ:id (~optional
+              (~seq #:arity op n:exact-nonnegative-integer)
+              #:defaults ([op #'>=] [n #'0])))
+     #:with τ-internal (generate-temporary #'τ)
+     #:with τ? (mk-? #'τ)
+     #:with τ-expander (format-id #'τ "~~~a" #'τ)
+     #:with τ-expander* (format-id #'τ-expander "~a*" #'τ-expander)
+     #:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
+     #'(begin
+         (provide τ (for-syntax τ-expander τ-expander* inferτ+erase))
+         (begin-for-syntax
+           (define-syntax τ-expander
+             (pattern-expander
+              (syntax-parser
+                [(_ . pat)
+                 #'((~literal #%plain-app) (~literal τ-internal) . pat)])))
+           (define-syntax τ-expander*
+             (pattern-expander
+              (syntax-parser
+                [(_ . pat)
+                 #'(~or
+                    ;((~literal #%plain-app) (~literal τ-internal) . pat)
+                    (τ-expander . pat)
+                    (~and
+                     any
+                     (~do
+                      (type-error #:src #'any
+                                  #:msg
+                                  "Expected ~a type, got: ~a"
+                                  #'τ #'any))))])))
+           (define (τ? t) (and (stx-pair? t) (typecheck? (stx-cadr t) #'τ-internal)))
+           (define (inferτ+erase e)
+             (syntax-parse (infer+erase e) #:context e
+               [(e- τ_e)
+                #:fail-unless (stx-pair? #'τ_e)
+                (format
+                 "~a (~a:~a): Expected expression ~a to have ~a type, got: ~a"
+                 (syntax-source e) (syntax-line e) (syntax-column e)
+                 (syntax->datum e) 'τ (type->str #'τ_e))
+                #:with ((~literal #%plain-app) tycon . args) #'τ_e
+                #:fail-unless (typecheck? #'tycon #'τ-internal)
+                (format
+                 "~a (~a:~a): Expected expression ~a to have ~a type, got: ~a"
+                 (syntax-source e) (syntax-line e) (syntax-column e)
+                 (syntax->datum e) 'τ (type->str #'τ_e))
+                #`(e- args)])))
+         (define τ-internal
+           (λ _ (raise (exn:fail:type:runtime
+                        (format "~a: Cannot use type at run time" 'τ)
+                        (current-continuation-marks)))))
+         ;(define (τ? ty) (syntax-parser ty [((~literal τ) . pat) #t][_ #f]))
+         ;; ; this is the actual constructor
+         (define-syntax (τ stx)
+           (syntax-parse stx
+             [(_ . args)
+              #:fail-unless (op (stx-length #'args) n)
+                            (format "wrong number of arguments, expected ~a ~a" 'op 'n)
+              #:with (~! (~var ty type) (... ...)) #'args
+;              #:with (~! [arg- τ_arg] (... ...)) (infers+erase #'args)
+;              #:when (stx-andmap (λ (t) (typecheck? t #'#%type)) #'(τ_arg (... ...)))
+              (assign-type #'(τ-internal ty.norm (... ...)) #'#%type)]
+             ;; else fail with err msg
+             [_
+              (type-error #:src stx
+                          #:msg (string-append
+                                 "Improper usage of type constructor ~a: ~a, expected ~a ~a arguments")
+                          #'τ stx #'op #'n)])))]
+    #;[(_ #:cat cat
+        (τ:id (~optional (~and bvs-pat:bound-vars bvs-test) ; bvs-test checks for existence of bound vars
+                         #:defaults ([bvs-pat.stx #'[[]]][(bvs-pat.x 1) null]))
               . pat)
         ; lits must have ~ prefix (for syntax-parse compat) for now
         (~optional (~seq #:lits (lit ...)) #:defaults ([(lit 1) null]))
@@ -175,6 +422,7 @@
      #:with τ-get (format-id #'τ "~a-get" #'τ)
      #:with τ-match+erase (format-id #'τ "infer~a+erase" #'τ)
      #:with τ-expander (format-id #'τ "~~~a" #'τ)
+     #:with τ-expander* (format-id #'τ "~~~a*" #'τ)
      #:with pat-class (generate-temporary #'τ) ; syntax-class name
      #:with tycon (generate-temporary #'τ) ; need a runtime id for expansion
      #:with (lit-tmp ...) (generate-temporaries #'(lit ...))
@@ -185,20 +433,41 @@
          (define lit-tmp void) ...
          (define-syntax lit (syntax-parser [(_ . xs) #'(lit-tmp . xs)])) ...
          (provide lit ...)
-         (provide τ (for-syntax τ-expander))
+         (provide τ (for-syntax τ-expander τ-expander*))
          (begin-for-syntax
-           #'(define-syntax lit
+           #;(define-syntax lit
              (pattern-expander
               (syntax-parser
                 [(_ . xs)
-                 #'((~literal #%plain-app) (~literal lit-tmp) . xs)]))) ...
+                 #'((~literal #%plain-app) (~literal lit-tmp) . xs)]))) ;...
+           ; the ~τ pattern backtracks normally;
+           ; the ~τ* version errors immediately for a non-match
            (define-syntax τ-expander
              (pattern-expander
               (syntax-parser
                 [(_ (~optional
                      (~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
                     . match-pat)
-                 #:with pat-from-constructor (quote-syntax (τ . pat))
+                 ;; manually replace literals with expanded form, to get around ~ restriction
+                 #:with new-match-pat
+                 #`#,(subst-datum-lits
+                      #`((#,(quote-syntax ~seq) (~literal #%plain-app) (~literal lit-tmp)) ...)
+                      #'(lit ...)
+                      #'match-pat)
+                 #'((~literal #%plain-type)
+                    ((~literal #%plain-lambda) (bvs.x (... ...))
+                     ((~literal let-values) () ((~literal let-values) ()
+                      ((~literal #%plain-app) (~literal tycon) . new-match-pat)))))])))
+           (define-syntax τ-expander*
+             (pattern-expander
+              (syntax-parser
+                [(_ (~optional
+                     (~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
+                    . match-pat)
+                 #:with pat-from-constructor
+                        #,(if (attribute bvs-test)
+                              #'(quote-syntax (τ bvs-pat.stx . pat))
+                              #'(quote-syntax (τ . pat)))
                  ;; manually replace literals with expanded form, to get around ~ restriction
                  #:with new-match-pat
                  #`#,(subst-datum-lits
@@ -271,16 +540,20 @@
                                     (current-continuation-marks)))))
          (define-syntax (τ stx)
            (syntax-parse stx #:literals (lit ...)
-             [(_ (~optional (~and bvs:bound-vars bvs-pat.stx)
-                            #:defaults ([(bvs.x 1) null]))
-                 . (~and pat !~ args)) ; first check shape
+             [(_ (~optional (~or (~and bvs:bound-vars bvs-pat.stx)
+                                 (~seq #:bind (~and bvs (bvs-pat.x ...)))))
+                 . (~and pat ~! args)) ; first check shape
+              #:with (tv (... ...)) (cond [(attribute bvs.x) #'(bvs.x (... ...))]
+                                          [(attribute bvs) #'bvs]
+                                          [else null])
               ; this inner syntax-parse gets the ~! to register
               ; otherwise, apparently #:declare's get subst into pat (before ~!)
               (syntax-parse #'args #:literals (lit ...)
                 [pat #,@#'(decls ...) ; then check declarations (eg, valid type)
                  #'(#%type
-                    (λ (bvs.x (... ...))
-                      (let-syntax ([bvs.x (syntax-parser [bvs.x:id #'(#%type bvs.x)])] (... ...))
+                    (λ (tv (... ...)) ;(bvs.x (... ...))
+;                      (let-syntax ([bvs.x (syntax-parser [bvs.x:id #'(#%type bvs.x)])] (... ...))
+                      (let-syntax ([tv (syntax-parser [tv:id #'(#%type tv)])] (... ...))
                         (tycon . args))))])]
              [_
               #:with expected-pat
@@ -299,6 +572,173 @@
                                    ", ")))
                           #'τ stx #'expected-pat)])))]))
 
+; define-type-constructor, archied 2015-08-12
+;(define-syntax define-type-constructor
+;  (syntax-parser
+;    [(_ (τ:id (~optional (~and bvs-pat:bound-vars bvs-test) ; bvs-test checks for existence of bound vars
+;                         #:defaults ([bvs-pat.stx #'[[]]][(bvs-pat.x 1) null]))
+;              . 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) ...)
+;                   #:defaults ([(tvar 1) null][(cls 1) null])))
+;     #:with τ-match (format-id #'τ "~a-match" #'τ)
+;     #:with τ? (format-id #'τ "~a?" #'τ)
+;     #:with τ-get (format-id #'τ "~a-get" #'τ)
+;     #:with τ-match+erase (format-id #'τ "infer~a+erase" #'τ)
+;     #:with τ-expander (format-id #'τ "~~~a" #'τ)
+;     #:with τ-expander* (format-id #'τ "~~~a*" #'τ)
+;     #: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
+;         ;; 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 τ (for-syntax τ-expander τ-expander*))
+;         (begin-for-syntax
+;           #;(define-syntax lit
+;             (pattern-expander
+;              (syntax-parser
+;                [(_ . xs)
+;                 #'((~literal #%plain-app) (~literal lit-tmp) . xs)]))) ;...
+;           ; the ~τ pattern backtracks normally;
+;           ; the ~τ* version errors immediately for a non-match
+;           (define-syntax τ-expander
+;             (pattern-expander
+;              (syntax-parser
+;                [(_ (~optional
+;                     (~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
+;                    . match-pat)
+;                 ;; manually replace literals with expanded form, to get around ~ restriction
+;                 #:with new-match-pat
+;                 #`#,(subst-datum-lits
+;                      #`((#,(quote-syntax ~seq) (~literal #%plain-app) (~literal lit-tmp)) ...)
+;                      #'(lit ...)
+;                      #'match-pat)
+;                 #'((~literal #%plain-type)
+;                    ((~literal #%plain-lambda) (bvs.x (... ...))
+;                     ((~literal let-values) () ((~literal let-values) ()
+;                      ((~literal #%plain-app) (~literal tycon) . new-match-pat)))))])))
+;           (define-syntax τ-expander*
+;             (pattern-expander
+;              (syntax-parser
+;                [(_ (~optional
+;                     (~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
+;                    . match-pat)
+;                 #:with pat-from-constructor
+;                        #,(if (attribute bvs-test)
+;                              #'(quote-syntax (τ bvs-pat.stx . pat))
+;                              #'(quote-syntax (τ . pat)))
+;                 ;; manually replace literals with expanded form, to get around ~ restriction
+;                 #:with new-match-pat
+;                 #`#,(subst-datum-lits
+;                      #`((#,(quote-syntax ~seq) (~literal #%plain-app) (~literal lit-tmp)) ...)
+;                      #'(lit ...)
+;                      #'match-pat)
+;                 #'(~and
+;                    (~or
+;                     ((~literal #%plain-type)
+;                      ((~literal #%plain-lambda) (bvs.x (... ...))
+;                       ((~literal let-values) () ((~literal let-values) ()
+;                        ((~literal #%plain-app) (~literal tycon) . new-match-pat)))))
+;                     (~and any
+;                           (~do
+;                            (type-error #:src #'any
+;                                        #:msg
+;                                        "Expected type of expression to match pattern ~a, got: ~a"
+;                                        (quote-syntax pat-from-constructor) #'any))))
+;                    ~!)])))
+;           (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
+;             ; uses "lit" pattern expander
+;             (pattern pat))
+;           (define (τ-match ty)
+;             (or (match-type ty tycon pat-class)
+;                 ;; error msg should go in specific macro def?
+;                 (type-error #:src ty
+;                      #:msg "Expected type with pattern: ~a, got: ~a"
+;                      (quote-syntax (τ . pat)) ty)))
+;           ; predicate version of τ-match
+;           (define (τ? ty) (match-type ty tycon pat-class))
+;           ;; expression version of τ-match
+;           (define (τ-match+erase e)
+;             (syntax-parse (infer+erase e)
+;               [(e- ty)
+;                #:with τ_matched/#f (match-type #'ty tycon pat-class)
+;                #:fail-unless (syntax-e #'τ_matched/#f)
+;                              (format
+;                               "~a (~a:~a): Expected type of expression ~a to match pattern ~a, got: ~a"
+;                               (syntax-source e) (syntax-line e) (syntax-column e)
+;                               (syntax->datum e) (type->str (quote-syntax (τ . pat))) (type->str #'ty))
+;                #'(e- τ_matched/#f)]))
+;           ;; get syntax bound to specific pat var (as declared in def-tycon)
+;           (define-syntax (τ-get stx)
+;             (syntax-parse stx #:datum-literals (from)
+;               [(_ attr from ty)
+;                #:with args (generate-temporary)
+;                #:with args.attr (format-id #'args "~a.~a" #'args #'attr)
+;                #:with the-pat (quote-syntax (τ . pat))
+;                #'(syntax-parse #'ty ;((current-type-eval) #'ty)
+;                    [typ ;((~literal #%plain-type) ((~literal #%plain-app) f . args))
+;                     #:fail-unless (τ? #'typ)
+;                                   (format "~a (~a:~a) Expected type with pattern: ~a, got: ~a"
+;                                           (syntax-source  #'typ) (syntax-line #'typ) (syntax-column #'typ)
+;                                           (type->str (quote-syntax the-pat)) (type->str #'typ))
+;                     #:with ((~literal #%plain-type)
+;                             ((~literal #%plain-lambda) tvs
+;                              ((~literal let-values) () ((~literal let-values) ()
+;                               ((~literal #%plain-app) f . args)))))
+;                            ((current-type-eval) #'typ)
+;                     #:declare args pat-class ; check shape of arguments
+;;                     #:fail-unless (typecheck? #'f #'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" 'τ)
+;                                    (current-continuation-marks)))))
+;         (define-syntax (τ stx)
+;           (syntax-parse stx #:literals (lit ...)
+;             [(_ (~optional (~or (~and bvs:bound-vars bvs-pat.stx)
+;                                 (~seq #:bind (~and bvs (bvs-pat.x ...)))))
+;                 . (~and pat ~! args)) ; first check shape
+;              #:with (tv (... ...)) (cond [(attribute bvs.x) #'(bvs.x (... ...))]
+;                                          [(attribute bvs) #'bvs]
+;                                          [else null])
+;              ; this inner syntax-parse gets the ~! to register
+;              ; otherwise, apparently #:declare's get subst into pat (before ~!)
+;              (syntax-parse #'args #:literals (lit ...)
+;                [pat #,@#'(decls ...) ; then check declarations (eg, valid type)
+;                 #'(#%type
+;                    (λ (tv (... ...)) ;(bvs.x (... ...))
+;;                      (let-syntax ([bvs.x (syntax-parser [bvs.x:id #'(#%type bvs.x)])] (... ...))
+;                      (let-syntax ([tv (syntax-parser [tv:id #'(#%type tv)])] (... ...))
+;                        (tycon . args))))])]
+;             [_
+;              #:with expected-pat
+;                     #,(if (attribute bvs-test)
+;                           #'(quote-syntax (τ bvs-pat.stx . pat))
+;                           #'(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 #'expected-pat)])))]))
+
+
 ;; TODO: refine this to enable specifying arity information
 ;; type constructors currently must have 1+ arguments
 ;#;(define-syntax (define-type-constructor stx)
@@ -360,18 +800,20 @@
 ;; syntax classes
 (begin-for-syntax
   (define-syntax-class type
-    ;; stx = surface syntax, as written
-    ;; norm = canonical form for the type
+    ;; τ = surface syntax, as written
+    ;; norm = canonical form for the type, ie expanded
+    ;; -dont bother to check if type is already expanded, because this class
+    ;; typically annotates user-written types
     (pattern τ
-     #:fail-unless (is-type? #'τ)
+     #:with [norm k] (infer+erase #'τ)
+     #:fail-unless (#%type? #'k)
                    (format "~a (~a:~a) not a valid type: ~a"
                            (syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ)
-                           (type->str #'τ))
-     #:attr norm (delay ((current-type-eval) #'τ))))
+                           (type->str #'τ))))
 
   (define-syntax-class typed-binding #:datum-literals (:)
-    #:attributes (x τ norm)
-    (pattern [x:id : ~! τ:type] #:attr norm (delay #'τ.norm))
+    #:attributes (x τ)
+    (pattern [x:id : ~! ty:type] #:attr τ #'ty.norm)
     (pattern any
      #:fail-when #t
      (format
@@ -379,7 +821,7 @@
        "Improperly formatted type annotation: ~a; should have shape [x : τ], "
        "where τ is a valid type.")
       (type->str #'any))
-     #:attr x #f #:attr τ #f #:attr norm #f))
+     #:attr x #f #:attr τ #f))
 
   (define (brace? stx)
     (define paren-shape/#f (syntax-property stx 'paren-shape))
@@ -400,127 +842,11 @@
       (type->str #'any))
       #:attr τ #f #:attr norm #f)))
 
-;; type assignment
-(begin-for-syntax
-  ;; macro for nicer syntax
-  (define-syntax (⊢ stx)
-    (syntax-parse stx #:datum-literals (:)
-      [(_ e : τ) #'(assign-type #'e #`τ)]
-      [(_ e τ) #'(⊢ e : τ)]))
-       
-  ;; assign-type Type -> Syntax
-  ;; Attaches type τ to (expanded) expression e.
-  ;; must eval here, to catch unbound types
-  (define (assign-type e τ #:tag [tag 'type])
-    (syntax-property e tag (syntax-local-introduce ((current-type-eval) τ))))
-  
-  ;; typeof : Syntax -> Type or #f
-  ;; Retrieves type of given stx, or #f if input has not been assigned a type.
-  (define (typeof stx #:tag [tag 'type]) (syntax-property stx tag))
-  
-  ;; infers the type and erases types in an expression
-  (define (infer+erase e)
-    (define e+ (expand/df e))
-    (list e+ (typeof e+)))
-  ;; infers the types and erases types in multiple expressions
-  (define (infers+erase es)
-    (stx-map infer+erase es))
 
-  ;; This is the main "infer" function. All others are defined in terms of this.
-  ;; It should be named infer+erase but leaving it for now for backward compat.
-  ;; NOTE: differs slightly from infer/type-ctxt+erase in that types are not
-  ;; expanded before wrapping in lambda
-  ;; - This caused one problem in fomega2.rkt #%app, but I just had to expand
-  ;; the types before typechecking, which is acceptable
-  (define (infer es #:ctx [ctx null] #:tvs [tvs null] #:tag [tag 'type])
-    (syntax-parse ctx #:datum-literals (:)
-      [([x : τ] ...) ; dont expand yet bc τ may have references to tvs
-       #:with (e ...) es
-       #:with (tv ...) tvs
-       #:with
-       ; old expander pattern
-       #;((~literal #%plain-lambda) tvs+
-        ((~literal #%expression)
-         ((~literal #%plain-lambda) xs+
-          ((~literal letrec-syntaxes+values) stxs1 ()
-            ((~literal letrec-syntaxes+values) stxs2 ()
-              ((~literal #%expression) e+) ...)))))
-       ; new expander pattern
-       ((~literal #%plain-lambda) tvs+
-        ((~literal let-values) () ((~literal let-values) ()
-         ((~literal #%expression)
-          ((~literal #%plain-lambda) xs+
-           ((~literal let-values) () ((~literal let-values) ()
-            ((~literal #%expression) e+) ...)))))))
-       (expand/df
-        #`(λ (tv ...)
-            (let-syntax ([tv (syntax-parser [tv:id #'(#%type tv)])] ...)
-              (λ (x ...)
-                (let-syntax ([x (make-rename-transformer (assign-type #'x #'τ #:tag '#,tag))] ...)
-                  (#%expression e) ...)))))
-       (list #'tvs+ #'xs+ #'(e+ ...)
-             (stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
-      [([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvs tvs)]))
-
-  ;; fns derived from infer ---------------------------------------------------
-  ;; some are syntactic shortcuts, some are for backwards compat
-  
-  ;; infers type and erases types in a single expression,
-  ;; in the context of the given bindings and their types
-  (define (infer/type-ctxt+erase x+τs e)
-    (syntax-parse (infer (list e) #:ctx x+τs)
-      [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
-  ;; infers type and erases types in multiple expressions,
-  ;; in the context of (one set of) given bindings and their tpyes
-  (define (infers/type-ctxt+erase ctxt es)
-    (stx-cdr (infer es #:ctx ctxt))) ; drop (empty) tyvars from result
-  ;; infers and erases types in an expression, in the context of given type vars
-  (define (infer/tvs+erase e tvs)
-    (syntax-parse (infer (list e) #:tvs tvs)
-      [(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
-
-  ; type parameters, for type checker aspects that require extension
-  (define current-typecheck-relation (make-parameter #f))
-  (define (typecheck? t1 t2)
-    ((current-typecheck-relation) ((current-type-eval) t1) ((current-type-eval) t2)))
-  (define (typechecks? τs1 τs2)
-    (and (= (stx-length τs1) (stx-length τs2))
-         (stx-andmap typecheck? τs1 τs2)))
-  
-  (define current-type-eval (make-parameter #f))
-  (define (type-evals τs) #`#,(stx-map (current-type-eval) τs))
-
-  ; get rid of this?
-  (define current-promote (make-parameter (λ (x) x)))
-
-  ;; term expansion
-  ;; expand/df : Syntax -> Syntax
-  ;; Local expands the given syntax object. 
-  ;; The result always has a type (ie, a 'type stx-prop).
-  ;; Note: 
-  ;; local-expand must expand all the way down, ie stop-ids == null
-  ;; If stop-ids is #f, then subexpressions won't get expanded and thus won't
-  ;; get assigned a type.
-  (define (expand/df e)
-    (local-expand e 'expression null))
-
-  (struct exn:fail:type:check exn:fail:user ())
-
-  ;; type-error #:src Syntax #:msg String Syntax ...
-  ;; usage:
-  ;; type-error #:src src-stx
-  ;;            #:msg msg-string msg-args ...
-  (define-syntax-rule (type-error #:src stx-src #:msg msg args ...)
-    (raise
-     (exn:fail:type:check
-      (format (string-append "TYPE-ERROR: ~a (~a:~a): " msg) 
-              (syntax-source stx-src) (syntax-line stx-src) (syntax-column stx-src) 
-              (type->str args) ...)
-      (current-continuation-marks)))))
 
 (define-syntax (define-primop stx)
     (syntax-parse stx #:datum-literals (:)
-      [(_ op:id : τ)
+      [(_ op:id : τ:type)
        #:with op/tc (generate-temporary #'op)
        #`(begin
            (provide (rename-out [op/tc op]))
@@ -532,7 +858,6 @@
                 #:with op (format-id stx "~a" #'op)
                 (syntax/loc stx (app op x (... ...)))])))]))
 
-(define-for-syntax (mk-pred x) (format-id x "~a?" x))
 (define-for-syntax (mk-acc base field) (format-id base "~a-~a" base field))
 
 (begin-for-syntax