diff --git a/tapl/exist.rkt b/tapl/exist.rkt
index c7367f8..8ad33df 100644
--- a/tapl/exist.rkt
+++ b/tapl/exist.rkt
@@ -17,63 +17,21 @@
 ;; - terms from stlc+reco+var.rkt
 ;; - pack and open
 
-#;(begin-for-syntax
-  (define (type=? t1 t2)
-    (or (stlc:type=? t1 t2)
-        (sysf:type=? t1 t2)))
-  (current-type=? type=?)
-  (current-typecheck-relation type=?))
 
-
-#;(define-type-constructor (∃ [[X]] τ_body))
-(define-basic-checked-stx ∃ #:arity = 1 #:bvs = 1)
-; 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) τ)
-;        #'((~literal #%plain-lambda) (tv) τ)])))
-;  (define-syntax ~∃*
-;    (pattern-expander
-;     (syntax-parser
-;       [(_ (tv:id) τ)
-;        #'(~or (~∃ (tv) τ)
-;               (~and any (~do
-;                          (type-error
-;                           #:src #'any
-;                           #:msg "Expected ∃ type, got: ~a" #'any))))]))))
+(define-type-constructor ∃ #:arity = 1 #:bvs = 1)
 
 (define-syntax (pack stx)
   (syntax-parse stx
     [(_ (τ:type e) as ∃τ:type)
      #:with (~∃* (τ_abstract) τ_body) #'∃τ.norm
-;     #:with (#%plain-lambda (τ_abstract:id) τ_body) #'∃τ.norm
      #:with [e- τ_e] (infer+erase #'e)
      #:when (typecheck? #'τ_e  (subst #'τ.norm #'τ_abstract #'τ_body))
-     (⊢ e- : ∃τ)]))
+     (⊢ e- : ∃τ.norm)]))
 
 (define-syntax (open stx)
   (syntax-parse stx #:datum-literals (<=)
     [(_ ([(tv:id x:id) <= e_packed]) e)
-;     #:with [e_packed- τ_packed] (infer+erase #'e_packed)
-;     #:when (displayln #'τ_packed)
-;     #:with (~∃ (τ_abstract) τ_body) #'τ_packed
      #:with [e_packed- ((τ_abstract) (τ_body))] (⇑ e_packed as ∃)
-;     #: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.
      ;; It's the (TaPL) type rule itself that is fast and loose.
      ;; Leveraging the macro system's management of binding reveals this.
diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
index bc2df66..3587bdf 100644
--- a/tapl/ext-stlc.rkt
+++ b/tapl/ext-stlc.rkt
@@ -129,10 +129,10 @@
 
 (define-syntax (letrec/tc stx)
   (syntax-parse stx
-    [(_ ([b:typed-binding e] ...) e_body)
+    [(_ ([b:type-bind e] ...) e_body)
      #:with ((x- ...) (e- ... e_body-) (τ ... τ_body))
             (infers/type-ctxt+erase #'(b ...) #'(e ... e_body))
-     #:fail-unless (typechecks? #'(b.τ ...) #'(τ ...))
+     #:fail-unless (typechecks? #'(b.type ...) #'(τ ...))
                    (string-append
                     "type check fail, args have wrong type:\n"
                     (string-join
@@ -141,7 +141,7 @@
                         (format
                          "~a has type ~a, expected ~a"
                          (syntax->datum e) (type->str τ) (type->str τ-expect)))
-                      #'(e ...) #'(τ ...) #'(b.τ ...))
+                      #'(e ...) #'(τ ...) #'(b.type ...))
                      "\n"))
      (⊢ (letrec ([x- e-] ...) e_body-) : τ_body)]))
 
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
index f2bdd24..331b346 100644
--- a/tapl/fomega.rkt
+++ b/tapl/fomega.rkt
@@ -1,17 +1,17 @@
 #lang racket/base
 (require "typecheck.rkt")
-(require (except-in "sysf.rkt" #%app λ Int #%datum → Λ inst ∀  + type-eval)
-         (prefix-in sysf: (only-in "sysf.rkt" type-eval))
-         (only-in "stlc+reco+var.rkt" same-types?))
-(provide (rename-out [app/tc #%app] [λ/tc λ] [datum/tc #%datum]))
+(require (except-in "sysf.rkt" #%app λ #%datum Λ inst ∀ type-eval type=?)
+         (rename-in (prefix-in sysf: (only-in "sysf.rkt" #%app λ type-eval ∀ ~∀ type=?))
+                    [sysf:~∀ ~sysf:∀])
+         (only-in "stlc+reco+var.rkt" String #%datum same-types?))
+(provide (rename-out [sysf:#%app #%app] [sysf:λ λ] #;[app/tc #%app] #;[λ/tc λ] #;[datum/tc #%datum]))
 #;(provide (except-out (all-from-out "sysf.rkt")
-                     sysf:Int sysf:→ sysf:∀
-                     sysf:#%app sysf:λ
-                     (for-syntax sysf:type-eval)))
-(provide (except-out (all-from-out "sysf.rkt") (for-syntax sysf:type-eval))
+                     sysf:∀ sysf:#%app sysf:λ
+                     (for-syntax sysf:type-eval sysf:type=?)))
+(provide (except-out (all-from-out "sysf.rkt") (for-syntax sysf:type-eval sysf:type=?))
          (all-from-out "stlc+reco+var.rkt"))
-(provide Int → ∀ inst Λ tyλ tyapp
-         (for-syntax type-eval))
+(provide ∀ inst Λ tyλ tyapp
+         (for-syntax type-eval type=?))
 
 ;; System F_omega
 ;; Type relation:
@@ -21,9 +21,11 @@
 ;; - terms from sysf.rkt
 
 (define-syntax-category kind)
+(begin-for-syntax
+  (current-type? (λ (t) (or (type? t) (kind? (typeof t))))))
 
-(provide define-type-alias)
-(define-syntax define-type-alias
+#;(provide define-type-alias)
+#;(define-syntax define-type-alias
   (syntax-parser
     [(_ alias:id τ)
      #:with (τ- k_τ) (infer+erase #'τ)
@@ -31,6 +33,18 @@
      #'(define-syntax alias (syntax-parser [x:id #'τ-]))]))
 
 (begin-for-syntax
+  (define (type=? t1 t2)
+    (printf "t1 = ~a\n" (syntax->datum t1))
+    (printf "t2 = ~a\n" (syntax->datum t2))
+    (and (syntax-parse (list t1 t2) #:datum-literals (:)
+          [((~∀ ([tv1 : k1] ...) tbody1)
+            (~∀ ([tv2 : k2] ...) tbody2))
+           #:when (displayln "here")
+           (types=? #'(k1 ...) #'(k2 ...))]
+           [_ #t])
+         (sysf:type=? t1 t2)))
+  (current-type=? type=?)
+  (current-typecheck-relation (current-type=?))
   ;; extend type-eval to handle tyapp
   ;; - requires manually handling all other forms
   (define (type-eval τ)
@@ -52,13 +66,12 @@
       [((~literal #%plain-app) arg ...)
        #:with (arg+ ...) (stx-map (current-type-eval) #'(arg ...))
        (syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
-      [(~or x:id ((~literal tyλ) . _)) ; dont eval under tyλ
+      [_ #;(~or x:id ((~literal tyλ) . _)) ; dont eval under tyλ
        (sysf:type-eval τ)]))
   (current-type-eval type-eval))
 
-(define-basic-checked-id-stx ★ : #%kind)
-(define-basic-checked-stx ⇒ : #%kind #:arity >= 1)
-;(define-type-constructor (⇒ k_in ... k_out))
+(define-base-kind ★)
+(define-kind-constructor ⇒ #:arity >= 1)
 
 ;; for now, handle kind checking in the types themselves
 ;; TODO: move kind checking to a common place (like #%app)?
@@ -66,15 +79,15 @@
 
 ;; TODO: need some kind of "promote" abstraction,
 ;; so I dont have to manually add kinds to all types
-(define-basic-checked-id-stx String : ★)
-(define-basic-checked-id-stx Int : ★)
+#;(define-basic-checked-id-stx String : ★)
+#;(define-basic-checked-id-stx Int : ★)
 ;(define-base-type Str)
 ;(provide String)
 ;(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-basic-checked-stx → : ★ #:arity >= 1)
+#;(define-basic-checked-stx → : ★ #:arity >= 1)
 #;(define-syntax (→ stx)
   (syntax-parse stx
     [(_ τ ... τ_res)
@@ -83,19 +96,57 @@
      #:when (same-types? #'(k ... k_res))
      (⊢ (sysf:→ (#%plain-type τ-) ... (#%plain-type τ_res-)) : ★)]))
 
-(define-syntax (∀ stx)
+#;(define-syntax (∀ stx)
   (syntax-parse stx
     [(_ (b:kinded-binding ...) τ_body)
      #:with (tvs- τ_body- k_body) (infer/ctx+erase #'(b ...) #'τ_body)
      #:when (★? #'k_body)
      (⊢ (λ tvs- b.tag ... τ_body-) : ★)]))
+(define-syntax (∀ stx)
+  (syntax-parse stx
+    [(_ bvs:kind-ctx τ_body)
+;     #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body)
+;     #:when (★? #'k_body)
+     #:when (displayln ((current-type-eval) #'(sysf:∀ (bvs.x ...) τ_body)))
+     (⊢ #,((current-type-eval) #'(sysf:∀ (bvs.x ...) τ_body)) : (⇒ bvs.kind ...))]))
+;    (⊢ (λ tvs- b.tag ... τ_body-) : ★)]))
+(begin-for-syntax
+  (define-syntax ~∀
+    (pattern-expander
+     (syntax-parser #:datum-literals (:)
+       [(_ ([tv:id : k] ...) τ)
+        #:when (displayln "pat expand")
+        #:with ∀τ (generate-temporary)
+        #'(~and ∀τ
+                (~parse (~sysf:∀ (tv ...) τ) #'∀τ)
+                (~parse (~⇒ k ...) (typeof #'∀τ)))]
+       [(_ . args)
+        #'(~and ∀τ
+                (~parse (~sysf:∀ (tv (... ...)) τ) #'∀τ)
+                (~parse (~⇒ k (... ...)) (typeof #'∀τ))
+                (~parse args #'(([tv k] (... ...)) τ)))])))
+  (define-syntax ~∀*
+    (pattern-expander
+     (syntax-parser #:datum-literals (<:)
+       [(_ . args)
+        #'(~or
+           (~∀ . args)
+           (~and any (~do
+                      (type-error
+                       #:src #'any
+                       #:msg "Expected ∀ type, got: ~a" #'any))))]))))
 
-(define-syntax (Λ stx)
+#;(define-syntax (Λ stx)
   (syntax-parse stx
     [(_ (b:kinded-binding ...) e)
      #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'(b ...) #'e)
      (⊢ e- : (∀ ([tv- : b.tag] ...) τ_e))]))
-(define-syntax (inst stx)
+(define-syntax (Λ stx)
+  (syntax-parse stx
+    [(_ bvs:kind-ctx e)
+     #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e)
+     (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))]))
+#;(define-syntax (inst stx)
   (syntax-parse stx
     [(_ e τ ...)
      #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
@@ -109,15 +160,47 @@
      #:with ((~literal #%plain-lambda) (tv ...) k_tv ... τ_body) #'∀τ
      #:when (typechecks? #'(k_τ ...) #'(k_tv ...))
      (⊢ e- : #,(substs #'(τ ...) #'(tv ...) #'τ_body))]))
+(define-syntax (inst stx)
+  (syntax-parse stx
+    [(_ e τ:type ...)
+     #:with (e- (([tv k] ...) τ_body)) (⇑ e as ∀)
+     #:with ([τ- k_τ] ...) (infers+erase #'(τ ...) #:expand (current-type-eval))
+     #:when (typechecks? (stx-map typeof #'(k_τ ...)) #'(k ...))
+     (⊢ e- : #,(substs #'(τ- ...) #'(tv ...) #'τ_body))]))
 
 ;; TODO: merge with regular λ and app?
 (define-syntax (tyλ stx)
+  (syntax-parse stx 
+    [(_ bvs:kind-ctx τ_body)
+     #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
+     (⊢ (λ tvs- τ_body-) : (⇒ bvs.kind ... k_body))]))
+#;(define-syntax (tyλ stx)
   (syntax-parse stx 
     [(_ (b:kinded-binding ...) τ_body)
      #:with (tvs- τ_body- k_body) (infer/ctx+erase #'(b ...) #'τ_body)
      (⊢ (λ tvs- τ_body-) : (⇒ b.tag ... k_body))]))
 
 (define-syntax (tyapp stx)
+  (syntax-parse stx
+    [(_ τ_fn τ_arg ...)
+     #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
+     #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...) #:expand (current-type-eval))
+     #:fail-unless (typechecks? #'(k_arg ...) #'(k_in ...))
+                   (string-append
+                    (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 (λ (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 type(s): "
+                            (stx-length #'(k_in ...)))
+                    (string-join (stx-map type->str #'(k_in ...)) ", "))
+     (⊢ (#%app τ_fn- τ_arg- ...) : k_out)]))
+#;(define-syntax (tyapp stx)
   (syntax-parse stx
     [(_ τ_fn τ_arg ...)
      #:with [τ_fn- (~⇒* k_in ... k_out)] (infer+erase #'τ_fn)
@@ -176,9 +259,9 @@
 ;; must override #%app and λ and primops to use new →
 ;; TODO: parameterize →?
 
-(define-primop + : (→ Int Int Int) : ★)
+#;(define-primop + : (→ Int Int Int) : ★)
 
-(define-syntax (λ/tc stx)
+#;(define-syntax (λ/tc stx)
   (syntax-parse stx #:datum-literals (:)
     [(_ ([x : τ] ...) e)
      ;#:when (andmap ★? (stx-map (λ (t) (typeof (expand/df t))) #'(τ ...)))
@@ -187,7 +270,7 @@
      #:with (xs- e- τ_res) (infer/type-ctxt+erase #'([x : τ] ...) #'e)
      (⊢ (λ xs- e-) : (→ τ ... τ_res))]))
 
-(define-syntax (app/tc stx)
+#;(define-syntax (app/tc stx)
   (syntax-parse stx
     [(_ e_fn e_arg ...)
      #:with [e_fn- (~→* τ_in ... τ_out)] (infer+erase #'e_fn)
@@ -244,7 +327,7 @@
 ;     (⊢ (#%app e_fn- e_arg- ...) : τ_res)]))
 
 ;; must override #%datum to use new kinded-Int, etc
-(define-syntax (datum/tc stx)
+#;(define-syntax (datum/tc stx)
   (syntax-parse stx
     [(_ . n:integer) (⊢ (#%datum . n) : Int)]
     [(_ . s:str) (⊢ (#%datum . s) : String)]
diff --git a/tapl/fsub.rkt b/tapl/fsub.rkt
index b6b8d62..c6aea3c 100644
--- a/tapl/fsub.rkt
+++ b/tapl/fsub.rkt
@@ -1,17 +1,15 @@
 #lang racket/base
 (require "typecheck.rkt")
-(require ;(except-in "sysf.rkt" #%app λ + #%datum ∀ Λ inst type=?)
-         ;(prefix-in sysf: (only-in "sysf.rkt" #%app λ))
-         (except-in "stlc+reco+sub.rkt" #%app λ + type=? #;sub?)
-         (prefix-in stlc: (only-in "stlc+reco+sub.rkt" #%app λ #;type=? sub?))
-         (only-in "stlc+rec-iso.rkt" type=?)) ; type=? for binding forms
+(require (except-in "stlc+reco+sub.rkt" #%app λ + type=?)
+         (prefix-in stlc: (only-in "stlc+reco+sub.rkt" #%app λ sub?))
+         (only-in "sysf.rkt" ∀? type=?)
+         (prefix-in sysf: (only-in "sysf.rkt" ∀ #;type=?))
+         (rename-in (only-in "sysf.rkt" ~∀) [~∀ ~sysf:∀]))
 (provide (rename-out [stlc:#%app #%app] [stlc:λ λ]) (for-syntax sub?))
 (provide (except-out (all-from-out "stlc+reco+sub.rkt")
                      stlc:#%app stlc:λ (for-syntax stlc:sub?))
-         (all-from-out "stlc+rec-iso.rkt")
-         #;(except-out (all-from-out "stlc+reco+sub.rkt")
-                     (for-syntax #;stlc+reco+sub:type=? stlc+reco+sub:sub?)))
-(provide ∀ Λ inst)
+         (except-out (all-from-out "sysf.rkt") sysf:∀ (for-syntax #;sysf:type=? ~sysf:∀)))
+(provide ∀ Λ inst (for-syntax #;type=?))
  
 ;; System F<:
 ;; Types:
@@ -33,67 +31,54 @@
            (if sub (expose sub) t)]
           [else t]))
   (current-promote expose)
+  #;(define (type=? t1 t2)
+    (displayln (typeof t1))
+    (displayln (typeof t2))
+    (and (sysf:type=? t1 t2)
+         (sysf:type=? (typeof t1) (typeof t2))))
+  #;(current-type=? type=?)
   ; need this, to lift base-types; is there another way to do this?
   (define (sub? t1 t2)
-    (stlc:sub? (expose t1) (expose t2)))
+    (stlc:sub? ((current-promote) t1) t2))
   (current-sub? sub?)
-  ;; extend to handle new ∀
-  #;(define (type=? τ1 τ2)
-    (syntax-parse (list τ1 τ2)
-      [(((~literal #%plain-lambda) (x:id ...) k1 ... t1)
-        ((~literal #%plain-lambda) (y:id ...) k2 ... t2))
-       #:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
-       #:when (= (stx-length #'(x ...)) (stx-length #'(k1 ...)))
-       ((current-type=?) (substs #'(k1 ...) #'(x ...) #'t1)
-                         (substs #'(k2 ...) #'(y ...) #'t2))]
-      [_ (or (sysf:type=? τ1 τ2) (stlc+reco+sub:type=? τ1 τ2))]))
-  #;(current-type=? type=?)
   (current-typecheck-relation (current-sub?)))
 
+(define-type-constructor <: #:arity >= 0) ; quasi-kind, but must be type constructor because its arguments are types
+(begin-for-syntax
+  (current-type? (λ (t) (or (type? t) (<:? (typeof t))))))
+
 ;; Type annotations used in two places:
 ;; 1) typechecking the body of 
 ;; 2) instantiation of ∀
 ;; Problem: need type annotations, even in expanded form
-#;(define-syntax (∀ stx)
-  (syntax-parse stx #:datum-literals (<:)
-    [(_ ([X:id <: τ] ...) ~! body)
-     (syntax/loc stx (#%plain-lambda (X ...) τ ... body))]
-    #;[(_ x ...) #'(sysf:∀ x ...)]))
-(define ∀-internal void)
+;(define ∀-internal void)
 (define-syntax ∀
   (syntax-parser #:datum-literals (<:)
     [(_ ([tv:id <: τ:type] ...) τ_body)
-     #:with ((tv- ...) τ_body- k) (infer/ctx+erase #'([tv : #%type] ...) #'τ_body)
-     #:when (#%type? #'k)
-     (mk-type #'(λ (tv- ...) (∀-internal τ.norm ... τ_body-)))]))
+     ;#:with ((tv- ...) τ_body- k) (infer/ctx+erase #'([tv : #%type] ...) #'τ_body)
+     ;#:when (#%type? #'k)
+     ;(mk-type #'(λ (tv- ...) (∀-internal τ.norm ... τ_body-)))]))
+     ; eval first to overwrite the old #%type
+     (⊢ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body)) : (<: τ.norm ...))]))
 (begin-for-syntax
-  #;(define (infer∀+erase e)
-    (syntax-parse (infer+erase e) #:context e
-      [(e- τ_e)
-       #:with ((~literal #%plain-lambda) (tv ...) τ_sub ... τ_body) #'τ_e
-       #'(e- (([tv τ_sub] ...) τ_body))]))
-  (define (∀? t)
-    (syntax-parse t
-      [((~literal #%plain-lambda) tvs ((~literal #%plain-app) (~literal ∀-internal) . args))
-       #t]
-      [_ #f]))
   (define-syntax ~∀
     (pattern-expander
      (syntax-parser #:datum-literals (<:)
        [(_ ([tv:id <: τ_sub] ...) τ)
-        #'((~literal #%plain-lambda) (tv ...)
-           ((~literal #%plain-app) (~literal ∀-internal) τ_sub ... τ))]
+        #'(~and ∀τ
+                (~parse (~sysf:∀ (tv ...) τ) #'∀τ)
+                (~parse (~<: τ_sub ...) (typeof #'∀τ)))]
        [(_ . args)
-        #'(~and ((~literal #%plain-lambda) (tv (... ...))
-                 ((~literal #%plain-app) (~literal ∀-internal) τ_sub (... ...) τ))
+        #'(~and ∀τ
+                (~parse (~sysf:∀ (tv (... ...)) τ) #'∀τ)
+                (~parse (~<: τ_sub (... ...)) (typeof #'∀τ))
                 (~parse args #'(([tv τ_sub] (... ...)) τ)))])))
   (define-syntax ~∀*
     (pattern-expander
      (syntax-parser #:datum-literals (<:)
-       [(_ . args) ; (_ ([tv:id <: τ_sub] ...) τ)
+       [(_ . args)
         #'(~or
            (~∀ . args)
-           ;((~literal #%plain-lambda) (tv ...) τ_sub ... τ)
            (~and any (~do
                       (type-error
                        #:src #'any
@@ -106,21 +91,13 @@
      ;; "environment", ie, a syntax property with another tag: 'sub
      ;; The "expose" function looks for this tag to enforce the bound,
      ;; as in TaPL (fig 28-1)
-     #:with ((tv- ...) _ (e-) (τ)) (infer #'(e) #:tvctx #'([tv : #%type] ...)
-                                                #:octx #'([tv : τsub] ...) #:tag 'sub)
-     (⊢ e- : (∀ ([tv- <: τsub] ...) τ))]
-    #;[(_ x ...) #'(sysf:Λ x ...)]))
+     #:with ((tv- ...) _ (e-) (τ_e)) (infer #'(e) #:tvctx #'([tv : #%type] ...)
+                                                  #:octx  #'([tv : τsub] ...) #:tag 'sub)
+     (⊢ e- : (∀ ([tv- <: τsub] ...) τ_e))]))
 (define-syntax (inst stx)
   (syntax-parse stx
     [(_ e τ:type ...)
-     ;#:with (e- (([tv τ_sub] ...) τ_body)) (infer∀+erase #'e)
      #:with (e- (([tv τ_sub] ...) τ_body)) (⇑ e as ∀)
-;     #:with (e- ∀τ) (infer+erase #'e)
-;     #:with ((~literal #%plain-lambda) (tv:id ...) τ_sub ... τ_body) #'∀τ
      #:when (typechecks? #'(τ.norm ...) #'(τ_sub ...))
-     (⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]
-    #;[(_ e τ:type ...) ; need to ensure no types (ie bounds) in lam (ie expanded ∀) body
-     #:with (e- ∀τ) (infer+erase #'e)
-     #:with ((~literal #%plain-lambda) (tv:id ...) τ_body) #'∀τ
-     #'(sysf:inst e τ ...)]))
+     (⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
 
diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt
index 4eda06a..a84512d 100644
--- a/tapl/stlc+box.rkt
+++ b/tapl/stlc+box.rkt
@@ -13,8 +13,7 @@
 ;; Terms:
 ;; - terms from stlc+cons.rkt
 
-;(define-type-constructor (Ref τ) #:declare τ type)
-(define-basic-checked-stx Ref #:arity = 1)
+(define-type-constructor Ref #:arity = 1)
 
 (define-syntax (ref stx)
   (syntax-parse stx
@@ -24,16 +23,12 @@
 (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- (τ)) (⇑ e as Ref)
      (⊢ (unbox e-) : τ)]))
 (define-syntax (:= stx)
   (syntax-parse stx
     [(_ e_ref e)
-;     #:with (e_ref- (τ1)) (inferRef+erase #'e_ref)
      #:with (e_ref- (τ1)) (⇑ e_ref as 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 257374b..39458c3 100644
--- a/tapl/stlc+cons.rkt
+++ b/tapl/stlc+cons.rkt
@@ -15,13 +15,12 @@
 
 ;; TODO: enable HO use of list primitives
 
-;(define-type-constructor (List τ) #:declare τ type)
-(define-basic-checked-stx List #:arity = 1)
+(define-type-constructor List #:arity = 1)
 
 (define-syntax (nil stx)
   (syntax-parse stx
-    [(_ ~! τi:ann)
-     (⊢ null : (List τi.τ))]
+    [(_ ~! τi:type-ann)
+     (⊢ null : (List τi.norm))]
     [null:id
      #:fail-when #t (error 'nil "requires type annotation")
      #'null]))
@@ -29,27 +28,18 @@
   (syntax-parse stx
     [(_ e1 e2)
      #:with (e1- τ1) (infer+erase #'e1)
-;     #:with (e2- (τ2)) (inferList+erase #'e2)
      #:with (e2- (τ2)) (⇑ e2 as List)
-;     #:with (e2- τ-lst) (infer+erase #'e2)
-;     #:with τ2 (List-get τ from τ-lst)
      #:when (typecheck? #'τ1 #'τ2)
      (⊢ (cons e1- e2-) : (List τ1))]))
 (define-syntax (isnil stx)
   (syntax-parse stx
     [(_ e)
-;     #:with (e- _) (inferList+erase #'e)
      #:with (e- _) (⇑ e as List)
-;     #:with (e- τ-lst) (infer+erase #'e)
-;     #:fail-unless (List? #'τ-lst) "expected argument of List type"
      (⊢ (null? e-) : Bool)]))
 (define-syntax (head stx)
   (syntax-parse stx
     [(_ e)
-;     #:with (e- (τ)) (inferList+erase #'e)
      #:with (e- (τ)) (⇑ e as List)
-;     #:with (e- τ-lst) (infer+erase #'e)
-;     #:with τ (List-get τ from τ-lst)
      (⊢ (car e-) : τ)]))
 (define-syntax (tail stx)
   (syntax-parse stx
diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt
index 4eab5bc..06696ec 100644
--- a/tapl/stlc+lit.rkt
+++ b/tapl/stlc+lit.rkt
@@ -1,9 +1,10 @@
 #lang racket/base
 (require "typecheck.rkt")
-(extends "stlc.rkt" #:impl-uses (→))
-;(require "stlc.rkt")
-;(provide (all-from-out "stlc.rkt"))
-(provide (rename-out [datum/tc #%datum]))
+;(extends "stlc.rkt" #:impl-uses (→))
+(require (except-in "stlc.rkt" #%app)
+         (prefix-in stlc: (only-in "stlc.rkt" #%app)))
+(provide (except-out (all-from-out "stlc.rkt") stlc:#%app))
+(provide (rename-out [stlc:#%app #%app] [datum/tc #%datum]) define-primop)
  
 ;; Simply-Typed Lambda Calculus, plus numeric literals and primitives
 ;; Types:
@@ -16,7 +17,19 @@
 
 (define-base-type Int)
 
-;(define-base-type Int)
+(define-syntax define-primop
+  (syntax-parser #:datum-literals (:)
+    [(_ op:id : τ:type)
+     #:with op/tc (generate-temporary #'op)
+     #'(begin
+         (provide (rename-out [op/tc op]))
+         (define-syntax (op/tc stx)
+           (syntax-parse stx
+             [f:id (⊢ #,(syntax/loc stx op) : τ)] ; HO case
+             [(o . rst)
+              #:with app (datum->syntax #'o '#%app)
+              #:with opp (format-id #'o "~a" #'op)
+              (syntax/loc stx (app opp . rst))])))]))
 
 (define-primop + : (→ Int Int Int))
 
diff --git a/tapl/stlc+rec-iso.rkt b/tapl/stlc+rec-iso.rkt
index 4b0d70c..dbff83d 100644
--- a/tapl/stlc+rec-iso.rkt
+++ b/tapl/stlc+rec-iso.rkt
@@ -17,29 +17,10 @@
 ;; - terms from stlc+reco+var.rkt
 ;; - fld/unfld
 
-(define-basic-checked-stx μ #:arity = 1 #:bvs = 1)
-#;(define-type-constructor
-  (μ [[tv]] τ_body))
-#;(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-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-type-constructor μ #:arity = 1 #:bvs = 1)
 
 (begin-for-syntax
-  ;; extend to handle μ
+  ;; extend to handle μ, ie lambdas
   (define (type=? τ1 τ2)
 ;    (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
 ;    (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2))
@@ -56,17 +37,15 @@
 
 (define-syntax (unfld stx)
   (syntax-parse stx
-    [(_ τ:ann e)
+    [(_ τ:type-ann e)
      #:with (~μ* (tv) τ_body) #'τ.norm
-;     #:with ((~literal #%plain-lambda) (tv:id) τ_body) #'τ.norm
      #:with [e- τ_e] (infer+erase #'e)
      #:when (typecheck? #'τ_e #'τ.norm)
      (⊢ e- : #,(subst #'τ.norm #'tv #'τ_body))]))
 (define-syntax (fld stx)
   (syntax-parse stx
-    [(_ τ:ann e)
+    [(_ τ:type-ann e)
      #: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))
-     (⊢ e- : τ.τ)]))
\ No newline at end of file
+     (⊢ e- : τ.norm)]))
\ No newline at end of file
diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt
index 15515c9..0231bb4 100644
--- a/tapl/stlc+reco+var.rkt
+++ b/tapl/stlc+reco+var.rkt
@@ -29,18 +29,6 @@
 ;; - define (values only)
 
 (begin-for-syntax
-  ; extend to:
-  ; 1) accept strings (ie, record labels)
-  #;(define (type=? τ1 τ2)
-;    (printf "t1 = ~a\n" (syntax->datum τ1))
-;    (printf "t2 = ~a\n" (syntax->datum τ2))
-    (syntax-parse (list τ1 τ2)
-      [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
-      [_ (stlc:type=? τ1 τ2)]))
-
-  ;(current-type=? type=?)
-  ;(current-typecheck-relation (current-type=?))
-
   (define (same-types? τs)
     (define τs-lst (syntax->list τs))
     (or (null? τs-lst)
@@ -51,23 +39,16 @@
   (syntax-parser
     [(_ alias:id τ:type)
      ; must eval, otherwise undefined types will be allowed
-     ;#'(define-syntax alias (syntax-parser [x:id #'τ.norm]))]))
      #'(define-syntax alias (syntax-parser [x:id #'τ.norm]))]))
 
-;(define-type-constructor [: str τ] #:lits (:))
-
 ; re-define tuples as records
+; dont use define-type-constructor because I want the : literal syntax
 (define-syntax ×
   (syntax-parser #:datum-literals (:)
     [(_ [label:id : τ:type] ...)
      #:with (valid-τ ...) (stx-map mk-type #'(('label τ.norm) ...))
      #`(stlc:× valid-τ ...)]))
 (begin-for-syntax
-  #;(define (infer×+erase e)
-    (syntax-parse (stlc:infer×+erase e) #:context e
-      [(e- τ_e)
-       #:with (((~literal #%plain-app) (quote l) τ) ...) #'τ_e
-       #'(e- ((l τ) ...))]))
   (define-syntax ~×
     (pattern-expander
      (syntax-parser #:datum-literals (:)
@@ -86,38 +67,20 @@
                                #:src #'any
                                #:msg "Expected × type, got: ~a" #'any))))]))))
 
-#;(define-type-constructor
-  ;(× [~× label τ_fld] ...) #:lits (~×)
-  (× [: label τ_fld] ...) #:lits (:)
-  #:declare label str
-  #:declare τ_fld type
-  )
-;  (× τ ...)
-;  #:declare τ type)
-
 ;; records
 (define-syntax (tup stx)
   (syntax-parse stx #:datum-literals (=)
     [(_ [l:id = e] ...)
      #:with ([e- τ] ...) (infers+erase #'(e ...))
-     ;(⊢ (list (list l e-) ...) : (× [~× l τ] ...))]
-     (⊢ (list (list 'l e-) ...) : (× [l : τ] ...))]
-    #;[(_ e ...)
-     #'(stlc:tup e ...)]))
+     (⊢ (list (list 'l e-) ...) : (× [l : τ] ...))]))
 (define-syntax (proj stx)
   (syntax-parse stx #:literals (quote)
     [(_ e_rec l:id)
-;     #:with (e_rec- (~×* [: 'l_τ τ] ...)) (infer+erase #'e_rec)
-;     #:with (e_rec- ([l_τ τ] ...)) (infer×+erase #'e_rec)
      #:with (e_rec- ([l_τ τ] ...)) (⇑ e_rec as ×)
-;     #:with [rec- τ_rec] (infer+erase #'e_rec) ; match method #2: get
-;     #:with ('l_τ:str ...) (×-get label from τ_rec)
-;     #:with (τ ...) (×-get τ_fld from τ_rec)
      #:with (_ τ_match) (stx-assoc #'l #'([l_τ τ] ...))
-     (⊢ (cadr (assoc 'l e_rec-)) : τ_match)]
-    #;[(_ e ...) #'(stlc:proj e ...)]))
+     (⊢ (cadr (assoc 'l e_rec-)) : τ_match)]))
 
-(define-basic-checked-stx ∨/internal)
+(define-type-constructor ∨/internal)
 
 ; re-define tuples as records
 (define-syntax ∨
@@ -132,16 +95,6 @@
                         "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 ∨? ∨/internal?)
   (define-syntax ~∨
     (pattern-expander
@@ -161,22 +114,10 @@
                                     #:msg "Expected ∨ type, got: ~a" #'any))))
                ~!)])))) ; dont backtrack here
 
-#;(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))
-;     #:when (displayln #'τ)
-;     #:when (displayln #'τ.norm)
-;     #:when (displayln (type->str #'τ.norm))
      #:with (~∨* [l_τ : τ_l] ...) #'τ.norm
-;     #:with ('l_τ:str ...) (∨-get label from τ)
-;     #:with (τ_l ...) (∨-get τ_var from τ)
      #:with match_res (stx-assoc #'l #'((l_τ τ_l) ...))
      #:fail-unless (syntax-e #'match_res)
                    (format "~a field does not exist" (syntax->datum #'l))
@@ -188,11 +129,7 @@
   (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 (e- ([l_x τ_x] ...)) (⇑ e as ∨)
-;     #: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) ...)
@@ -202,34 +139,6 @@
           (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_τ: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)
-  (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 ('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 [(string=? l_e l) (let ([x- (cadr e-)]) e_l-)] ...))
-        : #,(stx-car #'(τ_el ...)))]))
-
 (define-syntax (define/tc stx)
   (syntax-parse stx
     [(_ x:id e)
diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt
index 3b044b3..f6a5df0 100644
--- a/tapl/stlc+tup.rkt
+++ b/tapl/stlc+tup.rkt
@@ -14,7 +14,8 @@
 ;; - terms from ext-stlc.rkt
 ;; - tup and proj
 
-(define-basic-checked-stx ×)
+(define-type-constructor ×)
+;(define-basic-checked-stx ×)
 ;(define-type-constructor (× τ ...) #:declare τ type)
 
 (define-syntax (tup stx)
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
index 46cd56b..50eb913 100644
--- a/tapl/stlc.rkt
+++ b/tapl/stlc.rkt
@@ -1,11 +1,11 @@
 #lang racket/base
 (require "typecheck.rkt")
 (provide (rename-out [λ/tc λ] [app/tc #%app]))
-(provide (for-syntax type=? current-type=? type-eval))
+(provide (for-syntax type=? types=? current-type=? type-eval))
 (provide #%module-begin #%top-interaction #%top require) ; from racket
  
 ;; Simply-Typed Lambda Calculus
-;; - no base type so cannot write any terms
+;; - no base type, so cannot write any terms
 ;; Types: multi-arg → (1+)
 ;; Terms:
 ;; - var
@@ -14,12 +14,11 @@
 
 (begin-for-syntax
   ;; type eval
-  ;; - for now, type-eval = full expansion = canonical type representation
+  ;; - type-eval = =full expansion == canonical type representation
   ;; - must expand because:
   ;;   - checks for unbound identifiers (ie, undefined types)
   ;;   - later, expanding enables reuse of same mechanisms for kind checking
-  ;;   - may require some caution when mixing expanded and unexpanded types to
-  ;;     create other types
+  ;;     and type application
   (define (type-eval τ)
     (or #;(expanded-type? τ) ; don't expand if already expanded
         (add-orig (expand/df τ) τ)))
@@ -29,9 +28,7 @@
   ;; type=? : Type Type -> Boolean
   ;; Indicates whether two types are equal
   ;; type equality == structurally free-identifier=?
-  ;; does not assume any sort of representation (eg expanded/unexpanded)
-  ;; - caller (see typechecks? in typecheck.rkt) is responsible to
-  ;;   convert if necessary
+  ;; assumes canonical (ie expanded) representation
   (define (type=? τ1 τ2)
 ;    (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
 ;    (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2))
@@ -47,19 +44,16 @@
   (define current-type=? (make-parameter type=?))
   (current-typecheck-relation type=?))
 
-;(define-syntax-category type)
+(define-syntax-category type)
 
-(define-basic-checked-stx → #:arity >= 1)
-
-#;(define-type-constructor (→ τ_in ... τ_out)
-  #:declare τ_in type
-  #:declare τ_out type)
+;(define-basic-checked-stx → : #%type #:arity >= 1)
+(define-type-constructor → #:arity >= 1)
 
 (define-syntax (λ/tc stx)
   (syntax-parse stx 
-    [(_ (b:typed-binding ...) e)
-     #:with (xs- e- τ_res) (infer/type-ctxt+erase #'(b ...) #'e)
-     (⊢ (λ xs- e-) : (→ b.τ ... τ_res))]))
+    [(_ bvs:type-ctx e)
+     #:with (xs- e- τ_res) (infer/ctx+erase #'bvs #'e)
+     (⊢ (λ xs- e-) : (→ bvs.type ... τ_res))]))
 
 (define-syntax (app/tc stx)
   (syntax-parse stx
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
index 7b35095..7a6b1b6 100644
--- a/tapl/stx-utils.rkt
+++ b/tapl/stx-utils.rkt
@@ -3,6 +3,7 @@
 (provide (all-defined-out))
 
 (define (stx-cadr stx) (stx-car (stx-cdr stx)))
+(define (stx-caddr stx) (stx-cadr (stx-cdr stx)))
 
 (define (stx-andmap f . stx-lsts)
   (apply andmap f (map syntax->list stx-lsts)))
diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt
index 1d1697b..16f9db6 100644
--- a/tapl/sysf.rkt
+++ b/tapl/sysf.rkt
@@ -19,53 +19,7 @@
 ;; - terms from stlc+lit.rkt
 ;; - Λ and inst
 
-;; dont use define-type-constructor, instead define explicit macro
-;(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))
-
-(define-basic-checked-stx ∀ #:arity = 1 #:bvs >= 0)
-;(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))))]))))
-
-
-#;(begin-for-syntax
-  ;; extend to handle ∀
-  #;(define (type=? τ1 τ2)
-    (syntax-parse (list τ1 τ2)
-      [(((~literal #%plain-lambda) (x:id ...) k1 ... t1)
-        ((~literal #%plain-lambda) (y:id ...) k2 ... t2))
-       #:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
-       #:with (z ...) (generate-temporaries #'(x ...))
-       ((current-type=?) (substs #'(z ...) #'(x ...) #'t1)
-                         (substs #'(z ...) #'(y ...) #'t2))]
-      [_ (stlc:type=? τ1 τ2)]))
-  (current-type=? type=?)
-  (current-typecheck-relation type=?))
+(define-type-constructor ∀ #:arity = 1 #:bvs >= 0)
 
 (define-syntax (Λ stx)
   (syntax-parse stx
@@ -75,7 +29,5 @@
 (define-syntax (inst stx)
   (syntax-parse stx
     [(_ e τ:type ...)
-     #: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
+     #:with (e- (tvs (τ_body))) (⇑ e as ∀)
+     (⊢ e- : #,(substs #'(τ.norm ...) #'tvs #;#'(tv ...) #'τ_body))]))
\ No newline at end of file
diff --git a/tapl/tests/fomega-tests.rkt b/tapl/tests/fomega-tests.rkt
index 0be1146..36fca42 100644
--- a/tapl/tests/fomega-tests.rkt
+++ b/tapl/tests/fomega-tests.rkt
@@ -1,198 +1,204 @@
 #lang s-exp "../fomega.rkt"
 (require "rackunit-typechecking.rkt")
 
-(check-type Int : ★)
-(check-type String : ★)
+;(check-type Int : ★)
+(check-type Int : #%type)
+;(check-type String : ★)
+(check-type String : #%type)
 (typecheck-fail →)
-(check-type (→ Int Int) : ★)
+;(check-type (→ Int Int) : ★)
+(check-type (→ Int Int) : #%type)
 (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)) : (⇒ ★))
+;(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
+(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : #%type)
 
 (check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
 
 (check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
             : (∀ ([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)))
-(typecheck-fail
- (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1)
- #:with-msg "not a valid type: 1")
-
-;; 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
-(typecheck-fail
- (define-type-alias tmp 1)
- #:with-msg "not a valid type: 1")
-(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)))
+;(typecheck-fail
+; (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1)
+; #:with-msg "not a valid type: 1")
+;
+;;; 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
+;(typecheck-fail
+; (define-type-alias tmp 1)
+; #:with-msg "not a valid type: 1")
+;(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/fsub-tests.rkt b/tapl/tests/fsub-tests.rkt
index 6d927a4..4b4deb6 100644
--- a/tapl/tests/fsub-tests.rkt
+++ b/tapl/tests/fsub-tests.rkt
@@ -15,6 +15,10 @@
 (check-type (proj ((λ ([x : (× [a : Int])]) x) rab) a)
             : Int ⇒ 0)
 
+(check-type (Λ ([X <: Top]) (λ ([x : X]) x)) : (∀ ([X <: Top]) (→ X X)))
+(check-type (inst (Λ ([X <: Top]) (λ ([x : X]) x)) (× [a : Int][b : Bool]))
+            : (→ (× [a : Int][b : Bool]) (× [a : Int][b : Bool])))
+
 (check-type (proj ((inst (Λ ([X <: Top]) (λ ([x : X]) x))
                          (× [a : Int][b : Bool]))
                    rab) b)
@@ -29,7 +33,7 @@
 (define fNat (Λ ([X <: Nat]) (λ ([x : X]) (+ x 1))))
 (check-type fNat : (∀ ([X <: Nat]) (→ X Nat)))
 
-; check type constructors properly call expose
+;; check type constructors properly call expose
 (define f2poly
   (Λ ([X <: (× [a : Nat])])
      (λ ([x : X])
diff --git a/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
index 8ee98bd..4cf8507 100644
--- a/tapl/tests/run-all-tests.rkt
+++ b/tapl/tests/run-all-tests.rkt
@@ -22,6 +22,6 @@
 
 (require "fsub-tests.rkt") ; sysf + reco-sub
 
-;;; F_omega
-(require "fomega-tests.rkt")
-(require "fomega2-tests.rkt")
\ No newline at end of file
+;; F_omega
+;(require "fomega-tests.rkt")
+;(require "fomega2-tests.rkt")
\ No newline at end of file
diff --git a/tapl/tests/stlc+cons-tests.rkt b/tapl/tests/stlc+cons-tests.rkt
index 6d64eb8..7bd3e88 100644
--- a/tapl/tests/stlc+cons-tests.rkt
+++ b/tapl/tests/stlc+cons-tests.rkt
@@ -7,8 +7,14 @@
                 #:with-msg "nil: requires type annotation")
 (check-type (cons 1 (nil {Int})) : (List Int))
 (typecheck-fail nil #:with-msg "nil: requires type annotation")
-(typecheck-fail (nil Int) #:with-msg "expected ann")
-(typecheck-fail (nil (Int)) #:with-msg "expected ann")
+(typecheck-fail
+ (nil Int)
+ #:with-msg
+ "Improperly formatted type annotation: Int; should have shape {τ}, where τ is a valid type.")
+(typecheck-fail
+ (nil (Int))
+ #:with-msg
+ "Improperly formatted type annotation: \\(Int); should have shape {τ}, where τ is a valid type.")
 (typecheck-fail
  (λ ([lst : (List Int Int)]) lst)
  #:with-msg
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index 372af5e..e64fd1f 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -62,7 +62,7 @@
   ;; macro for nicer syntax
   (define-syntax (⊢ stx)
     (syntax-parse stx #:datum-literals (:)
-      [(_ e : τ) #'(assign-type #'e #`τ)]
+      [(_ e : τ) #'(assign-type #`e #`τ)]
       [(_ e τ) #'(⊢ e : τ)]))
        
   ;; assign-type Type -> Syntax
@@ -135,7 +135,9 @@
   ;; 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] #:octx [octx tvctx] #:tag [tag 'unused])
+  (define (infer es #:ctx [ctx null] #:tvctx [tvctx null]
+                 #:octx [octx tvctx] #:tag [tag 'unused]
+                 #:expand [expand expand/df])
     (syntax-parse ctx #:datum-literals (:)
       [([x : τ] ...) ; dont expand yet bc τ may have references to tvs
        #:with ([tv : k] ...) tvctx
@@ -156,7 +158,7 @@
           ((~literal #%plain-lambda) xs+
            ((~literal let-values) () ((~literal let-values) ()
             ((~literal #%expression) e+) ... (~literal void))))))))
-       (expand/df
+       (expand
         #`(λ (tv ...)
             (let-syntax ([tv (make-rename-transformer (assign-type (assign-type #'tv #'k) #'ok #:tag '#,tag))] ...)
               (λ (x ...)
@@ -177,8 +179,8 @@
   (define (infer/ctx+erase ctx e)
     (syntax-parse (infer (list e) #:ctx ctx)
       [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
-  (define (infers/ctx+erase ctx es)
-    (stx-cdr (infer es #:ctx ctx)))
+  (define (infers/ctx+erase ctx es #:expand [expand expand/df])
+    (stx-cdr (infer es #:ctx ctx #:expand expand)))
   ; tyctx = kind env for bound type vars in term e
   (define (infer/tyctx+erase ctx e)
     (syntax-parse (infer (list e) #:tvctx ctx)
@@ -239,7 +241,7 @@
 (begin-for-syntax
   ;; type validation
   ;; only check outer wrapper; tycons are responsible for verifying their own args
-  (define (#%type? t) (typecheck? t #'#%type))
+  #;(define (#%type? t) (typecheck? t #'#%type))
   #;(define (is-type? τ)
     (or (plain-type? τ)
         ; partial expand to reveal #%type wrapper
@@ -308,8 +310,8 @@
   (define (mk-? id) (format-id id "~a?" id))
   (define-for-syntax (mk-? id) (format-id id "~a?" id)))
 
-(define #%type void)
-(define-for-syntax (mk-type t) (assign-type t #'#%type))
+#;(define #%type void)
+#;(define-for-syntax (mk-type t) (assign-type t #'#%type))
 
 #;(define-syntax (define-base-type stx)
   (syntax-parse stx
@@ -361,12 +363,12 @@
                 #'e-]))))]))
 
 (define-syntax define-basic-checked-id-stx
-  (syntax-parser
-    [(_ τ:id (~optional (~seq : kind) #:defaults ([kind #'#%type])))
-     #:with τ? (format-id #'τ "~a?" #'τ)
+  (syntax-parser #:datum-literals (:)
+    [(_ τ:id : kind)
+     #:with τ? (mk-? #'τ)
      #:with τ-internal (generate-temporary #'τ)
-     #:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
-     #:with τ-cls (generate-temporary #'τ)
+     ;#:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
+     ;#:with τ-cls (generate-temporary #'τ)
      #:with τ-expander (format-id #'τ "~~~a" #'τ)
      #'(begin
          (provide τ (for-syntax τ? τ-expander))
@@ -395,26 +397,27 @@
            (syntax-parser
              [(~var _ id) (add-orig (assign-type #'τ-internal #'kind) #'τ)])))]))
 
-(define-syntax define-base-type (syntax-parser [(_ τ:id) #'(define-basic-checked-id-stx τ)]))
+#;(define-syntax define-base-type (syntax-parser [(_ τ:id) #'(define-basic-checked-id-stx τ)]))
 
 ; I use identifiers "τ" and "kind" but this form is not restricted to them.
 ; E.g., τ can be #'★ and kind can be #'#%kind (★'s type)
 (define-syntax (define-basic-checked-stx stx)
   (syntax-parse stx #:datum-literals (:)
-    [(_ τ:id (~optional (~seq : kind) #:defaults ([kind #'#%type]))
+    [(_ τ:id : kind
         (~optional
          (~seq #:arity op n:exact-nonnegative-integer)
          #:defaults ([op #'>=] [n #'0]))
         (~optional
          (~seq #:bvs (~and has-bvs? bvs-op) bvs-n:exact-nonnegative-integer)
          #:defaults ([bvs-op #'>=][bvs-n #'0])))
-     #:with kind+ ((current-type-eval) #'kind)
+     #:with #%kind (format-id #'kind "#%~a" #'kind)
+     ;#:with kind+ ((current-type-eval) #'kind)
      #: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" #'τ)
-     #:with τ-get (format-id #'τ "~a-get" #'τ)
+     ;#:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
+     ;#:with τ-get (format-id #'τ "~a-get" #'τ)
      #`(begin
          (provide τ (for-syntax τ-expander τ-expander* τ? #;inferτ+erase))
          (begin-for-syntax
@@ -450,25 +453,25 @@
              (and (stx-pair? t)
                   (syntax-parse t
                     [((~literal #%plain-lambda) bvs ((~literal #%plain-app) tycon . _))
-                     (typecheck? #'tycon #'τ-internal)])))
-           #;(define (τ-get t)
-             (syntax-parse t
-               [(τ-expander . pat) #'pat]))
-           #;(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)])))
+                     (typecheck? #'tycon #'τ-internal)]))))
+;           #;(define (τ-get t)
+;             (syntax-parse t
+;               [(τ-expander . pat) #'pat]))
+;           #;(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" 'τ)
@@ -485,186 +488,188 @@
                             (format "wrong number of type vars, expected ~a ~a" 'bvs-op 'bvs-n)
               #:fail-unless (op (stx-length #'args) n)
                             (format "wrong number of arguments, expected ~a ~a" 'op 'n)
-              #:with (bvs- τs- ks) (infers/ctx+erase #'([bv : kind] (... ...)) #'args)
-              #:when (stx-andmap
-                      (λ (t k)
-                        (or (typecheck? k #'kind+)
-                            (type-error #:src  t
-                                        #:msg "not a valid type: ~a" t)))
-                      #'args #'ks)
-              ;#:with (~! (~var _ type) (... ...)) #'τs-
+              #:with (bvs- τs- _)
+                     (infers/ctx+erase #'([bv : #%kind] (... ...)) #'args
+                                       #:expand (current-type-eval))
+;              #:when (stx-andmap
+;                      (λ (t k)
+;                        (or (typecheck? k #'kind+)
+;                            (type-error #:src  t
+;                                        #:msg "not a valid type: ~a" t)))
+;                      #'args #'ks)
+               #:with (~! (~var _ kind) (... ...)) #'τs-
 ;              #:with (~! [arg- τ_arg] (... ...)) (infers+erase #'args)
 ;              #:when (stx-andmap (λ (t) (typecheck? t #'#%type)) #'(τ_arg (... ...)))
-              (assign-type #'(λ bvs- (τ-internal . τs-)) #'kind)]
+              (assign-type #'(λ bvs- (τ-internal . τs-)) #'#%kind)]
              ;; 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]))
-        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)])))]))
+                          #'τ 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]))
+;        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)])))]))
 
 ; define-type-constructor, archied 2015-08-12
 ;(define-syntax define-type-constructor
@@ -897,31 +902,40 @@
 (define-syntax (define-syntax-category stx)
   (syntax-parse stx
     [(_ name:id)
+     #:with names (format-id #'name "~as" #'name)
      #:with #%tag (format-id #'name "#%~a" #'name)
      #:with #%tag? (mk-? #'#%tag)
-     #:with name? (mk-? #'name)
-     #:with named-binding (format-id #'name "~aed-binding" #'name)
-     #:with current-name? (format-id #'name? "current-~a" #'name?)
+     #:with is-name? (mk-? #'name)
+     #:with name-ctx (format-id #'name "~a-ctx" #'name)
+     #:with name-bind (format-id #'name "~a-bind" #'name)
+     #:with current-is-name? (format-id #'is-name? "current-~a" #'is-name?)
+     #:with mk-name (format-id #'name "mk-~a" #'name)
+     #:with define-base-name (format-id #'name "define-base-~a" #'name)
+     #:with define-name-cons (format-id #'name "define-~a-constructor" #'name)
+     #:with name-ann (format-id #'name "~a-ann" #'name)
      #'(begin
+         (provide (for-syntax current-is-name? is-name? #%tag? mk-name name name-bind name-ann)
+                  #%tag define-base-name define-name-cons)
          (define #%tag void)
          (begin-for-syntax
            (define (#%tag? t) (typecheck? t #'#%tag))
-           (define (name? t) (#%tag? (typeof t)))
-           (define current-name? (make-parameter name?))
+           (define (is-name? t) (#%tag? (typeof t)))
+           (define current-is-name? (make-parameter is-name?))
+           (define (mk-name t) (assign-type t #'#%tag))
            (define-syntax-class name
              #:attributes (norm)
              (pattern τ
               #:with norm ((current-type-eval) #'τ)
               #:with k (typeof #'norm)
-              #:fail-unless (#%tag? #'k)
-              ;#:fail-unless ((current-name?) #'norm)
-              ;#:fail-unless ((current-name?) #'norm)
+              ;#:fail-unless (#%tag? #'k)
+              #:fail-unless ((current-is-name?) #'norm)
               (format "~a (~a:~a) not a valid ~a: ~a"
                       (syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ)
                       'name (type->str #'τ))))
-           (define-syntax-class named-binding #:datum-literals (:)
-             #:attributes (x tag)
-             (pattern [x:id : ~! (~var ty name)] #:attr tag #'ty.norm)
+           (define-syntax-class name-bind #:datum-literals (:)
+             #:attributes (x name)
+             (pattern [x:id : ~! (~var ty name)]
+                      #:attr name #'ty.norm)
              (pattern any
                       #:fail-when #t
                       (format
@@ -929,10 +943,35 @@
                         "Improperly formatted ~a annotation: ~a; should have shape [x : τ], "
                         "where τ is a valid ~a.")
                        'name (type->str #'any) 'name)
-                      #:attr x #f #:attr tag #f))))]))
+                      #:attr x #f #:attr name #f))
+           (define-syntax-class name-ctx
+             #:attributes ((x 1) (name 1))
+             (pattern ((~var || name-bind) (... ...))))
+           (define-syntax-class name-ann ; type instantiation
+             #:attributes (norm)
+             (pattern stx
+                      #:when (stx-pair? #'stx)
+                      #:when (brace? #'stx)
+                      #:with ((~var t name)) #'stx
+                      #:attr norm (delay #'t.norm))
+             (pattern any
+                      #:fail-when #t
+                      (type-error #:src #'any #:msg 
+                       (format
+                        (string-append
+                        "Improperly formatted ~a annotation: ~a; should have shape {τ}, "
+                        "where τ is a valid ~a.")
+                       'name (type->str #'any) 'name))
+                      #:attr norm #f)))
+         (define-syntax define-base-name
+           (syntax-parser
+             [(_ (~var x id)) #'(define-basic-checked-id-stx x : #%tag)]))
+         (define-syntax define-name-cons
+           (syntax-parser
+             [(_ (~var x id) . rst)  #'(define-basic-checked-stx x : name . rst)])))]))
 ;; syntax classes
 (begin-for-syntax
-  (define-syntax-class type
+  #;(define-syntax-class 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
@@ -946,7 +985,7 @@
                            (syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ)
                            (type->str #'τ))))
 
-  (define-syntax-class typed-binding #:datum-literals (:)
+  #;(define-syntax-class typed-binding #:datum-literals (:)
     #:attributes (x τ)
     (pattern [x:id : ~! ty:type] #:attr τ #'ty.norm)
     (pattern any
@@ -961,7 +1000,7 @@
   (define (brace? stx)
     (define paren-shape/#f (syntax-property stx 'paren-shape))
     (and paren-shape/#f (char=? paren-shape/#f #\{)))
-  (define-syntax-class ann ; type instantiation
+  #;(define-syntax-class ann ; type instantiation
     #:attributes (τ norm)
     (pattern stx
              #:when (stx-pair? #'stx)
@@ -979,7 +1018,7 @@
 
 
 
-(define-syntax (define-primop stx)
+#;(define-syntax (define-primop stx)
     (syntax-parse stx #:datum-literals (:)
       [(_ op:id : τ (~optional (~seq : k) #:defaults ([k #'#%type])))
        #:with kind ((current-type-eval) #'k)
@@ -997,7 +1036,7 @@
                 #:with op (format-id stx "~a" #'op)
                 (syntax/loc stx (app op x (... ...)))])))]))
 
-(define-for-syntax (mk-acc base field) (format-id base "~a-~a" base field))
+;(define-for-syntax (mk-acc base field) (format-id base "~a-~a" base field))
 
 (begin-for-syntax
   ; subst τ for y in e, if (bound-id=? x y)