diff --git a/macrotypes/examples/fomega.rkt b/macrotypes/examples/fomega.rkt
index 4dfeb83..f2b8013 100644
--- a/macrotypes/examples/fomega.rkt
+++ b/macrotypes/examples/fomega.rkt
@@ -31,13 +31,11 @@
   ;; So now "type?" no longer validates types, rather it's a subset.
   ;; But we no longer need type? to validate types, instead we can use 
   ;; (kind? (typeof t))
-  (current-type? (λ (t)
-                   (define k (kindof t))
+  (current-type? (λ (t) (define k (kindof t))
                    #;(or (type? t) (★? (typeof t)) (∀★? (typeof t)))
                    (and k ((current-kind?) k) (not (⇒? k)))))
   ;; o.w., a valid type is one with any valid kind
-  (current-any-type? (λ (t) 
-                       (define k (kindof t))
+  (current-any-type? (λ (t) (define k (kindof t))
                        (and k ((current-kind?) k)))))
 
 
diff --git a/macrotypes/stx-utils.rkt b/macrotypes/stx-utils.rkt
index 702f7a6..2a4624c 100644
--- a/macrotypes/stx-utils.rkt
+++ b/macrotypes/stx-utils.rkt
@@ -11,6 +11,7 @@
 (define (stx-caddr stx) (stx-cadr (stx-cdr stx)))
 (define (stx-cddr stx) (stx-cdr (stx-cdr stx)))
 
+(define datum->stx datum->syntax)
 (define (stx->datum stx)
   (if (syntax? stx)
       (syntax->datum stx)
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
index 14cc917..89dc148 100644
--- a/macrotypes/typecheck.rkt
+++ b/macrotypes/typecheck.rkt
@@ -259,9 +259,12 @@
      #:with current-type? (mk-param #'type?)
      #:with current-any-type? (mk-param #'any-type?)
      ;; assigning and retrieving types
+     #:with type-key1 (format-id #'name "~a-key1" #'name)
+     #:with type-key2 (format-id #'name "~a-key2" #'name)
      #:with assign-type (format-id #'name "assign-~a" #'name)
      #:with fast-assign-type (format-id #'name "fast-assign-~a" #'name)
      #:with typeof (format-id #'name "~aof" #'name)
+     #:with tagoftype (format-id #'name "tagof~a" #'name)
      ;; type checking
      #:with current-typecheck-relation (format-id #'name "current-~acheck-relation" #'name)
      #:with typecheck? (format-id #'name "~acheck?" #'name)
@@ -288,17 +291,20 @@
            (define (#%tag? t)        (and (id? t) (free-id=? t #'#%tag)))
            (define (mk-type t)       (attach t 'key2 #'#%tag))
            ;; type? corresponds to "well-formed" types
-           (define (type? t)         (#%tag? (detach t 'key2)))
+           (define (type? t)         (#%tag? (tagoftype t)))
            (define current-type?     (make-parameter type?))
            ;; any-type? corresponds to any type, defaults to type?
            (define (any-type? t)     (type? t))
            (define current-any-type? (make-parameter any-type?))
            ;; assigning and retrieving types ----------------------------------
-           (define (typeof stx) (detach stx 'key1))
+           (define (type-key1) 'key1)
+           (define (type-key2) 'key2)
+           (define (typeof stx)    (detach stx 'key1))
+           (define (tagoftype stx) (detach stx 'key2)) ; = kindof if kind stx-cat defined
            (define (fast-assign-type e τ)
              (attach e 'key1 (syntax-local-introduce τ)))
            (define (assign-type e τ)
-               (fast-assign-type e ((current-type-eval) τ)))
+             (fast-assign-type e ((current-type-eval) τ)))
            ;; helper stx classes ----------------------------------------------
            (define-syntax-class type ;; e.g., well-formed types
              #:attributes (norm)
@@ -444,7 +450,7 @@
                      (add-orig 
                       (attach
                        (syntax/loc this-syntax (τ-internal))
-                       'new-key2 (expand/df #'new-#%tag))
+                       'new-key2 ((current-type-eval) #'new-#%tag))
                       #'τ)])))]))
          (define-syntax define-base-types
            (syntax-parser
@@ -681,7 +687,7 @@
                                          #'(kindcon k_arg (... (... ...)))
                                          #'#%tag)
                      (add-orig
-                      (attach #'(τ- bvs- . τs-) 'key2 (expand/df #'k_result))
+                      (attach #'(τ- bvs- . τs-) 'key2 ((current-type-eval) #'k_result))
                       stx)])))])))]))
 
 ;; end define-syntax-category -------------------------------------------------
@@ -690,16 +696,34 @@
 ;; pre-declare all type-related functions and forms
 (define-syntax-category type)
 
+;; generic, type-agnostic parameters
+;; Use these for code that is generic over types and kinds
+(begin-for-syntax
+  (define current=? (make-parameter (current-type=?)))
+  (define (=s? xs1 xs2) ; map current=? pairwise over lists
+    (and (stx-length=? xs1 xs2) (stx-andmap (current=?) xs1 xs2)))
+  (define (sames? stx)  ; check list contains same types
+    (define xs (stx->list stx))
+    (or (null? xs) (andmap (λ (x) ((current=?) (car xs) x)) (cdr xs))))
+  (define current-check-relation (make-parameter (current-typecheck-relation)))
+  (define (check? x1 x2) ((current-check-relation) x1 x2))
+  (define (checks? xs1 xs2) ; map current-check-relation pairwise of lists
+    (and (stx-length=? xs1 xs2) (stx-andmap check? xs1 xs2)))
+  ;; (define current-attach (make-parameter assign-type))
+  ;; (define current-detach (make-parameter typeof))
+  (define current-ev (make-parameter (current-type-eval)))
+  (define current-tag (make-parameter (type-key1))))
+
 ;; type assignment utilities --------------------------------------------------
 (begin-for-syntax
   ;; Type assignment macro for nicer syntax
   (define-syntax (⊢ stx)
     (syntax-parse stx
-      [(_ e tag τ) #'(attach #`e 'tag ((current-type-eval) #`τ))]
+      [(_ e tag τ) #'(attach #`e 'tag ((current-ev) #`τ))]
       [(_ e τ) #'(⊢ e : τ)]))
   (define-syntax (⊢/no-teval stx)
     (syntax-parse stx
-      [(_ e tag τ) #'(attach #`e 'tag ((current-type-eval) #`τ))]
+      [(_ e tag τ) #'(attach #`e 'tag ((current-ev) #`τ))]
       [(_ e τ) #'(⊢/no-teval e : τ)]))
 
   ;; Actual type assignment function.
@@ -817,18 +841,18 @@
 
   ;; basic infer function with no context:
   ;; infers the type and erases types in an expression
-  (define (infer+erase e #:tag [tag ':])
+  (define (infer+erase e #:tag [tag (current-tag)])
     (define e+ (expand/df e))
     (list e+ (detach e+ tag)))
   ;; infers the types and erases types in multiple expressions
-  (define (infers+erase es #:tag [tag ':])
+  (define (infers+erase es #:tag [tag (current-tag)])
     (stx-map (λ (e) (infer+erase e #:tag tag)) es))
 
   ;; This is the main "infer" function. All others are defined in terms of this.
   ;; It should be named infer+erase but leaving it for now for backward compat.
   ;; ctx = vars and their types (or other props, denoted with "sep")
   ;; tvctx = tyvars and their kinds
-  (define (infer es #:ctx [ctx null] #:tvctx [tvctx null] #:tag [tag ':])
+  (define (infer es #:ctx [ctx null] #:tvctx [tvctx null] #:tag [tag (current-tag)])
     (syntax-parse ctx
       [([x sep τ] ...) ; dont expand yet bc τ may have references to tvs
        #:with ([tv (~seq tvsep:id tvk) ...] ...) tvctx
@@ -855,16 +879,16 @@
                                (for/fold ([tv-id #'tv])
                                          ([s (in-list (list 'tvsep ...))]
                                           [k (in-list (list #'tvk ...))])
-                                 (attach tv-id s ((current-type-eval) k)))
+                                 (attach tv-id s ((current-ev) k)))
                                'tyvar #t))] ...)
               (λ (x ...)
                (let-syntax 
-                ([x (make-variable-like-transformer (attach #'x 'sep ((current-type-eval) #'τ)))] ...)
+                ([x (make-variable-like-transformer (attach #'x 'sep ((current-ev) #'τ)))] ...)
                  (#%expression e) ... void)))))
        (list #'tvs+ #'xs+ 
              #'(e+ ...) 
              (stx-map (λ (e) (detach e tag)) #'(e+ ...)))]
-      [([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvctx tvctx #:tag tag)]))
+      [([x τ] ...) (infer es #:ctx #`([x #,tag τ] ...) #:tvctx tvctx #:tag tag)]))
 
   ;; fns derived from infer ---------------------------------------------------
   ;; some are syntactic shortcuts, some are for backwards compat
@@ -872,16 +896,16 @@
   ;; 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 #:tag [tag ':])
+  (define (infer/ctx+erase ctx e #:tag [tag (current-tag)])
     (syntax-parse (infer (list e) #:ctx ctx #:tag tag)
       [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
-  (define (infers/ctx+erase ctx es #:tag [tag ':])
+  (define (infers/ctx+erase ctx es #:tag [tag (current-tag)])
     (stx-cdr (infer es #:ctx ctx #:tag tag)))
   ; tyctx = kind env for bound type vars in term e
-  (define (infer/tyctx+erase ctx e #:tag [tag ':])
+  (define (infer/tyctx+erase ctx e #:tag [tag (current-tag)])
     (syntax-parse (infer (list e) #:tvctx ctx #:tag tag)
       [(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
-  (define (infers/tyctx+erase ctx es #:tag [tag ':])
+  (define (infers/tyctx+erase ctx es #:tag [tag (current-tag)])
     (syntax-parse (infer es #:tvctx ctx #:tag tag)
       [(tvs+ _ es+ tys) (list #'tvs+ #'es+ #'tys)]))
 
@@ -1227,7 +1251,7 @@
                          #,(if (attribute has-annotations?)
                                #'(~and
                                   (~parse (kindcon-expander k (... (... ...)))
-                                          (detach #'expanded-τ))
+                                          (tagoftype #'expanded-τ))
                                   (~parse pat
                                           #'[([tv k] (... (... ...))) rst]))
                                #'(~parse
@@ -1363,7 +1387,7 @@
                                       (free-identifier=? #'actual #'lit))
                         fail-msg)
                  stx))])))
-  (define (merge-type-tags stx)
+  (define (merge-type-tags stx) ;; TODO: merge other tags
     (define t (syntax-property stx ':))
     (or (and (pair? t)
              (identifier? (car t)) (identifier? (cdr t))
diff --git a/turnstile/examples/fomega.rkt b/turnstile/examples/fomega.rkt
index 6746138..302c7f3 100644
--- a/turnstile/examples/fomega.rkt
+++ b/turnstile/examples/fomega.rkt
@@ -17,7 +17,7 @@
          (type-out ★ ⇒ ∀★ ∀)
          Λ inst tyλ tyapp)
 
-(define-syntax-category kind)
+(define-syntax-category :: kind :::)
 
 ; want #%type to be equiv to★
 ; => edit current-kind? so existing #%type annotations (with no #%kind tag)
@@ -31,16 +31,19 @@
   ;; So now "type?" no longer validates types, rather it's a subset.
   ;; But we no longer need type? to validate types, instead we can use
   ;; (kind? (typeof t))
-  (current-type? (λ (t)
-                   (define k (typeof t))
+  (current-type? (λ (t) (define k (kindof t))
                    #;(or (type? t) (★? (typeof t)) (∀★? (typeof t)))
-                   (and ((current-kind?) k) (not (⇒? k))))))
+                   (and k ((current-kind?) k) (not (⇒? k)))))
+  ;; o.w., a valid type is one with any valid kind
+  (current-any-type? (λ (t) (define k (kindof t))
+                        (and k ((current-kind?) k)))))
+
 
 ; must override, to handle kinds
 (define-syntax define-type-alias
   (syntax-parser
     [(define-type-alias alias:id τ)
-     #:with (τ- k_τ) (infer+erase #'τ)
+     #:with (τ- k_τ) (infer+erase #'τ #:tag '::)
      #:fail-unless ((current-kind?) #'k_τ)
                    (format "not a valid type: ~a\n" (type->str #'τ))
      #'(define-syntax alias 
@@ -79,39 +82,41 @@
   (define old-eval (current-type-eval))
   (define (type-eval τ) (normalize (old-eval τ)))
   (current-type-eval type-eval)
+  (current-ev type-eval)
   
   (define old-type=? (current-type=?))
   ; ty=? == syntax eq and syntax prop eq
   (define (type=? t1 t2)
-    (let ([k1 (typeof t1)][k2 (typeof t2)])
+    (let ([k1 (kindof t1)][k2 (kindof t2)])
       (and (or (and (not k1) (not k2))
-               (and k1 k2 ((current-type=?) k1 k2)))
+               (and k1 k2 ((current-kind=?) k1 k2)))
            (old-type=? t1 t2))))
   (current-type=? type=?)
-  (current-typecheck-relation (current-type=?)))
+  (current-typecheck-relation type=?)
+  (current-check-relation type=?))
 
 (define-typed-syntax (Λ bvs:kind-ctx e) ≫
-  [([bvs.x ≫ tv- : bvs.kind] ...) () ⊢ e ≫ e- ⇒ τ_e]
+  [([bvs.x ≫ tv- :: bvs.kind] ...) () ⊢ e ≫ e- ⇒ τ_e]
   --------
-  [⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)])
+  [⊢ e- ⇒ (∀ ([tv- :: bvs.kind] ...) τ_e)])
 
-(define-typed-syntax (inst e τ ...) ≫
-  [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ (~∀★ k ...))]
-  [⊢ τ ≫ τ- ⇐ k] ...
+(define-typed-syntax (inst e τ:any-type ...) ≫
+  [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ :: (~∀★ k ...))]
+  [⊢ τ ≫ τ- ⇐ :: k] ...
   #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
   --------
   [⊢ e- ⇒ τ-inst])
 
 ;; TODO: merge with regular λ and app?
 ;; - see fomega2.rkt
-(define-typed-syntax (tyλ bvs:kind-ctx τ_body) ≫
-  [[bvs.x ≫ tv- : bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body]
+(define-kinded-syntax (tyλ bvs:kind-ctx τ_body) ≫
+  [[bvs.x ≫ tv- :: bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body]
   #:fail-unless ((current-kind?) #'k_body)
-  (format "not a valid type: ~a\n" (type->str #'τ_body))
+                (format "not a valid type: ~a\n" (type->str #'τ_body))
   --------
   [⊢ (λ- (tv- ...) τ_body-) ⇒ (⇒ bvs.kind ... k_body)])
 
-(define-typed-syntax (tyapp τ_fn τ_arg ...) ≫
+(define-kinded-syntax (tyapp τ_fn τ_arg ...) ≫
   [⊢ τ_fn ≫ τ_fn- ⇒ (~⇒ k_in ... k_out)]
   #:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
   (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])
diff --git a/turnstile/examples/tests/fomega-tests.rkt b/turnstile/examples/tests/fomega-tests.rkt
index 12a9b2d..62e600e 100644
--- a/turnstile/examples/tests/fomega-tests.rkt
+++ b/turnstile/examples/tests/fomega-tests.rkt
@@ -1,82 +1,82 @@
 #lang s-exp "../fomega.rkt"
 (require "rackunit-typechecking.rkt")
 
-(check-type Int : ★)
-(check-type String : ★)
+(check-type Int :: ★)
+(check-type String :: ★)
 (typecheck-fail →)
-(check-type (→ Int Int) : ★)
+(check-type (→ Int Int) :: ★)
 (typecheck-fail (→ →))
 (typecheck-fail (→ 1))
 (check-type 1 : Int)
 
-(typecheck-fail (tyλ ([x : ★]) 1) #:with-msg "not a valid type: 1")
+(typecheck-fail (tyλ ([x :: ★]) 1) #:with-msg "not a valid type: 1")
 
-(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
-(check-not-type (Λ ([X : ★]) (λ ([x : X]) x)) :
-                (∀ ([X : (∀★ ★)]) (→ X X)))
+(check-type (Λ ([X :: ★]) (λ ([x : X]) x)) : (∀ ([X :: ★]) (→ X X)))
+(check-not-type (Λ ([X :: ★]) (λ ([x : X]) x)) :
+                (∀ ([X :: (∀★ ★)]) (→ X X)))
 
-;(check-type (∀ ([t : ★]) (→ t t)) : ★)
-(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
-(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
+;(check-type (∀ ([t :: ★]) (→ t t)) :: ★)
+(check-type (∀ ([t :: ★]) (→ t t)) :: (∀★ ★))
+(check-type (→ (∀ ([t :: ★]) (→ t t)) (→ Int Int)) :: ★)
 
-(check-type (Λ ([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))))
+(check-type ((λ ([x : (∀ ([X :: ★]) (→ X X))]) x) (Λ ([X :: ★]) (λ ([x : X]) x)))
+            : (∀ ([X :: ★]) (→ X X)))
+(typecheck-fail ((λ ([x : (∀ ([X :: ★]) (→ X X))]) x) (Λ ([X : (⇒ ★ ★)]) (λ ([x : X]) x))))
 
-(check-type (tyλ ([t : ★]) t) : (⇒ ★ ★))
-(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★))
-(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★)))
-(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★)))
-(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
-(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★))
+(check-type (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"))
+(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)
-            : (⇒ ★ ★))
+(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))))
+(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))
+             (Λ ([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 "inst: type mismatch: expected ★, given Int\n *expression: 1")
+ (inst (Λ ([X :: ★]) (λ ([x : X]) x)) 1)
+ #:with-msg "inst:.*not a valid type: 1")
 
 (typecheck-fail
- (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
+ (Λ ([tyf :: (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
  #:with-msg "Expected → type, got: \\(tyapp tyf String\\)")
 ;; applied f too early
 (typecheck-fail
  (inst
-  (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
-  (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+  (Λ ([tyf :: (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
+  (tyapp (tyλ ([arg :: ★]) (tyλ ([res :: ★]) (→ arg res))) Int))
  #:with-msg "Expected → type, got: \\(tyapp tyf String\\)")
 (check-type ((inst
-              (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
-              (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+              (Λ ([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))
+               (Λ ([tyf :: (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+              (tyapp (tyλ ([arg :: ★]) (tyλ ([res :: ★]) (→ arg res))) Int))
               (λ ([x : Int]) "int")) 1) : String ⇒ "int")
 
 ;; tapl examples, p441
 (typecheck-fail
  (define-type-alias tmp 1)
  #:with-msg "not a valid type: 1")
-(define-type-alias Id (tyλ ([X : ★]) X))
+(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))
@@ -89,104 +89,104 @@
 (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))))
+(define-type-alias Pair (tyλ ([A :: ★] [B :: ★]) (∀ ([X :: ★]) (→ (→ A B X) X))))
 
 ;(check-type Pair : (⇒ ★ ★ ★))
-(check-type Pair : (⇒ ★ ★ (∀★ ★)))
+(check-type Pair :: (⇒ ★ ★ (∀★ ★)))
 
-(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
+(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))))
+ (Λ ([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)))))
+ (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)))))
+ ((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)))
+ (Λ ([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))))
+  (Λ ([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))))
+   (Λ ([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)))))
+  ((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)))
+ (Λ ([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))))
+  (Λ ([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))))
+   (Λ ([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)))))
+  ((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 :: ★]) (λ ([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)))))
+(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-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-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)
+(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))
+(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))
+(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))))
+(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 ((λ ([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))
-             (Λ ([s : ★]) (λ ([y : s]) y)))
+(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)
 
 
diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt
index a7ce5b6..0ed9c76 100644
--- a/turnstile/turnstile.rkt
+++ b/turnstile/turnstile.rkt
@@ -25,16 +25,18 @@
   ;;   xs-   ; a stx-list of the expanded versions of variables in the ctx
   ;;   es*-  ; a nested list a depth given by the depth argument, with the same structure
   ;;         ; as es*, containing the expanded es*, with the types attached
-  (define (infer/depth #:ctx ctx #:tvctx tvctx depth es* origs*)
+  (define (infer/depth #:ctx ctx #:tvctx tvctx depth es* origs*
+                       #:tag [tag (current-tag)])
     (define flat (stx-flatten/depth-lens depth))
     (define es (lens-view flat es*))
     (define origs (lens-view flat origs*))
     (define/with-syntax [tvxs- xs- es- _]
-      (infer #:tvctx tvctx #:ctx ctx (stx-map pass-orig es origs)))
+      (infer #:tvctx tvctx #:ctx ctx (stx-map pass-orig es origs) #:tag tag))
     (define es*- (lens-set flat es* #'es-))
     (list #'tvxs- #'xs- es*-))
   ;; infers/depths
-  (define (infers/depths clause-depth tc-depth tvctxs/ctxs/ess/origss*)
+  (define (infers/depths clause-depth tc-depth tvctxs/ctxs/ess/origss*
+                         #:tag [tag (current-tag)])
     (define flat (stx-flatten/depth-lens clause-depth))
     (define tvctxs/ctxs/ess/origss
       (lens-view flat tvctxs/ctxs/ess/origss*))
@@ -42,7 +44,7 @@
       (for/list ([tvctx/ctx/es/origs (in-list (stx->list tvctxs/ctxs/ess/origss))])
         (match-define (list tvctx ctx es origs)
           (stx->list tvctx/ctx/es/origs))
-        (infer/depth #:tvctx tvctx #:ctx ctx tc-depth es origs)))
+        (infer/depth #:tvctx tvctx #:ctx ctx tc-depth es origs #:tag tag)))
     (define res
       (lens-set flat tvctxs/ctxs/ess/origss* tcs))
     res)
@@ -92,44 +94,45 @@
   (define-splicing-syntax-class ⇒-prop
     #:datum-literals (⇒)
     #:attributes (e-pat)
-    [pattern (~or (~seq ⇒ tag-pat ; implicit : tag
-                        (~parse tag #':) (tag-prop:⇒-prop) ...)
+    [pattern (~or (~seq ⇒ tag-pat ; implicit tag
+                          (~parse tag #',(current-tag))
+                          (tag-prop:⇒-prop) ...)
                   (~seq ⇒ tag:id tag-pat (tag-prop:⇒-prop) ...)) ; explicit tag
              #:with e-tmp (generate-temporary)
              #:with e-pat
              #'(~and e-tmp
                      (~parse
                       (~and tag-prop.e-pat ... tag-pat)
-                      (detach #'e-tmp 'tag)))])
+                      (detach #'e-tmp `tag)))])
   (define-splicing-syntax-class ⇒-prop/conclusion
     #:datum-literals (⇒)
     #:attributes (tag tag-expr)
-    [pattern (~or (~seq ⇒ tag-stx 
-                        (~parse tag #':)
-                        (~parse (tag-prop.tag ...) #'())
-                        (~parse (tag-prop.tag-expr ...) #'()))
+    [pattern (~or (~seq ⇒ tag-stx ; implicit tag
+                          (~parse tag #',(current-tag))
+                          (~parse (tag-prop.tag ...) #'())
+                          (~parse (tag-prop.tag-expr ...) #'()))
                   (~seq ⇒ tag:id tag-stx (tag-prop:⇒-prop/conclusion) ...))
              #:with tag-expr
              (for/fold ([tag-expr #'#`tag-stx])
-                       ([k (in-list (syntax->list #'[tag-prop.tag ...]))]
-                        [v (in-list (syntax->list #'[tag-prop.tag-expr ...]))])
+                       ([k (in-stx-list #'[tag-prop.tag ...])]
+                        [v (in-stx-list #'[tag-prop.tag-expr ...])])
                (with-syntax ([tag-expr tag-expr] [k k] [v v])
-                 #'(attach tag-expr 'k ((current-type-eval) v))))])
+                 #'(attach tag-expr `k ((current-ev) v))))])
   (define-splicing-syntax-class ⇐-prop
-    #:datum-literals (⇐ :)
+    #:datum-literals (⇐)
     #:attributes (τ-stx e-pat)
-    [pattern (~or (~seq ⇐ τ-stx)
-                  (~seq ⇐ : τ-stx))
+    [pattern (~or (~seq ⇐ τ-stx (~parse tag #',(current-tag)))
+                  (~seq ⇐ tag:id τ-stx))
              #:with e-tmp (generate-temporary)
              #:with τ-tmp (generate-temporary)
              #:with τ-exp (generate-temporary)
              #:with e-pat
-             #'(~and e-tmp
+             #`(~and e-tmp
                      (~parse τ-exp (get-expected-type #'e-tmp))
-                     (~parse τ-tmp (typeof #'e-tmp))
+                     (~parse τ-tmp (detach #'e-tmp `tag))
                      (~parse
                       (~post
-                       (~fail #:when (and (not (typecheck? #'τ-tmp #'τ-exp))
+                       (~fail #:when (and (not (check? #'τ-tmp #'τ-exp))
                                           (get-orig #'e-tmp))
                               (typecheck-fail-msg/1 #'τ-exp #'τ-tmp #'e-tmp)))
                       (get-orig #'e-tmp)))])
@@ -165,7 +168,7 @@
              #:with [x- ...] #'[ctx1.x- ... ...]
              #:with [ctx ...] #'[ctx1.ctx ... ...]])
   (define-syntax-class tc-elem
-    #:datum-literals (⊢ ⇒ ⇐ ≫ :)
+    #:datum-literals (⊢ ⇒ ⇐ ≫)
     #:attributes (e-stx e-stx-orig e-pat)
     [pattern [e-stx ≫ e-pat* props:⇒-props]
              #:with e-stx-orig #'e-stx
@@ -229,55 +232,56 @@
               #'[(tvctx.ctx ...) (ctx.ctx ...) tc.es-stx tc.es-stx-orig]
               #'[ooo ...])
              #:with pat
-             #'(~post
+             #`(~post
                 (~post
                  (~parse
                   tcs-pat
-                  (infers/depths 'clause-depth 'tc.depth #'tvctxs/ctxs/ess/origs))))]
+                  (infers/depths 'clause-depth 'tc.depth #'tvctxs/ctxs/ess/origs
+                                 #:tag (current-tag)))))]
     )
   (define-splicing-syntax-class clause
     #:attributes (pat)
-    #:datum-literals (τ⊑ τ=)
+    #:datum-literals (τ⊑ τ=) ; TODO: drop the τ
     [pattern :tc-clause]
     [pattern [a τ⊑ b]
              #:with pat
              #'(~post
-                (~fail #:unless (typecheck? #'a #'b)
+                (~fail #:unless (check? #'a #'b)
                        (typecheck-fail-msg/1/no-expr #'b #'a)))]
     [pattern [a τ⊑ b #:for e]
              #:with pat
              #'(~post
-                (~fail #:unless (typecheck? #'a #'b)
+                (~fail #:unless (check? #'a #'b)
                        (typecheck-fail-msg/1 #'b #'a #'e)))]
     [pattern (~seq [a τ⊑ b] ooo:elipsis)
              #:with pat
              #'(~post
-                (~fail #:unless (typechecks? #'[a ooo] #'[b ooo])
+                (~fail #:unless (checks? #'[a ooo] #'[b ooo])
                        (typecheck-fail-msg/multi/no-exprs #'[b ooo] #'[a ooo])))]
     [pattern (~seq [a τ⊑ b #:for e] ooo:elipsis)
              #:with pat
              #'(~post
-                (~fail #:unless (typechecks? #'[a ooo] #'[b ooo])
+                (~fail #:unless (checks? #'[a ooo] #'[b ooo])
                        (typecheck-fail-msg/multi #'[b ooo] #'[a ooo] #'[e ooo])))]
     [pattern [a τ= b]
              #:with pat
              #'(~post
-                (~fail #:unless ((current-type=?) #'a #'b)
+                (~fail #:unless ((current=?) #'a #'b)
                        (typecheck-fail-msg/1/no-expr #'b #'a)))]
     [pattern [a τ= b #:for e]
              #:with pat
              #'(~post
-                (~fail #:unless ((current-type=?) #'a #'b)
+                (~fail #:unless ((current=?) #'a #'b)
                        (typecheck-fail-msg/1 #'b #'a #'e)))]
     [pattern (~seq [a τ= b] ooo:elipsis)
              #:with pat
              #'(~post
-                (~fail #:unless (types=? #'[a ooo] #'[b ooo])
+                (~fail #:unless (=s? #'[a ooo] #'[b ooo])
                        (typecheck-fail-msg/multi/no-exprs #'[b ooo] #'[a ooo])))]
     [pattern (~seq [a τ= b #:for e] ooo:elipsis)
              #:with pat
              #'(~post
-                (~fail #:unless (types=? #'[a ooo] #'[b ooo])
+                (~fail #:unless (=s? #'[a ooo] #'[b ooo])
                        (typecheck-fail-msg/multi #'[b ooo] #'[a ooo] #'[e ooo])))]
     [pattern (~seq #:when condition:expr)
              #:with pat
@@ -296,7 +300,7 @@
              #'(~post (~fail #:unless condition message))]
     )
   (define-syntax-class last-clause
-    #:datum-literals (⊢ ≫ ≻ ⇒ ⇐ :)
+    #:datum-literals (⊢ ≫ ≻ ⇒ ⇐)
     #:attributes ([pat 0] [stuff 1] [body 0])
     ;; ⇒ conclusion
     [pattern (~or [⊢ pat ≫ e-stx props:⇒-props/conclusion]
@@ -304,21 +308,25 @@
              #:with [stuff ...] #'[]
              #:with body:expr
              (for/fold ([body #'(quasisyntax/loc this-syntax e-stx)])
-                       ([k (in-list (syntax->list #'[props.tag ...]))]
-                        [v (in-list (syntax->list #'[props.tag-expr ...]))])
+                       ([k (in-stx-list #'[props.tag ...])]
+                        [v (in-stx-list #'[props.tag-expr ...])])
                (with-syntax ([body body] [k k] [v v])
-                 #'(attach body 'k ((current-type-eval) v))))]
+                 #'(attach body `k ((current-ev) v))))]
     ;; ⇒ conclusion, implicit pat
     [pattern (~or [⊢ e-stx props:⇒-props/conclusion]
                   [⊢ [e-stx props:⇒-props/conclusion]])
              #:with :last-clause #'[⊢ [_ ≫ e-stx . props]]]
     ;; ⇐ conclusion
-    [pattern [⊢ (~and e-stx (~not [_ ≫ . rst]))]
-             #:with :last-clause #'[⊢ [_ ≫ e-stx ⇐ : _]]]
-    [pattern (~or [⊢ pat* ≫ e-stx ⇐ τ-pat]
-                  [⊢ pat* ≫ e-stx ⇐ : τ-pat]
-                  [⊢ [pat* ≫ e-stx ⇐ τ-pat]]
-                  [⊢ [pat* ≫ e-stx ⇐ : τ-pat]])
+    [pattern [⊢ (~and e-stx (~not [_ ≫ . rst]))] ;; TODO: this current tag isnt right?
+             #:with :last-clause #`[⊢ [_ ≫ e-stx ⇐ #,(datum->stx #'h (current-tag)) _]]]
+    [pattern (~or [⊢ pat* (~seq ≫ e-stx
+                                ⇐ τ-pat ; implicit tag
+                                  (~parse tag #',(current-tag)))]
+                  [⊢ pat* ≫ e-stx ⇐ tag:id τ-pat] ; explicit tag
+                  [⊢ [pat* (~seq ≫ e-stx
+                                 ⇐ τ-pat ; implicit tag
+                                   (~parse tag #',(current-tag)))]]
+                  [⊢ [pat* ≫ e-stx ⇐ tag:id τ-pat]]) ; explicit tag
              #:with stx (generate-temporary 'stx)
              #:with τ (generate-temporary #'τ-pat)
              #:with pat
@@ -330,7 +338,7 @@
                      (~parse τ-pat #'τ))
              #:with [stuff ...] #'[]
              #:with body:expr
-             #'(assign-type (quasisyntax/loc this-syntax e-stx) #`τ)]
+             #'(attach (quasisyntax/loc this-syntax e-stx) `tag #`τ)]
     ;; macro invocations
     [pattern [≻ e-stx]
              #:with :last-clause #'[_ ≻ e-stx]]
@@ -346,11 +354,12 @@
              #:with body:expr
              ;; should never get here
              #'(error msg)])
-  (define-splicing-syntax-class pat #:datum-literals (⇐ :)
+  (define-splicing-syntax-class pat #:datum-literals (⇐)
     [pattern (~seq pat)
              #:attr transform-body identity]
-    [pattern (~or (~seq pat* left:⇐ τ-pat)
-                  (~seq pat* left:⇐ : τ-pat))
+    [pattern (~or (~seq pat* left:⇐ τ-pat ; implicit tag
+                        (~parse tag #',current-tag))
+                  (~seq pat* left:⇐ tag:id τ-pat)) ; explicit tag
              #:with stx (generate-temporary 'stx)
              #:with τ (generate-temporary #'τ-pat)
              #:with b (generate-temporary 'body)
@@ -363,11 +372,10 @@
                      (~parse τ-pat #'τ))
              #:attr transform-body
              (lambda (body)
-               #`(let ([b #,body])
-                   (when (and (typeof b)
-                              (not (typecheck? (typeof b) #'τ)))
-                     (raise-⇐-expected-type-error #'left b #'τ (typeof b)))
-                   (assign-type b #'τ)))])
+               #`(let* ([b #,body][ty-b (detach b `tag)])
+                   (when (and ty-b (not (check? ty-b #'τ)))
+                     (raise-⇐-expected-type-error #'left b #'τ ty-b))
+                   (attach b `tag #'τ)))])
   (define-syntax-class rule #:datum-literals (≫)
     [pattern [pat:pat ≫
               clause:clause ...
@@ -425,25 +433,43 @@
 (define-syntax define-syntax-category
  (lambda (stx)
    (syntax-parse stx
-    [(_ name:id)
+    [(_ name:id)        ; default key1 = ': for types
+     #'(define-syntax-category : name)]
+    [(_ key:id name:id) ; default key2 = ':: for kinds
+     #`(define-syntax-category key name #,(mkx2 #'key))]
+    [(_ key1:id name:id key2:id)
      #:with def-named-syntax (format-id #'name "define-~aed-syntax" #'name)
-     #:with check-relation (format-id #'name "current-~acheck-relation" #'name)
+     #:with new-check-relation (format-id #'name "current-~acheck-relation" #'name)
+     ;; #:with new-attach (format-id #'name "assign-~a" #'name)
+     ;; #:with new-detach (format-id #'name "~aof" #'name)
+     #:with new-eval (format-id #'name "current-~a-eval" #'name)
      #'(begin
-        (-define-syntax-category name)
+        (-define-syntax-category key1 name key2)
         (define-syntax (def-named-syntax stx)
           (syntax-parse stx
             ;; single-clause def
-           [(_ (rulename:id . pats) . rst)
+            #;[(_ (rulename:id . pats) . rst)
             ;; cannot bind name as pat var, eg #%app, so replace with _
             #:with r #'[(_ . pats) . rst]
             #'(define-syntax (rulename stxx)
-                (parameterize ([current-typecheck-relation (check-relation)])
+                (parameterize ([current-check-relation (new-check-relation)]
+                               [current-attach new-attach]
+                               [current-detach new-detach]
+                               [current-tag 'key1])
                   (syntax-parse/typed-syntax stxx r)))]
+            [(_ (rulename:id . pats) . rst)
+            ;; cannot bind name as pat var, eg #%app, so replace with _
+            #:with r #'[(_ . pats) . rst]
+             #'(def-named-syntax rulename r)]
            ;; multi-clause def
            [(_ rulename:id
               (~and (~seq kw-stuff (... ...)) :stxparse-kws)
               rule:rule (... ...+))
             #'(define-syntax (rulename stxx)
-                (parameterize ([current-typecheck-relation (check-relation)])
+                (parameterize ([current-check-relation (new-check-relation)]
+                               ;; [current-attach new-attach]
+                               ;; [current-detach new-detach]
+                               [current-ev (new-eval)]
+                               [current-tag 'key1])
                   (syntax-parse/typed-syntax stxx kw-stuff (... ...)
                     rule (... ...))))])))])))