diff --git a/tapl/exist.rkt b/tapl/exist.rkt
index 4254371..c7367f8 100644
--- a/tapl/exist.rkt
+++ b/tapl/exist.rkt
@@ -1,12 +1,10 @@
 #lang racket/base
 (require "typecheck.rkt")
 (require (except-in "stlc+reco+var.rkt" #%app λ let type=?)
-         (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ let #;type=?))
+         (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ let))
          (only-in "stlc+rec-iso.rkt" type=?))
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let])
-         #;(for-syntax type=?))
-(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app stlc:λ stlc:let
-                     #;(for-syntax stlc:type=?))
+(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let]))
+(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app stlc:λ stlc:let)
          (all-from-out "stlc+rec-iso.rkt"))
 (provide ∃ pack open)
 
@@ -28,29 +26,34 @@
 
 
 #;(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) τ)
-        #'(~or
-           ((~literal #%plain-lambda) (tv) τ)
-           (~and any (~do
-                      (type-error
-                       #:src #'any
-                       #:msg "Expected ∃ type, got: ~a" #'any))))]))))
+;(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-syntax (pack stx)
   (syntax-parse stx
@@ -64,7 +67,11 @@
 (define-syntax (open stx)
   (syntax-parse stx #:datum-literals (<=)
     [(_ ([(tv:id x:id) <= e_packed]) e)
-     #:with [e_packed- (τ_abstract τ_body)] (infer∃+erase #'e_packed)
+;     #:with [e_packed- τ_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.
diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
index abb2bc0..bc2df66 100644
--- a/tapl/ext-stlc.rkt
+++ b/tapl/ext-stlc.rkt
@@ -47,8 +47,10 @@
 (define-syntax (and/tc stx)
   (syntax-parse stx
     [(_ e1 e2)
-     #:with e1- (inferBool+erase #'e1)
-     #:with e2- (inferBool+erase #'e2)
+;     #:with e1- (inferBool+erase #'e1)
+;     #:with e2- (inferBool+erase #'e2)
+     #:with e1- (⇑ e1 as Bool)
+     #:with e2- (⇑ e2 as Bool)
 ;     #:with (e1- τ1) (infer+erase #'e1)
 ;     #:fail-unless (Bool? #'τ1) (format "given non-Bool arg: ~a\n" (syntax->datum #'e1))
 ;     #:with (e2- τ2) (infer+erase #'e2)
@@ -58,8 +60,10 @@
 (define-syntax (or/tc stx)
   (syntax-parse stx
     [(_ e1 e2)
-     #:with e1- (inferBool+erase #'e1)
-     #:with e2- (inferBool+erase #'e2)
+;     #:with e1- (inferBool+erase #'e1)
+;     #:with e2- (inferBool+erase #'e2)
+     #:with e1- (⇑ e1 as Bool)
+     #:with e2- (⇑ e2 as Bool)
 ;     #:with (e1- τ1) (infer+erase #'e1)
 ;     #:fail-unless (Bool? #'τ1) (format "given non-Bool arg: ~a\n" (syntax->datum #'e1))
 ;     #:with (e2- τ2) (infer+erase #'e2)
@@ -69,13 +73,13 @@
 (define-syntax (if/tc stx)
   (syntax-parse stx
     [(_ e_tst e1 e2)
-     #:with e_tst- (inferBool+erase #'e_tst)
+     #:with e_tst- (⇑ e_tst as Bool)
 ;     #:with (e_tst- τ_tst) (infer+erase #'e_tst)
 ;     #:fail-unless (Bool? #'τ_tst) (format "given non-Bool test: ~a\n" (syntax->datum #'e_tst))
      #:with (e1- τ1) (infer+erase #'e1)
      #:with (e2- τ2) (infer+erase #'e2)
-     #:fail-unless (or ((current-typecheck-relation) #'τ1 #'τ2)
-                       ((current-typecheck-relation) #'τ2 #'τ1))
+     #:fail-unless (or (typecheck? #'τ1 #'τ2)
+                       (typecheck? #'τ2 #'τ1))
                    (format "branches must have the same type: given ~a and ~a"
                            (type->str #'τ1) (type->str #'τ2))
      (⊢ (if e_tst- e1- e2-) : τ1)]))
@@ -86,7 +90,8 @@
 (define-syntax (begin/tc stx)
   (syntax-parse stx
     [(_ e_unit ... e)
-     #:with (e_unit- ...) (stx-map inferUnit+erase #'(e_unit ...))
+     ;#:with (e_unit- ...) (stx-map inferUnit+erase #'(e_unit ...))
+     #:with (e_unit- ...) (⇑s (e_unit ...) as Unit)
 ;     #:with ([e_unit- τ_unit] ...) (infers+erase #'(e_unit ...))
 ;     #:fail-unless (stx-andmap Unit? #'(τ_unit ...))
 ;                   (string-append
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
index c0875c3..f2bdd24 100644
--- a/tapl/fomega.rkt
+++ b/tapl/fomega.rkt
@@ -1,13 +1,15 @@
 #lang racket/base
 (require "typecheck.rkt")
 (require (except-in "sysf.rkt" #%app λ Int #%datum → Λ inst ∀  + type-eval)
-         (prefix-in sysf: (only-in "sysf.rkt" #%app λ Int → ∀ type-eval))
+         (prefix-in sysf: (only-in "sysf.rkt" type-eval))
          (only-in "stlc+reco+var.rkt" same-types?))
 (provide (rename-out [app/tc #%app] [λ/tc λ] [datum/tc #%datum]))
-(provide (except-out (all-from-out "sysf.rkt")
+#;(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))
+         (all-from-out "stlc+reco+var.rkt"))
 (provide Int → ∀ inst Λ tyλ tyapp
          (for-syntax type-eval))
 
@@ -18,11 +20,15 @@
 ;; Terms:
 ;; - terms from sysf.rkt
 
+(define-syntax-category kind)
+
 (provide define-type-alias)
 (define-syntax define-type-alias
   (syntax-parser
-    [(_ alias:id τ:type)
-     #'(define-syntax alias (syntax-parser [x:id #'τ]))]))
+    [(_ alias:id τ)
+     #:with (τ- k_τ) (infer+erase #'τ)
+     #:fail-unless (kind? #'k_τ) (format "not a valid type: ~a\n" (type->str #'τ))
+     #'(define-syntax alias (syntax-parser [x:id #'τ-]))]))
 
 (begin-for-syntax
   ;; extend type-eval to handle tyapp
@@ -33,23 +39,26 @@
        #:with ((~literal #%plain-lambda) (tv ...) τ_body) ((current-type-eval) #'τ_fn)
        #:with (τ_arg+ ...) (stx-map (current-type-eval) #'(τ_arg ...))
        (substs #'(τ_arg+ ...) #'(tv ...) #'τ_body)]
-      [((~literal ∀) _ ...) ((current-type-eval) (sysf:type-eval τ))]
-      [((~literal →) _ ...) ((current-type-eval) (sysf:type-eval τ))]
-      [((~literal ⇒) _ ...) ((current-type-eval) (sysf:type-eval τ))]
-      [((~literal tyλ) _ ...) (sysf:type-eval τ)]
-      [((~literal tyapp) _ ...) ((current-type-eval) (sysf:type-eval τ))]
+      [((~or (~literal ∀)(~literal →)
+             (~literal ⇒)(~literal tyapp)) . _)
+       ((current-type-eval) (sysf:type-eval τ))]
+      ;[((~literal →) _ ...) ((current-type-eval) (sysf:type-eval τ))]
+      ;[((~literal ⇒) _ ...) ((current-type-eval) (sysf:type-eval τ))]
+      ;[((~literal tyapp) _ ...) ((current-type-eval) (sysf:type-eval τ))]
+      ;[((~literal tyλ) _ ...) (sysf:type-eval τ)] ; dont eval under tyλ
       [((~literal #%plain-lambda) (x ...) τ_body ...)
        #:with (τ_body+ ...) (stx-map (current-type-eval) #'(τ_body ...))
-       (syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'plain-lambda)]
+       (syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'#%plain-lambda)]
       [((~literal #%plain-app) arg ...)
        #:with (arg+ ...) (stx-map (current-type-eval) #'(arg ...))
        (syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
-      ;[(τ ...) (stx-map (current-type-eval) #'(τ ...))]
-      [_ (sysf:type-eval τ)]))
+      [(~or x:id ((~literal tyλ) . _)) ; dont eval under tyλ
+       (sysf:type-eval τ)]))
   (current-type-eval type-eval))
 
-(define-base-type ★)
-(define-type-constructor (⇒ k_in ... k_out))
+(define-basic-checked-id-stx ★ : #%kind)
+(define-basic-checked-stx ⇒ : #%kind #:arity >= 1)
+;(define-type-constructor (⇒ k_in ... k_out))
 
 ;; for now, handle kind checking in the types themselves
 ;; TODO: move kind checking to a common place (like #%app)?
@@ -57,13 +66,16 @@
 
 ;; TODO: need some kind of "promote" abstraction,
 ;; so I dont have to manually add kinds to all types
-(define-base-type Str)
-(provide String)
-(define-syntax String (syntax-parser [x:id (⊢ Str : ★)]))
-(define-syntax Int (syntax-parser [x:id (⊢ sysf:Int : ★)]))
+(define-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-syntax (→ stx)
+(define-basic-checked-stx → : ★ #:arity >= 1)
+#;(define-syntax (→ stx)
   (syntax-parse stx
     [(_ τ ... τ_res)
      #:with ([τ- k] ... [τ_res- k_res]) (infers+erase #'(τ ... τ_res))
@@ -73,36 +85,37 @@
 
 (define-syntax (∀ stx)
   (syntax-parse stx
-    [(∀ (b:typed-binding ...) τ)
-     #:with ((tv- ...) τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
-     #:when (typecheck? #'k #'★)
-     (⊢ (#%type
-         (λ (tv- ...)
-          (let-syntax ([tv- (syntax-parser [tv-:id #'(#%type tv-)])] ...)
-           b.τ ... τ-))) #;(sysf:∀ #:bind tvs- τ-) : ★)]))
+    [(_ (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
-    [(_ (b:typed-binding ...) e)
-     #:with ((tv- ...) e- τ) (infer/type-ctxt+erase #'(b ...) #'e)
-     #:when (displayln #'(∀ ([tv- : b.τ] ...) τ))
-     (⊢ e- : (∀ ([tv- : b.τ] ...) τ))]))
+    [(_ (b:kinded-binding ...) e)
+     #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'(b ...) #'e)
+     (⊢ e- : (∀ ([tv- : b.tag] ...) τ_e))]))
 (define-syntax (inst stx)
   (syntax-parse stx
-    [(_ e τ:type ...)
-     #:with ([τ- k] ...) (infers+erase #'(τ ...))
+    [(_ e τ ...)
+     #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
+     #:when (stx-andmap
+             (λ (t k)
+               (or (kind? k)
+                   (type-error #:src t
+                               #:msg "not a valid type: ~a" t)))
+             #'(τ ...) #'(k_τ ...))
      #:with (e- ∀τ) (infer+erase #'e)
      #:with ((~literal #%plain-lambda) (tv ...) k_tv ... τ_body) #'∀τ
-     #:when (typechecks? #'(k ...) #'(k_tv ...))
-     (⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
+     #:when (typechecks? #'(k_τ ...) #'(k_tv ...))
+     (⊢ e- : #,(substs #'(τ ...) #'(tv ...) #'τ_body))]))
 
 ;; TODO: merge with regular λ and app?
 (define-syntax (tyλ stx)
   (syntax-parse stx 
-    [(_ (b:typed-binding ...) τ)
-     #:with (tvs- τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
-     ;; b.τ's here are actually kinds
-     (⊢ (λ tvs- τ-) : (⇒ b.τ ... k))]))
+    [(_ (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
@@ -163,14 +176,16 @@
 ;; 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)
-  (syntax-parse stx 
-    [(_ (b:typed-binding ...) e)
-     #:when (andmap ★? (stx-map (λ (t) (typeof (expand/df t))) #'(b.τ ...)))
-     #:with (xs- e- τ_res) (infer/type-ctxt+erase #'(b ...) #'e)
-     (⊢ (λ xs- e-) : (→ b.τ ... τ_res))]))
+  (syntax-parse stx #:datum-literals (:)
+    [(_ ([x : τ] ...) e)
+     ;#:when (andmap ★? (stx-map (λ (t) (typeof (expand/df t))) #'(τ ...)))
+     #:with (k ...) (stx-map (λ (t) (typeof ((current-type-eval) t))) #'(τ ...))
+     #:when (stx-andmap ★? #'(k ...))
+     #:with (xs- e- τ_res) (infer/type-ctxt+erase #'([x : τ] ...) #'e)
+     (⊢ (λ xs- e-) : (→ τ ... τ_res))]))
 
 (define-syntax (app/tc stx)
   (syntax-parse stx
diff --git a/tapl/fomega2.rkt b/tapl/fomega2.rkt
index 2faabdb..8969497 100644
--- a/tapl/fomega2.rkt
+++ b/tapl/fomega2.rkt
@@ -1,34 +1,35 @@
 #lang racket/base
 (require "typecheck.rkt")
 (require (except-in "sysf.rkt" #%app λ Int #%datum → Λ inst ∀  + type-eval)
-         (prefix-in sysf: (only-in "sysf.rkt" #%app λ Int → ∀ type-eval)))
+         (prefix-in sysf: (only-in "sysf.rkt" type-eval))
+         (only-in "stlc+reco+var.rkt" same-types?))
 (provide (rename-out [app/tc #%app] [λ/tc λ] [datum/tc #%datum]))
-(provide (except-out (all-from-out "sysf.rkt")
+#;(provide (except-out (all-from-out "sysf.rkt")
                      sysf:Int sysf:→ sysf:∀
                      sysf:#%app sysf:λ
                      (for-syntax sysf:type-eval)))
-(provide Int → ∀ inst Λ
-         (for-syntax type-eval))
+(provide (except-out (all-from-out "sysf.rkt") (for-syntax sysf:type-eval))
+         (all-from-out "stlc+reco+var.rkt"))
+(provide Int → ∀ inst Λ (for-syntax type-eval))
 
 ;; same as fomega.rkt, except tyapp == #%app, tyλ = λ, and ⇒ = →
 
-;; System F_omega 
+;; System F_omega
 ;; Type relation:
 ;; Types:
 ;; - types from sysf.rkt
 ;; Terms:
 ;; - terms from sysf.rkt
 
+(define-syntax-category kind)
+
 (provide define-type-alias)
 (define-syntax define-type-alias
   (syntax-parser
-    [(_ alias:id τ:type)
-     ; must eval, otherwise undefined types will be allowed
-     #'(define-syntax alias
-         (syntax-parser
-           [x:id #'τ.norm]
-           [(_ x (... ...))
-            ((current-type-eval) (⊢ #'(#%plain-app τ.norm x (... ...)) #'★))]))]))
+    [(_ alias:id τ)
+     #:with (τ- k_τ) (infer+erase #'τ)
+     #:fail-unless (kind? #'k_τ) (format "not a valid type: ~a\n" (type->str #'τ))
+     #'(define-syntax alias (syntax-parser [x:id #'τ-]))]))
 
 (begin-for-syntax
   ;; extend type-eval to handle tyapp
@@ -54,46 +55,56 @@
       [_ (sysf:type-eval τ)]))
   (current-type-eval type-eval))
 
-(define-base-type ★)
-;(define-type-constructor ⇒)
+(define-basic-checked-id-stx ★ : #%kind)
+(define-basic-checked-id-stx String : ★)
+(define-basic-checked-id-stx Int : ★)
 
-;; for now, handle kind checking in the types themselves
-;; TODO: move kind checking to a common place (like #%app)?
-;; when expanding: check and erase kinds
-
-;; TODO: need some kind of "promote" abstraction,
-;; so I dont have to manually add kinds to all types
-(define-base-type Str)
-(provide String)
-(define-syntax String (syntax-parser [x:id (⊢ #'Str #'★)]))
-(define-syntax Int (syntax-parser [x:id (⊢ #'sysf:Int #'★)]))
-
-;; → in Fω is not first-class, can't pass it around
-(define-syntax (→ stx)
+(define-syntax (define-multi stx)
   (syntax-parse stx
-    [(_ τ ... τ_res)
-     #:with ([τ- k] ... [τ_res- k_res]) (infers+erase #'(τ ... τ_res))
-     #:when (or
-             ; when used as →
-             (and (typecheck? #'k_res #'★)
-                  (same-types? #'(k ... k_res)))
-             ; when used as ⇒
-             (not (syntax-e (stx-ormap (λ (x) x) #'(k ... k_res)))))
-     (⊢ #'(sysf:→ τ- ... τ_res-) #'★)]))
+    [(_ tycon:id)
+     #:with tycon-internal (generate-temporary #'tycon)
+     #'(...
+        (begin
+          (define tycon-internal void)
+          (define-syntax (tycon stx)
+            (syntax-parse stx
+              [(_ τ ... τ_res)
+               #:with ([τ- k] ... [τ_res- k_res]) (infers+erase #'(τ ... τ_res))
+               #:when (or ; when used as →
+                       (and (or (★? #'k_res) (#%kind? #'k_res))
+                            (same-types? #'(k ... k_res))))
+               (if (★? #'k_res)
+                   (⊢ (tycon-internal τ- ... τ_res-) : ★)
+                   (⊢ (tycon-internal τ- ... τ_res-) : #%kind))]))))]))
+(define-multi →)
 
 (define-syntax (∀ stx)
   (syntax-parse stx
-    [(∀ (b:typed-binding ...) τ)
+    [(_ (b:kinded-binding ...) τ)
      #:with (tvs- τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
-     #:when (typecheck? #'k #'★)
-     (⊢ #'(#%plain-lambda tvs- b.τ ... τ-) #;#'(sysf:∀ tvs- τ-) #'★)]))
+     #:when (★? #'k)
+     (⊢ (λ tvs- b.tag ... τ-) : ★)]))
 
 (define-syntax (Λ stx)
   (syntax-parse stx
-    [(_ (b:typed-binding ...) e)
+    [(_ (b:kinded-binding ...) e)
      #:with ((tv- ...) e- τ) (infer/type-ctxt+erase #'(b ...) #'e)
-     (⊢ #'e- #'(∀ ([tv- : b.τ] ...) τ))]))
+     (⊢ e- : (∀ ([tv- : b.tag] ...) τ))]))
 (define-syntax (inst stx)
+  (syntax-parse stx
+    [(_ e τ ...)
+     #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
+     #:when (stx-andmap
+             (λ (t k)
+               (or (kind? k)
+                   (type-error #:src t
+                               #:msg "not a valid type: ~a" t)))
+             #'(τ ...) #'(k_τ ...))
+     #:with (e- ∀τ) (infer+erase #'e)
+     #: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 ([τ- k] ...) (infers+erase #'(τ ...))
@@ -102,9 +113,19 @@
      #:when (typechecks? #'(k ...) #'(k_tv ...))
      (⊢ #'e- (substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
 
-(define-primop + : (→ Int Int Int))
+(define-primop + : (→ Int Int Int) : ★)
 
 (define-syntax (λ/tc stx)
+  (syntax-parse stx #:datum-literals (:)
+    [(_ ([x : τ] ...) e)
+     ;#:when (andmap ★? (stx-map (λ (t) (typeof (expand/df t))) #'(τ ...)))
+     #:with (k ...) (stx-map (λ (t) (typeof ((current-type-eval) t))) #'(τ ...))
+     #:when (or (stx-andmap ★? #'(k ...))
+                (stx-andmap #%kind? #'(k ...)))
+     #:with (xs- e- τ_res) (infer/type-ctxt+erase #'([x : τ] ...) #'e)
+     (⊢ (λ xs- e-) : (→ τ ... τ_res))]))
+
+#;(define-syntax (λ/tc stx)
   (syntax-parse stx 
     [(_ (b:typed-binding ...) e)
      #:with (k ...) (stx-map (λ (t) (typeof (expand/df t))) #'(b.τ ...))
@@ -117,6 +138,26 @@
      (⊢ #'(λ xs- e-) #'(→ b.τ ... τ_res))]))
 
 (define-syntax (app/tc stx)
+  (syntax-parse stx
+    [(_ e_fn e_arg ...)
+     #:with [e_fn- ((~literal #%plain-lambda) _ τ_in ... τ_out)] (infer+erase #'e_fn)
+     #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
+     #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
+                   (string-append
+                    (format "~a (~a:~a) Arguments to function ~a have wrong type(s), "
+                            (syntax-source stx) (syntax-line stx) (syntax-column stx)
+                            (syntax->datum #'e_fn))
+                    "or wrong number of arguments:\nGiven:\n"
+                    (string-join
+                     (map (λ (e t) (format "  ~a : ~a" e t)) ; indent each line
+                          (syntax->datum #'(e_arg ...))
+                          (stx-map type->str #'(τ_arg ...)))
+                     "\n" #:after-last "\n")
+                    (format "Expected: ~a arguments with type(s): "
+                            (stx-length #'(τ_in ...)))
+                    (string-join (stx-map type->str #'(τ_in ...)) ", "))
+     (⊢ (#%app e_fn- e_arg- ...) : τ_out)]))
+#;(define-syntax (app/tc stx)
   (syntax-parse stx
     [(_ e_fn e_arg ...)
      #:with [e_fn- τ_fn] (infer+erase #'e_fn)
@@ -158,8 +199,8 @@
 ;; must override #%datum to use new kinded-Int, etc
 (define-syntax (datum/tc stx)
   (syntax-parse stx
-    [(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)]
-    [(_ . s:str) (⊢ (syntax/loc stx (#%datum . s)) #'String)]
+    [(_ . n:integer) (⊢ (#%datum . n) : Int)]
+    [(_ . s:str) (⊢ (#%datum . s) : String)]
     [(_ . x)
      #:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
      #'(#%datum . x)]))
\ No newline at end of file
diff --git a/tapl/fsub.rkt b/tapl/fsub.rkt
index f85c639..b6b8d62 100644
--- a/tapl/fsub.rkt
+++ b/tapl/fsub.rkt
@@ -1,15 +1,16 @@
 #lang racket/base
 (require "typecheck.rkt")
-(require (except-in "sysf.rkt" #%app #%datum + ∀ Λ inst type=?)
-         (prefix-in sysf: (only-in "sysf.rkt" #%app ∀ Λ inst type=?))
-         (except-in "stlc+reco+sub.rkt" #%app + type=? sub?)
-         (prefix-in stlc: (only-in "stlc+reco+sub.rkt" type=? sub?)))
-(provide (rename-out [sysf:#%app #%app]) (for-syntax sub?))
-(provide (except-out (all-from-out "sysf.rkt")
-                     sysf:#%app sysf:∀ sysf:Λ sysf:inst
-                     (for-syntax sysf:type=?))
-         (except-out (all-from-out "stlc+reco+sub.rkt")
-                     (for-syntax stlc:type=? stlc:sub?)))
+(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
+(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)
  
 ;; System F<:
@@ -20,6 +21,11 @@
 
 (define-primop + : (→ Nat Nat Nat))
 
+; can't just call expose in type-eval,
+; otherwise typevars will have bound as type, rather than instantiated type
+; only need expose during
+; 1) subtype checking
+; 2) pattern matching -- including base types
 (begin-for-syntax
   (define (expose t)
     (cond [(identifier? t)
@@ -27,11 +33,12 @@
            (if sub (expose sub) t)]
           [else t]))
   (current-promote expose)
+  ; need this, to lift base-types; is there another way to do this?
   (define (sub? t1 t2)
     (stlc:sub? (expose t1) (expose t2)))
   (current-sub? sub?)
   ;; extend to handle new ∀
-  (define (type=? τ1 τ2)
+  #;(define (type=? τ1 τ2)
     (syntax-parse (list τ1 τ2)
       [(((~literal #%plain-lambda) (x:id ...) k1 ... t1)
         ((~literal #%plain-lambda) (y:id ...) k2 ... t2))
@@ -39,36 +46,80 @@
        #:when (= (stx-length #'(x ...)) (stx-length #'(k1 ...)))
        ((current-type=?) (substs #'(k1 ...) #'(x ...) #'t1)
                          (substs #'(k2 ...) #'(y ...) #'t2))]
-      [_ (or (sysf:type=? τ1 τ2) (stlc:type=? τ1 τ2))]))
-  (current-type=? type=?)
+      [_ (or (sysf:type=? τ1 τ2) (stlc+reco+sub:type=? τ1 τ2))]))
+  #;(current-type=? type=?)
   (current-typecheck-relation (current-sub?)))
 
-;; TODO: shouldnt really support non-bounded (ie, no <: annotation) ∀, etc
-;; but support for now, so old tests pass
-(define-syntax (∀ stx)
+;; 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 ...)]))
+    #;[(_ x ...) #'(sysf:∀ x ...)]))
+(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-)))]))
+(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 ... τ))]
+       [(_ . args)
+        #'(~and ((~literal #%plain-lambda) (tv (... ...))
+                 ((~literal #%plain-app) (~literal ∀-internal) τ_sub (... ...) τ))
+                (~parse args #'(([tv τ_sub] (... ...)) τ)))])))
+  (define-syntax ~∀*
+    (pattern-expander
+     (syntax-parser #:datum-literals (<:)
+       [(_ . args) ; (_ ([tv:id <: τ_sub] ...) τ)
+        #'(~or
+           (~∀ . args)
+           ;((~literal #%plain-lambda) (tv ...) τ_sub ... τ)
+           (~and any (~do
+                      (type-error
+                       #:src #'any
+                       #:msg "Expected ∀ type, got: ~a" #'any))))]))))
 
 (define-syntax (Λ stx)
   (syntax-parse stx #:datum-literals (<:)
-    [(_ ([tv:id <: τsub] ...) ~! e)
-     ;; NOTE: we are storing the subtyping relation of tv and τsub in the
-     ;; "environment", as we store type annotations
-     ;; So we need to add "expose" to certain forms that expect a certain type,
+    [(_ ([tv:id <: τsub:type] ...) e)
+     ;; NOTE: store the subtyping relation of tv and τsub in another
+     ;; "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) #:ctx #'([tv : τsub] ...) #:tag 'sub)
-     (⊢ #'e- #'(∀ ([tv- <: τsub] ...) τ))]
-    [(_ x ...) #'(sysf:Λ x ...)]))
+     #:with ((tv- ...) _ (e-) (τ)) (infer #'(e) #:tvctx #'([tv : #%type] ...)
+                                                #:octx #'([tv : τsub] ...) #:tag 'sub)
+     (⊢ e- : (∀ ([tv- <: τsub] ...) τ))]
+    #;[(_ x ...) #'(sysf:Λ x ...)]))
 (define-syntax (inst stx)
   (syntax-parse stx
     [(_ e τ:type ...)
-     #:with (e- ∀τ) (infer+erase #'e)
-     #:with ((~literal #%plain-lambda) (tv:id ...) τ_sub ... τ_body) #'∀τ
+     ;#: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
+     (⊢ 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 τ ...)]))
diff --git a/tapl/notes.txt b/tapl/notes.txt
index 51b6d3a..de1075e 100644
--- a/tapl/notes.txt
+++ b/tapl/notes.txt
@@ -1,3 +1,20 @@
+2015-08-16:
+TODO:
+- generalize binding forms
+- add tags to distinguish different binding forms
+
+2015-08-16:
+Paper outline
+
+stlc.rkt
+Concepts: 
+- #%app
+- lambda
+- user input types must be checked
+
+stlc+rec-iso.rkt
+Concept(s): binding form, type=? for binding forms
+
 2015-08-13
 Requirements for define-type-constructor syntax:
 - identifier types, like Int
diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt
index 1b46515..4eda06a 100644
--- a/tapl/stlc+box.rkt
+++ b/tapl/stlc+box.rkt
@@ -25,12 +25,14 @@
   (syntax-parse stx
     [(_ e)
 ;     #:with (e- (~Ref* τ)) (infer+erase #'e) ; alternate pattern; worse err msg
-     #:with (e- (τ)) (inferRef+erase #'e)
+;     #: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)) (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)
diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt
index 98c713f..257374b 100644
--- a/tapl/stlc+cons.rkt
+++ b/tapl/stlc+cons.rkt
@@ -29,7 +29,8 @@
   (syntax-parse stx
     [(_ e1 e2)
      #:with (e1- τ1) (infer+erase #'e1)
-     #:with (e2- (τ2)) (inferList+erase #'e2)
+;     #: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)
@@ -37,14 +38,16 @@
 (define-syntax (isnil stx)
   (syntax-parse stx
     [(_ e)
-     #:with (e- _) (inferList+erase #'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- (τ)) (inferList+erase #'e)
+     #:with (e- (τ)) (⇑ e as List)
 ;     #:with (e- τ-lst) (infer+erase #'e)
 ;     #:with τ (List-get τ from τ-lst)
      (⊢ (car e-) : τ)]))
diff --git a/tapl/stlc+rec-iso.rkt b/tapl/stlc+rec-iso.rkt
index 5f262d1..4b0d70c 100644
--- a/tapl/stlc+rec-iso.rkt
+++ b/tapl/stlc+rec-iso.rkt
@@ -17,15 +17,16 @@
 ;; - terms from stlc+reco+var.rkt
 ;; - fld/unfld
 
+(define-basic-checked-stx μ #:arity = 1 #:bvs = 1)
 #;(define-type-constructor
   (μ [[tv]] τ_body))
-(define-syntax μ
+#;(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
+#;(begin-for-syntax
   (define-syntax ~μ*
     (pattern-expander
      (syntax-parser
diff --git a/tapl/stlc+reco+sub.rkt b/tapl/stlc+reco+sub.rkt
index eea9ded..62930f1 100644
--- a/tapl/stlc+reco+sub.rkt
+++ b/tapl/stlc+reco+sub.rkt
@@ -1,15 +1,16 @@
 #lang racket/base
 (require "typecheck.rkt")
-;; want to use type=? and eval-type from stlc+reco+var.rkt, not stlc+sub.rkt
-(require (except-in "stlc+sub.rkt" #%app #%datum sub? type=? type-eval)
-         (prefix-in stlc: (only-in "stlc+sub.rkt" #%app #%datum sub?))
+;;use type=? and eval-type from stlc+reco+var.rkt, not stlc+sub.rkt
+;; but extend sub? from stlc+sub.rkt
+(require (except-in "stlc+sub.rkt" #%app #%datum sub?)
+         (prefix-in stlc+sub: (only-in "stlc+sub.rkt" #%app #%datum sub?))
          (except-in "stlc+reco+var.rkt" #%app #%datum +)
-         (prefix-in var: (only-in "stlc+reco+var.rkt" #%datum)))
-(provide (rename-out [stlc:#%app #%app]
+         (prefix-in stlc+reco+var: (only-in "stlc+reco+var.rkt" #%datum)))
+(provide (rename-out [stlc+sub:#%app #%app]
                      [datum/tc #%datum]))
-(provide (except-out (all-from-out "stlc+sub.rkt") stlc:#%app stlc:#%datum
-                     (for-syntax stlc:sub?))
-         (except-out (all-from-out "stlc+reco+var.rkt") var:#%datum))
+(provide (except-out (all-from-out "stlc+sub.rkt") stlc+sub:#%app stlc+sub:#%datum
+                     (for-syntax stlc+sub:sub?))
+         (except-out (all-from-out "stlc+reco+var.rkt") stlc+reco+var:#%datum))
 (provide (for-syntax sub?))
 
 ;; Simply-Typed Lambda Calculus, plus subtyping, plus records
@@ -22,40 +23,34 @@
 
 (define-syntax (datum/tc stx)
   (syntax-parse stx
-    [(_ . n:number) #'(stlc:#%datum . n)]
-    [(_ . x) #'(var:#%datum . x)]))
+    [(_ . n:number) #'(stlc+sub:#%datum . n)]
+    [(_ . x) #'(stlc+reco+var:#%datum . x)]))
 
 (begin-for-syntax
   (define (sub? τ1 τ2)
+;    (printf "t1 = ~a\n" (syntax->datum τ1))
+;    (printf "t2 = ~a\n" (syntax->datum τ2))
     (or
-     (syntax-parse (list τ1 τ2) #:literals (quote)
-       [((~× [: 'k τk] ...) (~× [: 'l τl] ...))
-;       [(tup1 tup2)
-;        #:when (and (×? #'tup1) (×? #'tup2))
-;        #:with (['k:str τk] ...) (stx-map :-args (×-args #'tup1))
-;        #:with (['l:str τl] ...) (stx-map :-args (×-args #'tup2))
+     (syntax-parse (list τ1 τ2)
+       [((~× [k : τk] ...) (~× [l : τl] ...))
         #:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
                         (stx-map syntax-e (syntax->list #'(k ...))))
         (stx-andmap
          (syntax-parser
-           [(l:str τl)
-            #:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...))
-            ((current-sub?) #'τk_match #'τl)])
+           [(label τlabel)
+            #:with (k_match τk_match) (stx-assoc #'label #'([k τk] ...))
+            ((current-sub?) #'τk_match #'τlabel)])
          #'([l τl] ...))]
-       [((~∨ [<> 'k τk] ...) (~∨ [<> 'l τl] ...))
-;       [(var1 var2)
-;        #:when (and (∨? #'var1) (∨? #'var2))
-;        #:with (['k:str τk] ...) (stx-map :-args (∨-args #'var1))
-;        #:with (['l:str τl] ...) (stx-map :-args (∨-args #'var2))
+       [((~∨ [k : τk] ...) (~∨ [l : τl] ...))
         #:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
                         (stx-map syntax-e (syntax->list #'(k ...))))
         (stx-andmap
          (syntax-parser
-           [(l:str τl)
-            #:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...))
-            ((current-sub?) #'τk_match #'τl)])
+           [(label τlabel)
+            #:with (k_match τk_match) (stx-assoc #'label #'([k τk] ...))
+            ((current-sub?) #'τk_match #'τlabel)])
          #'([l τl] ...))]
        [_ #f])
-     (stlc:sub? τ1 τ2)))
+     (stlc+sub:sub? τ1 τ2)))
   (current-sub? sub?)
   (current-typecheck-relation (current-sub?)))
\ No newline at end of file
diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt
index 7715ae8..15515c9 100644
--- a/tapl/stlc+reco+var.rkt
+++ b/tapl/stlc+reco+var.rkt
@@ -1,15 +1,16 @@
 #lang racket/base
 (require "typecheck.rkt")
 (require (only-in racket/bool symbol=?))
-(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin let #;type=? × infer×+erase))
-         (except-in "stlc+tup.rkt" #%app begin tup proj let #;type=? × infer×+erase))
+(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin let × ×?))
+         (except-in "stlc+tup.rkt" #%app begin tup proj let ×)
+         (rename-in (only-in "stlc+tup.rkt" ~×)  [~× ~stlc:×]))
 (provide (rename-out [stlc:#%app #%app] [stlc:let let] [stlc:begin begin]
                      [define/tc define]))
 (provide (except-out (all-from-out "stlc+tup.rkt")
                      stlc:#%app stlc:let stlc:begin stlc:×
-                     (for-syntax #;stlc:type=? stlc:infer×+erase)))
-(provide tup proj × var case ∨)
-(provide (for-syntax #;type=? same-types?))
+                     (for-syntax ~stlc:× stlc:×?)))
+(provide × tup proj ∨ var case)
+(provide (for-syntax same-types? ~× ~×* ~∨ ~∨*))
 
 
 ;; Simply-Typed Lambda Calculus, plus records and variants
@@ -61,11 +62,29 @@
     [(_ [label:id : τ:type] ...)
      #:with (valid-τ ...) (stx-map mk-type #'(('label τ.norm) ...))
      #`(stlc:× valid-τ ...)]))
-(define-for-syntax (infer×+erase e)
-  (syntax-parse (stlc:infer×+erase e) #:context e
-    [(e- τ_e)
-     #:with (((~literal #%plain-app) (quote l) τ) ...) #'τ_e
-     #'(e- ((l τ) ...))]))
+(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 (:)
+       [(_ [l : τ_l] (~and ddd (~literal ...)))
+        #'(~stlc:× ((~literal #%plain-app) (quote l) τ_l) ddd)]
+       [(_ . args)
+        #'(~and (~stlc:× ((~literal #%plain-app) (quote l) τ_l) (... ...))
+                (~parse args #'((l τ_l) (... ...))))])))
+  (define ×? stlc:×?)
+  (define-syntax ~×*
+    (pattern-expander
+     (syntax-parser #:datum-literals (:)
+       [(_ [l : τ_l] (~and ddd (~literal ...)))
+        #'(~or (~× [l : τ_l] ddd)
+               (~and any (~do (type-error
+                               #:src #'any
+                               #:msg "Expected × type, got: ~a" #'any))))]))))
 
 #;(define-type-constructor
   ;(× [~× label τ_fld] ...) #:lits (~×)
@@ -89,7 +108,8 @@
   (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_τ τ] ...)) (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)
@@ -112,7 +132,7 @@
                         "Improper usage of type constructor ∨: ~a, expected (∨ [label:id : τ:type] ...+)")
                  #'any)]))
 (begin-for-syntax
-  (define (infer∨+erase e)
+  #;(define (infer∨+erase e)
     (syntax-parse (infer+erase e) #:context e
       [(e- τ_e)
        #:fail-unless (∨/internal? #'τ_e)
@@ -122,14 +142,24 @@
         (syntax->datum e) (type->str #'τ_e))
        #:with (~∨/internal ((~literal #%plain-app) (quote l) τ) ...) #'τ_e
        #'(e- ((l τ) ...))]))
+  (define ∨? ∨/internal?)
+  (define-syntax ~∨
+    (pattern-expander
+     (syntax-parser #:datum-literals (:)
+      [(_ [l : τ_l] (~and ddd (~literal ...)))
+       #'(~∨/internal ((~literal #%plain-app) (quote l) τ_l) ddd)]
+      [(_ . args)
+        #'(~and (~∨/internal ((~literal #%plain-app) (quote l) τ_l) (... ...))
+                (~parse args #'((l τ_l) (... ...))))])))
   (define-syntax ~∨*
     (pattern-expander
      (syntax-parser #:datum-literals (:)
       [(_ [l : τ_l] (~and ddd (~literal ...)))
-       #'(~or (~∨/internal ((~literal #%plain-app) (quote l) τ_l) ddd)
-              (~and any (~do (type-error
-                              #:src #'any
-                              #:msg "Expected ∨ type, got: ~a" #'any))))]))))
+       #'(~and (~or (~∨ [l : τ_l] ddd)
+                    (~and any (~do (type-error
+                                    #:src #'any
+                                    #:msg "Expected ∨ type, got: ~a" #'any))))
+               ~!)])))) ; dont backtrack here
 
 #;(define-type-constructor
   (∨ [<> label τ_var] ...) #:lits (<>)
@@ -141,10 +171,16 @@
     [(_ 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) (stx-assoc #'l #'((l_τ τ_l) ...))
+     #:with match_res (stx-assoc #'l #'((l_τ τ_l) ...))
+     #:fail-unless (syntax-e #'match_res)
+                   (format "~a field does not exist" (syntax->datum #'l))
+     #:with (_ τ_match) #'match_res
      #:with (e- τ_e) (infer+erase #'e)
      #:when (typecheck? #'τ_e #'τ_match)
      (⊢ (list 'l e) : τ)]))
@@ -153,7 +189,8 @@
     [(_ 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] ...)) (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"
diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
index b6240de..7818d96 100644
--- a/tapl/stlc+sub.rkt
+++ b/tapl/stlc+sub.rkt
@@ -37,7 +37,7 @@
     [(_ . x) #'(stlc:#%datum . x)]))
 
 (begin-for-syntax
-  (define (sub? τ1 τ2)
+  (define (sub? t1 t2)
     ; only need this because recursive calls made with unexpanded types
     (define τ1 ((current-type-eval) t1))
     (define τ2 ((current-type-eval) t2))
diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt
index 9601110..3b044b3 100644
--- a/tapl/stlc+tup.rkt
+++ b/tapl/stlc+tup.rkt
@@ -25,7 +25,8 @@
 (define-syntax (proj stx)
   (syntax-parse stx
     [(_ e_tup n:nat)
-     #:with [e_tup- τs_tup] (infer×+erase #'e_tup)
+;     #:with [e_tup- τs_tup] (infer×+erase #'e_tup)
+     #:with [e_tup- τs_tup] (⇑ e_tup as ×)
      #:fail-unless (< (syntax-e #'n) (stx-length #'τs_tup)) "index too large"
      (⊢ (list-ref e_tup- n) : #,(stx-list-ref #'τs_tup (syntax-e #'n)))]))
    
\ No newline at end of file
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
index 52eda68..82604e1 100644
--- a/tapl/stlc.rkt
+++ b/tapl/stlc.rkt
@@ -21,7 +21,7 @@
   ;;   - may require some caution when mixing expanded and unexpanded types to
   ;;     create other types
   (define (type-eval τ)
-    (or (plain-type? τ) ; don't expand if already expanded
+    (or (expanded-type? τ) ; don't expand if already expanded
         (add-orig (expand/df τ) τ)))
   
   (current-type-eval type-eval)
@@ -67,7 +67,7 @@
      ;#:with [e_fn- τ_fn] (infer+erase #'e_fn) ; #2 get, via (internal) pattern expander
      ;#:with (τ_in ...) (→-get τ_in from #'τ_fn)
      ;#:with τ_out (→-get τ_out from #'τ_fn)
-     #:with [e_fn- (τ_in ... τ_out)] (infer→+erase #'e_fn) ; #3 work directly on term -- better err msg
+     #:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn as →) ; #3 work directly on term -- better err msg
      #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
      #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
                    (string-append
diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt
index 35c34b3..1d1697b 100644
--- a/tapl/sysf.rkt
+++ b/tapl/sysf.rkt
@@ -1,12 +1,12 @@
 #lang racket/base
 (require "typecheck.rkt")
 (require (except-in "stlc+lit.rkt" #%app λ type=?)
-         (prefix-in stlc: (only-in "stlc+lit.rkt" #%app λ type=?)))
+         (prefix-in stlc: (only-in "stlc+lit.rkt" #%app λ))
+         (only-in "stlc+rec-iso.rkt" type=?))
 (provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
-(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app
-                     (for-syntax stlc:type=?)))
-(provide Λ inst)
-(provide (for-syntax type=?))
+(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app stlc:λ)
+         (all-from-out "stlc+rec-iso.rkt")) ; type=?
+(provide ∀ Λ inst)
 
  
 ;; System F
@@ -26,11 +26,36 @@
     [(_ (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-type-constructor (∀ [[x ...]] body))
 
-(begin-for-syntax
+(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)
+  #;(define (type=? τ1 τ2)
     (syntax-parse (list τ1 τ2)
       [(((~literal #%plain-lambda) (x:id ...) k1 ... t1)
         ((~literal #%plain-lambda) (y:id ...) k2 ... t2))
@@ -45,12 +70,12 @@
 (define-syntax (Λ stx)
   (syntax-parse stx
     [(_ (tv:id ...) e)
-     #:with ((tv- ...) e- τ) (infer/tvs+erase #'e #'(tv ...))
-     (⊢ e- : (∀ #:bind (tv- ...) τ))]))
+     #:with ((tv- ...) e- τ) (infer/tyctx+erase #'([tv : #%type] ...) #'e)
+     (⊢ e- : (∀ (tv- ...) τ))]))
 (define-syntax (inst stx)
   (syntax-parse stx
     [(_ e τ:type ...)
-     #:with (e- (~∀* [[tv ...]] τ_body)) (infer+erase #'e)
+     #:with (e- (~∀* (tv ...) τ_body)) (infer+erase #'e)
 ;     #:with (e- ∀τ) (infer+erase #'e)
 ;     #:with ((~literal #%plain-lambda) (tv ...) τ_body) #'∀τ
      (⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
\ No newline at end of file
diff --git a/tapl/tests/ext-stlc-tests.rkt b/tapl/tests/ext-stlc-tests.rkt
index 7acfc3a..d1eefc1 100644
--- a/tapl/tests/ext-stlc-tests.rkt
+++ b/tapl/tests/ext-stlc-tests.rkt
@@ -29,7 +29,7 @@
 (typecheck-fail (begin) #:with-msg "expected more terms")
 (typecheck-fail
  (begin 1 2 3)
- #:with-msg "Expected expression 1 to have type Unit, got: Int")
+ #:with-msg "Expected expression 1 to have Unit type, got: Int")
 
 (check-type (begin (void) 1) : Int ⇒ 1)
 (check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int)
@@ -101,23 +101,23 @@
 ;; check some more err msgs
 (typecheck-fail
  (and "1" #f)
- #:with-msg "Expected expression \"1\" to have type Bool, got: String")
+ #:with-msg "Expected expression \"1\" to have Bool type, got: String")
 (typecheck-fail
  (and #t "2")
  #:with-msg
- "Expected expression \"2\" to have type Bool, got: String")
+ "Expected expression \"2\" to have Bool type, got: String")
 (typecheck-fail
  (or "1" #f)
  #:with-msg
- "Expected expression \"1\" to have type Bool, got: String")
+ "Expected expression \"1\" to have Bool type, got: String")
 (typecheck-fail
  (or #t "2")
  #:with-msg
- "Expected expression \"2\" to have type Bool, got: String")
+ "Expected expression \"2\" to have Bool type, got: String")
 (typecheck-fail
  (if "true" 1 2)
  #:with-msg
- "Expected expression \"true\" to have type Bool, got: String")
+ "Expected expression \"true\" to have Bool type, got: String")
 (typecheck-fail
  (if #t 1 "2")
  #:with-msg 
diff --git a/tapl/tests/fomega-tests.rkt b/tapl/tests/fomega-tests.rkt
index b610da3..0be1146 100644
--- a/tapl/tests/fomega-tests.rkt
+++ b/tapl/tests/fomega-tests.rkt
@@ -1,191 +1,198 @@
 #lang s-exp "../fomega.rkt"
 (require "rackunit-typechecking.rkt")
 
-;(check-type Int : ★)
-;(check-type String : ★)
-;(typecheck-fail →)
-;(check-type (→ Int Int) : ★)
-;(typecheck-fail (→ →))
-;(typecheck-fail (→ 1))
-;(check-type 1 : Int)
-;
-;(check-type (∀ ([t : ★]) (→ t t)) : ★)
-;(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
+(check-type Int : ★)
+(check-type String : ★)
+(typecheck-fail →)
+(check-type (→ Int Int) : ★)
+(typecheck-fail (→ →))
+(typecheck-fail (→ 1))
+(check-type 1 : Int)
 
-(Λ ([X : ★]) (λ ([x : X]) x))
+(check-type (∀ ([t : ★]) (→ t t)) : ★)
+(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
 
-#;(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+
+(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
             : (∀ ([X : ★]) (→ X X)))
-;(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (⇒ ★ ★)]) (λ ([x : X]) x))))
+(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")
 
-;(check-type (tyλ ([t : ★]) t) : (⇒ ★ ★))
-;(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★))
-;(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★)))
-;(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★)))
-;(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
-;(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★))
-;
-;(check-type (tyapp (tyλ ([t : ★]) t) Int) : ★)
-;(check-type (λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) : (→ Int Int))
-;(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
-;(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
-;(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
-;(typecheck-fail ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
-;
-;;; partial-apply →
-;(check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)
-;            : (⇒ ★ ★))
-;; f's type must have kind ★
-;(typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f))
-;(check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) :
-;            (∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String))))
-;(check-type (inst
-;             (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
-;             (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
-;            : (→ (→ Int String) (→ Int String)))
-;;; applied f too early
-;(typecheck-fail (inst
-;                 (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
-;                 (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)))
-;(check-type ((inst
-;              (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
-;              (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
-;             (λ ([x : Int]) "int")) : (→ Int String))
-;(check-type (((inst
-;               (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
-;              (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
-;              (λ ([x : Int]) "int")) 1) : String ⇒ "int")
-;
 ;; tapl examples, p441
-;(define-type-alias Id (tyλ ([X : ★]) X))
-;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
-;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int))
-;(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int))
-;(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int (tyapp Id String)) Int))
-;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) (tyapp Id String)) Int))
-;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) String) Int))
-;(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (→ Int String) Int))
-;(check-type (λ ([f : (→ Int String)]) 1) : (→ (tyapp Id (→ Int String)) Int))
-;(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (→ Int String)) Int))
-;(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int))
-;
+(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)
+(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/fomega2-tests.rkt b/tapl/tests/fomega2-tests.rkt
index 4211059..2123cda 100644
--- a/tapl/tests/fomega2-tests.rkt
+++ b/tapl/tests/fomega2-tests.rkt
@@ -6,14 +6,17 @@
 (typecheck-fail →)
 (check-type (→ Int Int) : ★)
 (typecheck-fail (→ →))
+(typecheck-fail (→ 1))
 (check-type 1 : Int)
 
 (check-type (∀ ([t : ★]) (→ t t)) : ★)
 (check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
 
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+
 (check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
-            : (∀ ([X : ★]) (→ X X )))
-(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (⇒ ★ ★)]) (λ ([x : X]) x))))
+            : (∀ ([X : ★]) (→ X X)))
+(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (→ ★ ★)]) (λ ([x : X]) x))))
 
 (check-type (λ ([t : ★]) t) : (→ ★ ★))
 (check-type (λ ([t : ★] [s : ★]) t) : (→ ★ ★ ★))
@@ -40,9 +43,13 @@
              (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
              ((λ ([arg : ★]) (λ ([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
-                 (Λ ([yf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
+                 (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
                  ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)))
 (check-type ((inst
               (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
@@ -53,7 +60,10 @@
               ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
               (λ ([x : Int]) "int")) 1) : String ⇒ "int")
 
-; tapl examples, p441
+;; tapl examples, p441
+(typecheck-fail
+ (define-type-alias tmp 1)
+ #:with-msg "not a valid type: 1")
 (define-type-alias Id (λ ([X : ★]) X))
 (check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
 (check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (Id String)) Int))
@@ -66,13 +76,13 @@
 (check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (→ Int String)) Int))
 (check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (Id (→ Int String))) Int))
 
-; tapl examples, p451
+;; tapl examples, p451
 (define-type-alias Pair (λ ([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
+; parametric pair constructor
 (check-type
  (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
  : (∀ ([X : ★][Y : ★]) (→ X Y (Pair X Y))))
diff --git a/tapl/tests/fsub-tests.rkt b/tapl/tests/fsub-tests.rkt
index 046c5f9..6d927a4 100644
--- a/tapl/tests/fsub-tests.rkt
+++ b/tapl/tests/fsub-tests.rkt
@@ -3,64 +3,65 @@
 
 ;; examples from tapl ch26, bounded quantification
 ;; (same tests from stlc+reco+sub.rkt, but last one should not typecheck)
-(check-type (λ ([x : (× [: "a" Int])]) x) : (→ (× [: "a" Int]) (× [: "a" Int])))
+(check-type (λ ([x : (× [a : Int])]) x) : (→ (× [a : Int]) (× [a : Int])))
 
-(define ra (tup ["a" = 0]))
-(check-type ((λ ([x : (× [: "a" Int])]) x) ra)
-            : (× [: "a" Int]) ⇒ (tup ["a" = 0]))
-(define rab (tup ["a" = 0]["b" = #t]))
-(check-type ((λ ([x : (× [: "a" Int])]) x) rab)
-            : (× [: "a" Int]) ⇒ (tup ["a" = 0]["b" = #t]))
+(define ra (tup [a = 0]))
+(check-type ((λ ([x : (× [a : Int])]) x) ra)
+            : (× [a : Int]) ⇒ (tup [a = 0]))
+(define rab (tup [a = 0][b = #t]))
+(check-type ((λ ([x : (× [a : Int])]) x) rab)
+            : (× [a : Int]) ⇒ (tup [a = 0][b = #t]))
 
-(check-type (proj ((λ ([x : (× [: "a" Int])]) x) rab) "a")
+(check-type (proj ((λ ([x : (× [a : Int])]) x) rab) a)
             : Int ⇒ 0)
 
-(check-type (proj ((inst (Λ (X) (λ ([x : X]) x))
-                         (× [: "a" Int][: "b" Bool]))
-                   rab) "b")
+(check-type (proj ((inst (Λ ([X <: Top]) (λ ([x : X]) x))
+                         (× [a : Int][b : Bool]))
+                   rab) b)
             : Bool ⇒ #t)
 
-(define f2 (λ ([x : (× [: "a" Nat])]) (tup ["orig" = x] ["asucc" = (+ 1 (proj x "a"))])))
-(check-type f2 : (→ (× [: "a" Nat]) (× [: "orig" (× [: "a" Nat])] [: "asucc" Nat])))
-(check-type (f2 ra) : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat]))
-(check-type (f2 rab) : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat]))
+(define f2 (λ ([x : (× [a : Nat])]) (tup [orig = x] [asucc = (+ 1 (proj x a))])))
+(check-type f2 : (→ (× [a : Nat]) (× [orig : (× [a : Nat])] [asucc : Nat])))
+(check-type (f2 ra) : (× [orig : (× [a : Nat])][asucc : Nat]))
+(check-type (f2 rab) : (× [orig : (× [a : Nat])][asucc : Nat]))
 
-;; define-primop (actually #%app) needs to call current-promote
+; check expose properly called for primops
 (define fNat (Λ ([X <: Nat]) (λ ([x : X]) (+ x 1))))
 (check-type fNat : (∀ ([X <: Nat]) (→ X Nat)))
 
+; check type constructors properly call expose
 (define f2poly
-  (Λ ([X <: (× [: "a" Nat])])
+  (Λ ([X <: (× [a : Nat])])
      (λ ([x : X])
-       (tup ["orig" = x]["asucc" = (+ (proj x "a") 1)]))))
+       (tup [orig = x][asucc = (+ (proj x a) 1)]))))
 
-(check-type f2poly : (∀ ([X <: (× [: "a" Nat])]) (→ X (× [: "orig" X][: "asucc" Nat]))))
+(check-type f2poly : (∀ ([X <: (× [a : Nat])]) (→ X (× [orig : X][asucc : Nat]))))
 
-;; inst f2poly with (× [: "a" Nat])
-(check-type (inst f2poly (× [: "a" Nat]))
-            : (→ (× [: "a" Nat])
-                 (× [: "orig" (× [: "a" Nat])][: "asucc" Nat])))
-(check-type ((inst f2poly (× [: "a" Nat])) ra)
-            : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat])
-            ⇒ (tup ["orig" = ra]["asucc" = 1]))
+; inst f2poly with (× [a : Nat])
+(check-type (inst f2poly (× [a : Nat]))
+            : (→ (× [a : Nat])
+                 (× [orig : (× [a : Nat])][asucc : Nat])))
+(check-type ((inst f2poly (× [a : Nat])) ra)
+            : (× [orig : (× [a : Nat])][asucc : Nat])
+            ⇒ (tup [orig = ra][asucc = 1]))
 
-(check-type ((inst f2poly (× [: "a" Nat])) rab)
-            : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat])
-            ⇒ (tup ["orig" = rab]["asucc" = 1]))
+(check-type ((inst f2poly (× [a : Nat])) rab)
+            : (× [orig : (× [a : Nat])][asucc : Nat])
+            ⇒ (tup [orig = rab][asucc = 1]))
 
-(typecheck-fail (proj (proj ((inst f2poly (× [: "a" Nat])) rab) "orig") "b"))
+(typecheck-fail (proj (proj ((inst f2poly (× [a : Nat])) rab) orig) b))
 
-;; inst f2poly with (× [: "a" Nat][: "b" Bool])
-(check-type (inst f2poly (× [: "a" Nat][: "b" Bool]))
-            : (→ (× [: "a" Nat][: "b" Bool])
-                 (× [: "orig" (× [: "a" Nat][: "b" Bool])][: "asucc" Nat])))
-(typecheck-fail ((inst f2poly (× [: "a" Nat][: "b" Bool])) ra))
+;; inst f2poly with (× [a : Nat][b : Bool])
+(check-type (inst f2poly (× [a : Nat][b : Bool]))
+            : (→ (× [a : Nat][b : Bool])
+                 (× [orig : (× [a : Nat][b : Bool])][asucc : Nat])))
+(typecheck-fail ((inst f2poly (× [a : Nat][b : Bool])) ra))
 
-(check-type ((inst f2poly (× [: "a" Nat][: "b" Bool])) rab)
-            : (× [: "orig" (× [: "a" Nat][: "b" Bool])][: "asucc" Nat])
-            ⇒ (tup ["orig" = rab]["asucc" = 1]))
+(check-type ((inst f2poly (× [a : Nat][b : Bool])) rab)
+            : (× [orig : (× [a : Nat][b : Bool])][asucc : Nat])
+            ⇒ (tup [orig = rab][asucc = 1]))
 
-(check-type (proj (proj ((inst f2poly (× [: "a" Nat][: "b" Bool])) rab) "orig") "b")
+(check-type (proj (proj ((inst f2poly (× [a : Nat][b : Bool])) rab) orig) b)
             : Bool ⇒ #t)
 
 ;; make sure inst still checks args
@@ -78,49 +79,50 @@
 
 
 ;; old sysf tests -------------------------------------------------------------
-(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)
+;; old syntax no longer valid
+;(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 -------------------------------------------------------------
diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt
index 76474dd..38f03f2 100644
--- a/tapl/tests/rackunit-typechecking.rkt
+++ b/tapl/tests/rackunit-typechecking.rkt
@@ -5,9 +5,9 @@
 (define-syntax (check-type stx)
   (syntax-parse stx #:datum-literals (: ⇒)
     [(_ e : τ ⇒ v) #'(check-type-and-result e : τ ⇒ v)]
-    [(_ e : τ-expected:type)
+    [(_ e : τ-expected)
      #:with τ (typeof (expand/df #'e))
-     #:fail-unless (typecheck? #'τ #'τ-expected.norm)
+     #:fail-unless (typecheck? #'τ ((current-type-eval) #'τ-expected))
      (format
       "Expression ~a [loc ~a:~a] has type ~a, expected ~a"
       (syntax->datum #'e) (syntax-line #'e) (syntax-column #'e)
@@ -16,9 +16,9 @@
 
 (define-syntax (check-not-type stx)
   (syntax-parse stx #:datum-literals (:)
-    [(_ e : not-τ:type)
+    [(_ e : not-τ)
      #:with τ (typeof (expand/df #'e))
-     #:fail-when (typecheck? #'τ #'not-τ.norm)
+     #:fail-when (typecheck? #'τ ((current-type-eval) #'not-τ))
      (format
       "(~a:~a) Expression ~a should not have type ~a"
       (syntax-line stx) (syntax-column stx)
diff --git a/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
index 8618c91..8ee98bd 100644
--- a/tapl/tests/run-all-tests.rkt
+++ b/tapl/tests/run-all-tests.rkt
@@ -15,12 +15,13 @@
 
 ;; subtyping
 (require "stlc+sub-tests.rkt")
-;(require "stlc+reco+sub-tests.rkt")
-;;(require "fsub-tests.rkt")
-;
-;;; system F
-;(require "sysf-tests.rkt")
+(require "stlc+reco+sub-tests.rkt")
+
+;; system F
+(require "sysf-tests.rkt")
+
+(require "fsub-tests.rkt") ; sysf + reco-sub
 
 ;;; F_omega
-;(require "fomega-tests.rkt")
-;(require "fomega2-tests.rkt")
\ No newline at end of file
+(require "fomega-tests.rkt")
+(require "fomega2-tests.rkt")
\ No newline at end of file
diff --git a/tapl/tests/stlc+reco+sub-tests.rkt b/tapl/tests/stlc+reco+sub-tests.rkt
index 6d4325a..8857170 100644
--- a/tapl/tests/stlc+reco+sub-tests.rkt
+++ b/tapl/tests/stlc+reco+sub-tests.rkt
@@ -3,57 +3,61 @@
 
 ;; record subtyping tests
 (check-type "coffee" : String)
-(check-type (tup ["coffee" = 3]) : (× [: "coffee" Int])) ; element subtyping
-(check-type (var "coffee" = 3 as (∨ [<> "coffee" Nat])) : (∨ [<> "coffee" Int])) ; element subtyping
-(check-type (tup ["coffee" = 3]) : (× [: "coffee" Nat]))
-(check-type (tup ["coffee" = 3]) : (× [: "coffee" Top]))
-(check-type (var "coffee" = 3 as (∨ [<> "coffee" Int])) : (∨ [<> "coffee" Top])) ; element subtyping (twice)
-(check-type (tup ["coffee" = 3]) : (× [: "coffee" Num]))
-(check-not-type (tup ["coffee" = -3]) : (× [: "coffee" Nat]))
-(check-type (tup ["coffee" = -3]) : (× [: "coffee" Num]))
-(check-type (tup ["coffee" = -3] ["tea" = 3]) : (× [: "coffee" Int])) ; width subtyping
-(check-type (tup ["coffee" = -3] ["tea" = 3]) : (× [: "coffee" Num])) ; width+element subtyping
+(check-type (tup [coffee = 3]) : (× [coffee : Int])) ; element subtyping
+(check-type (var coffee = 3 as (∨ [coffee : Nat])) : (∨ [coffee : Int])) ; element subtyping
+;err
+(typecheck-fail
+ (var cooffee = 3 as (∨ [coffee : Nat]))
+ #:with-msg "cooffee field does not exist")
+(check-type (tup [coffee = 3]) : (× [coffee : Nat]))
+(check-type (tup [coffee = 3]) : (× [coffee : Top]))
+(check-type (var coffee = 3 as (∨ [coffee : Int])) : (∨ [coffee : Top])) ; element subtyping (twice)
+(check-type (tup [coffee = 3]) : (× [coffee : Num]))
+(check-not-type (tup [coffee = -3]) : (× [coffee : Nat]))
+(check-type (tup [coffee = -3]) : (× [coffee : Num]))
+(check-type (tup [coffee = -3] [tea = 3]) : (× [coffee : Int])) ; width subtyping
+(check-type (tup [coffee = -3] [tea = 3]) : (× [coffee : Num])) ; width+element subtyping
 
 ;; record + fns
-(check-type (tup ["plus" = +]) : (× [: "plus" (→ Num Num Num)]))
+(check-type (tup [plus = +]) : (× [plus : (→ Num Num Num)]))
 (check-type + : (→ Num Num Num))
-(check-type (tup ["plus" = +]) : (× [: "plus" (→ Int Num Num)]))
-(check-type (tup ["plus" = +]) : (× [: "plus" (→ Int Num Top)]))
-(check-type (tup ["plus" = +] ["mul" = *]) : (× [: "plus" (→ Int Num Top)]))
+(check-type (tup [plus = +]) : (× [plus : (→ Int Num Num)]))
+(check-type (tup [plus = +]) : (× [plus : (→ Int Num Top)]))
+(check-type (tup [plus = +] [mul = *]) : (× [plus : (→ Int Num Top)]))
 
 ;; examples from tapl ch26, bounded quantification
-(check-type (λ ([x : (× [: "a" Int])]) x) : (→ (× [: "a" Int]) (× [: "a" Int])))
+(check-type (λ ([x : (× [a : Int])]) x) : (→ (× [a : Int]) (× [a : Int])))
 
-(check-type ((λ ([x : (× [: "a" Int])]) x) (tup ["a" = 0]))
-            : (× [: "a" Int]) ⇒ (tup ["a" = 0]))
-(check-type ((λ ([x : (× [: "a" Int])]) x) (tup ["a" = 0]["b" = #t]))
-            : (× [: "a" Int]) ⇒ (tup ["a" = 0]["b" = #t]))
+(check-type ((λ ([x : (× [a : Int])]) x) (tup [a = 0]))
+            : (× [a : Int]) ⇒ (tup [a = 0]))
+(check-type ((λ ([x : (× [a : Int])]) x) (tup [a = 0][b = #t]))
+            : (× [a : Int]) ⇒ (tup [a = 0][b = #t]))
 
-(check-type (proj ((λ ([x : (× [: "a" Int])]) x) (tup ["a" = 0]["b" = #t])) "a")
+(check-type (proj ((λ ([x : (× [a : Int])]) x) (tup [a = 0][b = #t])) a)
             : Int ⇒ 0)
 
 ;; this should work! but needs bounded quantification, see fsub.rkt
-(typecheck-fail (proj ((λ ([x : (× [: "a" Int])]) x) (tup ["a" = 0]["b" = #t])) "b"))
+(typecheck-fail (proj ((λ ([x : (× [a : Int])]) x) (tup [a = 0][b = #t])) b))
 
 ;; previous record tests ------------------------------------------------------
 ;; records (ie labeled tuples)
 (check-type "Stephen" : String)
-(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-            (× [: "name" String] [: "phone" Int] [: "male?" Bool]))
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(check-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+            (× [name : String] [phone : Int] [male? : Bool]))
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
             : String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
             : String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone)
             : Int ⇒ 781)
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) male?)
             : Bool ⇒ #t)
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-                (× [: "my-name" String] [: "phone" Int] [: "male?" Bool]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-                (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
-                (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [my-name : String] [phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [name : String] [my-phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [name : String] [phone : Int] [is-male? : Bool]))
 
 
 ;; previous basic subtyping tests ------------------------------------------------------
diff --git a/tapl/tests/sysf-tests.rkt b/tapl/tests/sysf-tests.rkt
index d76da29..470f0e5 100644
--- a/tapl/tests/sysf-tests.rkt
+++ b/tapl/tests/sysf-tests.rkt
@@ -1,20 +1,20 @@
 #lang s-exp "../sysf.rkt"
 (require "rackunit-typechecking.rkt")
 
-(check-type (Λ (X) (λ ([x : X]) x)) : (∀ [[X]] (→ X X)))
+(check-type (Λ (X) (λ ([x : X]) x)) : (∀ (X) (→ X X)))
 
-(check-type (Λ (X) (λ ([t : X] [f : X]) t)) : (∀ [[X]] (→ X X X))) ; true
-(check-type (Λ (X) (λ ([t : X] [f : X]) f)) : (∀ [[X]] (→ X X X))) ; false
-(check-type (Λ (X) (λ ([t : X] [f : X]) f)) : (∀ [[Y]] (→ Y Y Y))) ; false, alpha equiv
+(check-type (Λ (X) (λ ([t : X] [f : X]) t)) : (∀ (X) (→ X X X))) ; true
+(check-type (Λ (X) (λ ([t : X] [f : X]) f)) : (∀ (X) (→ X X X))) ; false
+(check-type (Λ (X) (λ ([t : X] [f : X]) f)) : (∀ (Y) (→ Y Y Y))) ; false, alpha equiv
 
 (check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ [[t1]] (∀ [[t2]] (→ t1 (→ t2 t2)))))
+            : (∀ (t1) (∀ (t2) (→ t1 (→ t2 t2)))))
 
 (check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ [[t3]] (∀ [[t4]] (→ t3 (→ t4 t4)))))
+            : (∀ (t3) (∀ (t4) (→ t3 (→ t4 t4)))))
 
 (check-not-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ [[t4]] (∀ [[t3]] (→ t3 (→ t4 t4)))))
+            : (∀ (t4) (∀ (t3) (→ t3 (→ t4 t4)))))
 
 (check-type (inst (Λ (t) (λ ([x : t]) x)) Int) : (→ Int Int))
 (check-type (inst (Λ (t) 1) (→ Int Int)) : Int)
@@ -30,27 +30,29 @@
  "Expected type of expression to match pattern \\(∀ \\(\\(x ...)) body), got: Int")
 
 ;; polymorphic arguments
-(check-type (Λ (t) (λ ([x : t]) x)) : (∀ [[t]] (→ t t)))
-(check-type (Λ (t) (λ ([x : t]) x)) : (∀ [[s]] (→ s s)))
-(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ [[s]] (∀ [[t]] (→ t t))))
-(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ [[r]] (∀ [[t]] (→ t t))))
-(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ [[r]] (∀ [[s]] (→ s s))))
-(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ [[r]] (∀ [[u]] (→ u u))))
-(check-type (λ ([x : (∀ [[t]] (→ t t))]) x) : (→ (∀ [[s]] (→ s s)) (∀ [[u]] (→ u u))))
-(typecheck-fail ((λ ([x : (∀ [[t]] (→ t t))]) x) (λ ([x : Int]) x)))
-(typecheck-fail ((λ ([x : (∀ [[t]] (→ t t))]) x) 1))
-(check-type ((λ ([x : (∀ [[t]] (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) : (∀ [[u]] (→ u u)))
+(check-type (Λ (t) (λ ([x : t]) x)) : (∀ (t) (→ t t)))
+(check-type (Λ (t) (λ ([x : t]) x)) : (∀ (s) (→ s s)))
+(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (s) (∀ (t) (→ t t))))
+(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (t) (→ t t))))
+(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (s) (→ s s))))
+(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (u) (→ u u))))
+(check-type (λ ([x : (∀ (t) (→ t t))]) x) : (→ (∀ (s) (→ s s)) (∀ (u) (→ u u))))
+(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
+(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
+(check-type ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) : (∀ (u) (→ u u)))
 (check-type
- (inst ((λ ([x : (∀ [[t]] (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) : (→ Int Int))
+ (inst ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) : (→ Int Int))
 (check-type
- ((inst ((λ ([x : (∀ [[t]] (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) 10)
+ ((inst ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) 10)
  : Int ⇒ 10)
-(check-type (λ ([x : (∀ [[t]] (→ t t))]) (inst x Int)) : (→ (∀ [[t]] (→ t t)) (→ Int Int)))
-(check-type (λ ([x : (∀ [[t]] (→ t t))]) ((inst x Int) 10)) : (→ (∀ [[t]] (→ t t)) Int))
-(check-type ((λ ([x : (∀ [[t]] (→ t t))]) ((inst x Int) 10))
+(check-type (λ ([x : (∀ (t) (→ t t))]) (inst x Int)) : (→ (∀ (t) (→ t t)) (→ Int Int)))
+(check-type (λ ([x : (∀ (t) (→ t t))]) ((inst x Int) 10)) : (→ (∀ (t) (→ t t)) Int))
+(check-type ((λ ([x : (∀ (t) (→ t t))]) ((inst x Int) 10))
              (Λ (s) (λ ([y : s]) y)))
              : Int ⇒ 10)
 
+; ∀ errs
+(typecheck-fail (λ ([x : (∀ (y) (+ 1 y))]) x))
 
 ;; previous tests -------------------------------------------------------------
 (check-type 1 : Int)
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index ee7629d..56c7e44 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -74,7 +74,53 @@
   ;; typeof : Syntax -> Type or #f
   ;; Retrieves type of given stx, or #f if input has not been assigned a type.
   (define (typeof stx #:tag [tag 'type]) (syntax-property stx tag))
-  
+
+  (define-syntax (⇑ stx)
+    (syntax-parse stx #:datum-literals (as)
+      [(_ e as tycon)
+       #:with τ? (mk-? #'tycon)
+       #:with τ-get (format-id #'tycon "~a-get" #'tycon)
+       #:with τ-expander (format-id #'tycon "~~~a" #'tycon)
+       #'(syntax-parse (infer+erase #'e) #:context #'e
+           [(e- τ_e_)
+            #:with τ_e ((current-promote) #'τ_e_)
+            #:fail-unless (τ? #'τ_e)
+            (format
+             "~a (~a:~a): Expected expression ~s to have ~a type, got: ~a"
+             (syntax-source #'e) (syntax-line #'e) (syntax-column #'e)
+             (syntax->datum #'e) 'tycon (type->str #'τ_e))
+            ;#:with args (τ-get #'τ_e)
+            (if (stx-pair? #'τ_e)
+                (syntax-parse #'τ_e
+                 [(τ-expander . args) #'(e- args)])
+                #'e-)])]))
+  (define-syntax (⇑s stx)
+    (syntax-parse stx #:datum-literals (as)
+      [(_ es as tycon)
+       #:with τ? (mk-? #'tycon)
+       #:with τ-get (format-id #'tycon "~a-get" #'tycon)
+       #:with τ-expander (format-id #'tycon "~~~a" #'tycon)
+       #'(syntax-parse (stx-map infer+erase #'es) #:context #'es
+           [((e- τ_e_) (... ...))
+            #:with (τ_e (... ...)) (stx-map (current-promote) #'(τ_e_ (... ...)))
+            #:when (stx-andmap
+                    (λ (e t)
+                      (or (τ? t)
+                          (type-error #:src e
+                                      #:msg "Expected expression ~a to have ~a type, got: ~a"
+                                      e (quote-syntax tycon) t)))
+                    #'es
+                    #'(τ_e (... ...)))
+            ;#:with args (τ-get #'τ_e)
+            #:with res
+            (stx-map (λ (e t)
+                       (if (stx-pair? t)
+                           (syntax-parse t
+                             [(τ-expander . args) #`(#,e #'args)])
+                           e))
+                     #'(e- (... ...))
+                     #'(τ_e (... ...)))
+            #'res])]))
   ;; infers the type and erases types in an expression
   (define (infer+erase e)
     (define e+ (expand/df e))
@@ -89,10 +135,11 @@
   ;; expanded before wrapping in lambda
   ;; - This caused one problem in fomega2.rkt #%app, but I just had to expand
   ;; the types before typechecking, which is acceptable
-  (define (infer es #:ctx [ctx null] #:tvctx [tvctx null] #:tag [tag 'type])
+  (define (infer es #:ctx [ctx null] #:tvctx [tvctx null] #:octx [octx tvctx] #:tag [tag 'unused])
     (syntax-parse ctx #:datum-literals (:)
       [([x : τ] ...) ; dont expand yet bc τ may have references to tvs
        #:with ([tv : k] ...) tvctx
+       #:with ([_ : ok] ...) octx
        #:with (e ...) es
        #:with
        ; old expander pattern
@@ -108,13 +155,15 @@
          ((~literal #%expression)
           ((~literal #%plain-lambda) xs+
            ((~literal let-values) () ((~literal let-values) ()
-            ((~literal #%expression) e+) ...)))))))
+            ((~literal #%expression) e+) ... (~literal void))))))))
        (expand/df
         #`(λ (tv ...)
-            (let-syntax ([tv (make-rename-transformer (assign-type #'tv #'k #:tag '#,tag))] ...)
+            (let-syntax ([tv (make-rename-transformer (assign-type (assign-type #'tv #'k) #'ok #:tag '#,tag))] ...)
               (λ (x ...)
-                (let-syntax ([x (make-rename-transformer (assign-type #'x #'τ #:tag '#,tag))] ...)
-                  (#%expression e) ...)))))
+                (let-syntax ([x (make-rename-transformer (assign-type #'x #'τ))] ...)
+                  (#%expression e) ... void)))))
+       ;#:when (stx-map displayln #'(e+ ...))
+           ;   #:when (displayln (stx-map typeof #'(e+ ...)))
        (list #'tvs+ #'xs+ #'(e+ ...)
              (stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
       [([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvctx tvctx)]))
@@ -122,10 +171,19 @@
   ;; fns derived from infer ---------------------------------------------------
   ;; some are syntactic shortcuts, some are for backwards compat
 
-  ;; shorter name
+  ;; shorter names
+  ; ctx = type env for bound vars in term e, etc
+  ; can also use for bound tyvars in type e
   (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)))
+  ; tyctx = kind env for bound type vars in term e
+  (define (infer/tyctx+erase ctx e)
+    (syntax-parse (infer (list e) #:tvctx ctx)
+      [(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
+  
   ;; infers type and erases types in a single expression,
   ;; in the context of the given bindings and their types
   (define (infer/type-ctxt+erase x+τs e)
@@ -151,8 +209,7 @@
   (define current-type-eval (make-parameter #f))
   (define (type-evals τs) #`#,(stx-map (current-type-eval) τs))
 
-  ; get rid of this?
-  (define current-promote (make-parameter (λ (x) x)))
+  (define current-promote (make-parameter (λ (t) t)))
 
   ;; term expansion
   ;; expand/df : Syntax -> Syntax
@@ -188,8 +245,8 @@
         ; partial expand to reveal #%type wrapper
         (syntax-parse (local-expand τ 'expression (list #'#%type))
           [((~literal #%type) _) #t] [_ #f])))
-  (define (plain-type? τ)
-    (and (typeof τ) (typecheck? (typeof τ) #'#%type) τ))
+  (define (expanded-type? τ)
+    (and (typeof τ) #;(typecheck? (typeof τ) #'#%type) τ))
 
   ; surface type syntax is saved as the value of the 'orig property
   (define (add-orig stx orig)
@@ -248,7 +305,8 @@
                    (bracket? (stx-car #'stx)))))))
 
 (begin-for-syntax
-  (define (mk-? id) (format-id id "~a?" id)))
+  (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))
@@ -304,7 +362,7 @@
 
 (define-syntax define-basic-checked-id-stx
   (syntax-parser
-    [(_ τ:id)
+    [(_ τ:id (~optional (~seq : kind) #:defaults ([kind #'#%type])))
      #:with τ? (format-id #'τ "~a?" #'τ)
      #:with τ-internal (generate-temporary #'τ)
      #:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
@@ -335,28 +393,45 @@
                          (current-continuation-marks)))))
          (define-syntax τ
            (syntax-parser
-             [(~var _ id) (add-orig (assign-type #'τ-internal #'#%type) #'τ)])))]))
+             [(~var _ id) (add-orig (assign-type #'τ-internal #'kind) #'τ)])))]))
 
 (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
-    [(_ τ:id (~optional
-              (~seq #:arity op n:exact-nonnegative-integer)
-              #:defaults ([op #'>=] [n #'0])))
+  (syntax-parse stx #:datum-literals (:)
+    [(_ τ:id (~optional (~seq : kind) #:defaults ([kind #'#%type]))
+        (~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 τ-internal (generate-temporary #'τ)
      #:with τ? (mk-? #'τ)
      #:with τ-expander (format-id #'τ "~~~a" #'τ)
      #:with τ-expander* (format-id #'τ-expander "~a*" #'τ-expander)
      #:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
-     #'(begin
-         (provide τ (for-syntax τ-expander τ-expander* inferτ+erase))
+     #:with τ-get (format-id #'τ "~a-get" #'τ)
+     #`(begin
+         (provide τ (for-syntax τ-expander τ-expander* τ? #;inferτ+erase))
          (begin-for-syntax
            (define-syntax τ-expander
              (pattern-expander
               (syntax-parser
-                [(_ . pat)
-                 #'((~literal #%plain-app) (~literal τ-internal) . pat)])))
+                [(_ . pat:id)
+                 #'(~and ((~literal #%plain-lambda) bvs
+                          ((~literal #%plain-app) (~literal τ-internal) . rst))
+                         #,(if (attribute has-bvs?)
+                               #'(~parse pat #'(bvs rst))
+                               #'(~parse pat #'rst)))]
+                [(_ (~optional (~and (~fail #:unless #,(attribute has-bvs?))
+                                  (bv (... ...)))
+                            #:defaults ([(bv 1) null])) . pat)
+                 #'((~literal #%plain-lambda) (bv (... ...))
+                    ((~literal #%plain-app) (~literal τ-internal) . pat))])))
            (define-syntax τ-expander*
              (pattern-expander
               (syntax-parser
@@ -371,8 +446,15 @@
                                   #:msg
                                   "Expected ~a type, got: ~a"
                                   #'τ #'any))))])))
-           (define (τ? t) (and (stx-pair? t) (typecheck? (stx-cadr t) #'τ-internal)))
-           (define (inferτ+erase e)
+           (define (τ? t)
+             (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)
@@ -395,13 +477,25 @@
          ;; ; this is the actual constructor
          (define-syntax (τ stx)
            (syntax-parse stx
-             [(_ . args)
+             [(_ (~optional (~and (~fail #:unless #,(attribute has-bvs?))
+                                  (bv (... ...)))
+                            #:defaults ([(bv 1) null])) . args)
+              #:with bvs #'(bv (... ...))
+              #:fail-unless (bvs-op (stx-length #'bvs) bvs-n)
+                            (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 (~! (~var ty type) (... ...)) #'args
+              #: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 (~! [arg- τ_arg] (... ...)) (infers+erase #'args)
 ;              #:when (stx-andmap (λ (t) (typecheck? t #'#%type)) #'(τ_arg (... ...)))
-              (assign-type #'(τ-internal ty.norm (... ...)) #'#%type)]
+              (assign-type #'(λ bvs- (τ-internal . τs-)) #'kind)]
              ;; else fail with err msg
              [_
               (type-error #:src stx
@@ -797,6 +891,41 @@
 ;              #:when (typecheck? #'tycon #'tmp)
 ;              (stx-length #'(τ_arg (... ...)))])))]))
 
+; examples:
+; (define-syntax-category type)
+; (define-syntax-category kind)
+(define-syntax (define-syntax-category stx)
+  (syntax-parse stx
+    [(_ name:id)
+     #:with #%tag (format-id #'name "#%~a" #'name)
+     #:with #%tag? (mk-? #'#%tag)
+     #:with name? (mk-? #'name)
+     #:with named-binding (format-id #'name "~aed-binding" #'name)
+     #'(begin
+         (define #%tag void)
+         (begin-for-syntax
+           (define (#%tag? t) (typecheck? t #'#%tag))
+           (define (name? t) (#%tag? (typeof t)))
+           (define-syntax-class name
+             #:attributes (norm)
+             (pattern τ
+              #:with norm ((current-type-eval) #'τ)
+              #:with k (typeof #'norm)
+              #:fail-unless (#%tag? #'k)
+              (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)
+             (pattern any
+                      #:fail-when #t
+                      (format
+                       (string-append
+                        "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))))]))
 ;; syntax classes
 (begin-for-syntax
   (define-syntax-class type
@@ -805,7 +934,9 @@
     ;; -dont bother to check if type is already expanded, because this class
     ;; typically annotates user-written types
     (pattern τ
-     #:with [norm k] (infer+erase #'τ)
+;     #:with [norm k] (infer+erase #'τ)
+      #:with norm ((current-type-eval) #'τ)
+      #:with k (typeof #'norm)
      #:fail-unless (#%type? #'k)
                    (format "~a (~a:~a) not a valid type: ~a"
                            (syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ)
@@ -846,7 +977,11 @@
 
 (define-syntax (define-primop stx)
     (syntax-parse stx #:datum-literals (:)
-      [(_ op:id : τ:type)
+      [(_ op:id : τ (~optional (~seq : k) #:defaults ([k #'#%type])))
+       #:with kind ((current-type-eval) #'k)
+       #:with τ+ ((current-type-eval) #'τ)
+       #:with k_τ (typeof #'τ+)
+       #:when (typecheck? #'k_τ #'kind)
        #:with op/tc (generate-temporary #'op)
        #`(begin
            (provide (rename-out [op/tc op]))