diff --git a/macrotypes/examples/fomega.rkt b/macrotypes/examples/fomega.rkt
index b689673..7cf1d36 100644
--- a/macrotypes/examples/fomega.rkt
+++ b/macrotypes/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)
diff --git a/macrotypes/examples/fomega2.rkt b/macrotypes/examples/fomega2.rkt
index ce8145c..88341c9 100644
--- a/macrotypes/examples/fomega2.rkt
+++ b/macrotypes/examples/fomega2.rkt
@@ -20,7 +20,7 @@
          λ #%app Λ inst
          (for-syntax current-kind-eval kindcheck?))
 
-(define-syntax-category :: kind :::)
+(define-syntax-category :: kind)
 
 ;; modify predicates to recognize → (function type) as both type and kind
 (begin-for-syntax
@@ -40,7 +40,7 @@
 (define-syntax define-type-alias
   (syntax-parser
     [(_ alias:id τ)
-     #:with (τ- k_τ) (infer+erase #'τ)
+     #:with (τ- _) (infer+erase #'τ #:tag '::)
      #'(define-syntax alias
          (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))]))
 
diff --git a/macrotypes/examples/fomega3.rkt b/macrotypes/examples/fomega3.rkt
new file mode 100644
index 0000000..3ebeb82
--- /dev/null
+++ b/macrotypes/examples/fomega3.rkt
@@ -0,0 +1,34 @@
+#lang s-exp macrotypes/typecheck
+(extends "fomega.rkt" #:except tyapp tyλ)
+
+;; NOTE 2017-02-03: currently not working
+
+; same as fomega2.rkt --- λ and #%app works as both regular and type versions,
+; → is both type and kind --- but reuses parts of fomega.rkt,
+; ie removes the duplication in fomega2.rkt
+
+;; System F_omega
+;; Type relation:
+;; - redefine current-kind? and current-type so #%app and λ
+;;   work for both terms and types
+;; Types:
+;; - types from fomega.rkt
+;; - String from stlc+reco+var
+;; Terms:
+;; - extend ∀ Λ inst from fomega.rkt
+;; - #%datum from stlc+reco+var
+
+;; types and kinds are now mixed, due to #%app and λ
+(begin-for-syntax
+  (define old-kind? (current-kind?))
+  (current-kind? (λ (k) (or (#%type? k) (old-kind? k) (#%type? (typeof k)))))
+  ;; Try to keep "type?" backward compatible with its uses so far,
+  ;; eg in the definition of λ or previous type constuctors.
+  ;; (However, this is not completely possible, eg define-type-alias)
+  ;; 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) (or (type? t)
+                            (let ([k (typeof t)])
+                              (or (★? k) (∀★? k)))
+                            ((current-kind?) t)))))
diff --git a/macrotypes/examples/tests/fomega2-tests.rkt b/macrotypes/examples/tests/fomega2-tests.rkt
index 78ab66c..d5281bf 100644
--- a/macrotypes/examples/tests/fomega2-tests.rkt
+++ b/macrotypes/examples/tests/fomega2-tests.rkt
@@ -1,6 +1,6 @@
 #lang s-exp "../fomega2.rkt"
 (require "rackunit-typechecking.rkt")
-(require "rackunit-typechecking-fomega2.rkt")
+(require "rackunit-kindchecking.rkt")
 
 (check-kind Int :: ★)
 (check-kind String :: ★)
diff --git a/macrotypes/examples/tests/fomega3-tests.rkt b/macrotypes/examples/tests/fomega3-tests.rkt
new file mode 100644
index 0000000..9a98ede
--- /dev/null
+++ b/macrotypes/examples/tests/fomega3-tests.rkt
@@ -0,0 +1,200 @@
+#lang s-exp "../fomega3.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)) : (∀★ ★))
+(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))))
+
+(check-type (λ ([t : ★]) t) : (→ ★ ★))
+(check-type (λ ([t : ★] [s : ★]) t) : (→ ★ ★ ★))
+(check-type (λ ([t : ★]) (λ ([s : ★]) t)) : (→ ★ (→ ★ ★)))
+(check-type (λ ([t : (→ ★ ★)]) t) : (→ (→ ★ ★) (→ ★ ★)))
+(check-type (λ ([t : (→ ★ ★ ★)]) t) : (→ (→ ★ ★ ★) (→ ★ ★ ★)))
+(check-type (λ ([arg : ★] [res : ★]) (→ arg res)) : (→ ★ ★ ★))
+
+(check-type ((λ ([t : ★]) t) Int) : ★)
+(check-type (λ ([x : ((λ ([t : ★]) t) Int)]) x) : (→ Int Int))
+(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
+(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
+(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
+(typecheck-fail ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
+
+;; partial-apply →
+(check-type ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)
+            : (→ ★ ★))
+; f's type must have kind ★
+(typecheck-fail (λ ([f : ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)]) f))
+(check-type (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) :
+            (∀ ([tyf : (→ ★ ★)]) (→ (tyf String) (tyf String))))
+(check-type (inst
+             (Λ ([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
+                 (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
+                 ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)))
+(check-type ((inst
+              (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+              ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+             (λ ([x : Int]) "int")) : (→ Int String))
+(check-type (((inst
+               (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+              ((λ ([arg : ★]) (λ ([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 (λ ([X : ★]) X))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (Id String)) Int))
+(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int (Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) (Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) String) Int))
+(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (Id (→ Int String)) Int))
+(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
+(define-type-alias Pair (λ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
+
+;(check-type Pair : (→ ★ ★ ★))
+(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 (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 (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")
+ : (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 : ★]) (→ (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)
+ : (→ (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 : ★]) (→ (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)
+ : (→ (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/macrotypes/examples/tests/rackunit-typechecking-fomega2.rkt b/macrotypes/examples/tests/rackunit-kindchecking.rkt
similarity index 100%
rename from macrotypes/examples/tests/rackunit-typechecking-fomega2.rkt
rename to macrotypes/examples/tests/rackunit-kindchecking.rkt
diff --git a/macrotypes/info.rkt b/macrotypes/info.rkt
index 11cb2be..f008017 100644
--- a/macrotypes/info.rkt
+++ b/macrotypes/info.rkt
@@ -1,13 +1,15 @@
 #lang info
 
 (define compile-omit-paths 
-  '("examples/tests"))
+  '("examples/fomega3.rkt"
+    "examples/tests"))
 
 (define test-include-paths
   '("examples/tests/mlish")) ; to include .mlish files
 
 (define test-omit-paths
   '("examples/tests/mlish/sweet-map.rkt" ; needs sweet-exp
+    "examples/tests/fomega3-tests.rkt"
     "examples/tests/mlish/bg/README.md"))
 
 (define test-timeouts
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
index b4b391a..983be89 100644
--- a/macrotypes/typecheck.rkt
+++ b/macrotypes/typecheck.rkt
@@ -211,7 +211,10 @@
   ;; If Val is a non-empty list, return first element, otherwise return Val.
   ;; e.g., Stx = expression, Tag = ':, Val = Type stx
   (define (detach stx tag)
-    (get-stx-prop/car stx tag)))
+;    (or
+     (get-stx-prop/car stx tag)
+;     (error 'detach "~a has no ~a prop" (stx->datum stx) tag))
+     ))
 
 ;; ----------------------------------------------------------------------------
 ;; define-syntax-category ------------------------------------------------------
diff --git a/turnstile/examples/fomega2.rkt b/turnstile/examples/fomega2.rkt
index 7b088c3..a107a37 100644
--- a/turnstile/examples/fomega2.rkt
+++ b/turnstile/examples/fomega2.rkt
@@ -1,5 +1,5 @@
 #lang turnstile/lang
-(extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst)
+(extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst λ #%app →)
 (reuse String #%datum #:from "stlc+reco+var.rkt")
 
 ; same as fomega.rkt except here λ and #%app works as both type and terms
@@ -17,31 +17,42 @@
 
 (provide define-type-alias
          ★ ∀★ ∀
-         Λ inst)
+         λ #%app → Λ inst
+         (for-syntax current-kind-eval kindcheck?))
 
-(define-syntax-category kind)
+(define-syntax-category :: kind)
 
 (begin-for-syntax
-  (current-kind? (λ (k) (or (#%type? k) (kind? k) (#%type? (typeof k)))))
+  (define old-kind? (current-kind?))
+  (current-kind? (λ (k) (or (#%type? k) (old-kind? k))))
   ;; Try to keep "type?" backward compatible with its uses so far,
   ;; eg in the definition of λ or previous type constuctors.
   ;; (However, this is not completely possible, eg define-type-alias)
   ;; 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) (or (type? t)
-                            (let ([k (typeof t)])
-                              (or (★? k) (∀★? k)))
-                            ((current-kind?) t)))))
+  (current-type? (λ (t) (define k (kindof 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))
+                        (and k ((current-kind?) k)))))
 
 ; must override
 (define-syntax define-type-alias
   (syntax-parser
     [(_ alias:id τ)
-     #:with (τ- k_τ) (infer+erase #'τ)
+     #:with (τ- _) (infer+erase #'τ #:tag '::)
      #'(define-syntax alias
          (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))]))
 
+;; extend → to serve as both type and kind
+(define-syntax (→ stx)
+  (syntax-parse stx
+    [(_ k:kind ...)                ; kind
+     (add-orig (mk-kind #'(sysf:→- k.norm ...)) stx)]
+    [(_ . tys) #'(sysf:→ . tys)])) ; type
+
 (define-base-kind ★)
 (define-kind-constructor ∀★ #:arity >= 0)
 (define-binding-type ∀ #:arr ∀★)
@@ -73,28 +84,62 @@
   
   (define old-type=? (current-type=?))
   (define (type=? t1 t2)
-    (or (and (★? t1) (#%type? t2))
-        (and (#%type? t1) (★? t2))
-        (and (syntax-parse (list t1 t2) #:datum-literals (:)
-               [((~∀ ([tv1 : k1]) tbody1)
-                 (~∀ ([tv2 : k2]) tbody2))
-                ((current-type=?) #'k1 #'k2)]
-               [_ #t])
-             (old-type=? t1 t2))))
+    (syntax-parse (list t1 t2) #:datum-literals (:)
+                  ;; TODO: compare tbody1 and tbody2
+     [((~∀ ([tv1 : k1]) tbody1)
+       (~∀ ([tv2 : k2]) tbody2))
+      ((current-kind=?) #'k1 #'k2)]
+     [_ (old-type=? t1 t2)]))
   (current-type=? type=?)
   (current=? type=?)
   (current-typecheck-relation type=?)
-  (current-check-relation type=?))
+  (current-check-relation type=?)
+
+  (define old-kind=? (current-kind=?))
+  (define (new-kind=? k1 k2)
+    (or (and (★? k1) (#%type? k2)) ; enables use of existing type defs
+        (and (#%type? k1) (★? k2))
+        (old-kind=? k1 k2)))
+  (current-kind=? new-kind=?)
+  (current-kindcheck-relation new-kind=?))
 
 (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 ...))]
+   #:do[(define old-check (current-check-relation))
+        (current-check-relation new-kind=?)]
+  [⊢ τ ≫ τ- ⇐ :: k] ...
+   #:do[(current-check-relation old-check)]
   #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
   --------
   [⊢ e- ⇒ τ-inst])
 
+;; extend λ to also work as a type
+;; must be define-typed-syntax because of default case
+;; so use explicit tag in first case
+(define-typed-syntax λ
+  [(_ bvs:kind-ctx τ) ≫ ; type
+   [[bvs.x ≫ X- :: bvs.kind] ... ⊢ τ ≫ τ- ⇒ :: k_res]
+   ------------
+   [⊢ (λ- (X- ...) τ-) ⇒ :: (→ bvs.kind ... k_res)]]
+  [(_ . rst) ≫
+   --- [≻ (sysf:λ . rst)]])  ; term
+
+;; extend #%app to also work as a type
+(define-typed-syntax #%app
+  [(_ τ_fn τ_arg ...) ≫ ; type
+   [⊢ τ_fn ≫ τ_fn- ⇒ :: (~→ k_in ... k_out)]
+   #:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
+                 (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])
+   #:do[(define old-check (current-check-relation))
+        (current-check-relation new-kind=?)]
+   [⊢ τ_arg ≫ τ_arg- ⇐ :: k_in] ...
+   #:do[(current-check-relation old-check)]
+   -------------
+   [⊢ (#%app- τ_fn- τ_arg- ...) ⇒ :: k_out]]
+  [(_ . rst) ≫
+   --- [≻ (sysf:#%app . rst)]]) ; term
diff --git a/turnstile/examples/tests/fomega2-tests.rkt b/turnstile/examples/tests/fomega2-tests.rkt
index a3eeaec..11dadfc 100644
--- a/turnstile/examples/tests/fomega2-tests.rkt
+++ b/turnstile/examples/tests/fomega2-tests.rkt
@@ -1,74 +1,76 @@
 #lang s-exp "../fomega2.rkt"
 (require "rackunit-typechecking.rkt")
+(require "rackunit-kindchecking.rkt")
 
-(check-type Int : ★)
-(check-type String : ★)
+(check-kind Int :: ★)
+(check-kind String :: ★)
 (typecheck-fail →)
-(check-type (→ Int Int) : ★)
+(check-kind (→ Int Int) :: ★)
 (typecheck-fail (→ →))
 (typecheck-fail (→ 1))
 (check-type 1 : Int)
 
 ;; this should error but it doesnt
-#;(λ ([x : ★]) 1)
+#;(λ ([x :: ★]) 1)
 
-;(check-type (∀ ([t : ★]) (→ t t)) : ★)
-(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
-(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
+;(check-type (∀ ([t :: ★]) (→ t t)) :: ★)
+(check-kind (∀ ([t :: ★]) (→ t t)) :: (∀★ ★))
+(check-kind (→ (∀ ([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 (λ ([t : ★]) t) : (→ ★ ★))
-(check-type (λ ([t : ★] [s : ★]) t) : (→ ★ ★ ★))
-(check-type (λ ([t : ★]) (λ ([s : ★]) t)) : (→ ★ (→ ★ ★)))
-(check-type (λ ([t : (→ ★ ★)]) t) : (→ (→ ★ ★) (→ ★ ★)))
-(check-type (λ ([t : (→ ★ ★ ★)]) t) : (→ (→ ★ ★ ★) (→ ★ ★ ★)))
-(check-type (λ ([arg : ★] [res : ★]) (→ arg res)) : (→ ★ ★ ★))
+;; tests for λ as a type
+(check-kind (λ ([t :: ★]) t) :: (→ ★ ★))
+(check-kind (λ ([t :: ★] [s :: ★]) t) :: (→ ★ ★ ★))
+(check-kind (λ ([t :: ★]) (λ ([s :: ★]) t)) :: (→ ★ (→ ★ ★)))
+(check-kind (λ ([t :: (→ ★ ★)]) t) :: (→ (→ ★ ★) (→ ★ ★)))
+(check-kind (λ ([t :: (→ ★ ★ ★)]) t) :: (→ (→ ★ ★ ★) (→ ★ ★ ★)))
+(check-kind (λ ([arg :: ★] [res :: ★]) (→ arg res)) :: (→ ★ ★ ★))
 
-(check-type ((λ ([t : ★]) t) Int) : ★)
-(check-type (λ ([x : ((λ ([t : ★]) t) Int)]) x) : (→ Int Int))
-(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
-(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
-(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
-(typecheck-fail ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
+(check-kind ((λ ([t :: ★]) t) Int) :: ★)
+(check-type (λ ([x : ((λ ([t :: ★]) t) Int)]) x) : (→ Int Int))
+(check-type ((λ ([x : ((λ ([t :: ★]) t) Int)]) x) 1) : Int ⇒ 1)
+(check-type ((λ ([x : ((λ ([t :: ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
+(check-type ((λ ([x : ((λ ([t :: ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
+(typecheck-fail ((λ ([x : ((λ ([t :: ★]) t) Int)]) (+ 1 x)) "a-string"))
 
 ;; partial-apply →
-(check-type ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)
-            : (→ ★ ★))
+(check-kind ((λ ([arg :: ★]) (λ ([res :: ★]) (→ arg res))) Int)
+            :: (→ ★ ★))
 ; f's type must have kind ★
-(typecheck-fail (λ ([f : ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)]) f))
-(check-type (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) :
-            (∀ ([tyf : (→ ★ ★)]) (→ (tyf String) (tyf String))))
+(typecheck-fail (λ ([f : ((λ ([arg :: ★]) (λ ([res :: ★]) (→ arg res))) Int)]) f))
+(check-type (Λ ([tyf :: (→ ★ ★)]) (λ ([f : (tyf String)]) f)) :
+            (∀ ([tyf :: (→ ★ ★)]) (→ (tyf String) (tyf String))))
 (check-type (inst
-             (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
-             ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+             (Λ ([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")
+ (inst (Λ ([X :: ★]) (λ ([x : X]) x)) 1)
+ #:with-msg "not a valid type: 1")
 
 ;; applied f too early
 (typecheck-fail (inst
-                 (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
-                 ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)))
+                 (Λ ([tyf :: (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
+                 ((λ ([arg :: ★]) (λ ([res :: ★]) (→ arg res))) Int)))
 (check-type ((inst
-              (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
-              ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+              (Λ ([tyf :: (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+              ((λ ([arg :: ★]) (λ ([res :: ★]) (→ arg res))) Int))
              (λ ([x : Int]) "int")) : (→ Int String))
 (check-type (((inst
-               (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
-              ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+               (Λ ([tyf :: (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+              ((λ ([arg :: ★]) (λ ([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 (λ ([X : ★]) X))
+(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))
 (check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int String) Int))
@@ -81,104 +83,104 @@
 (check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (Id (→ Int String))) Int))
 
 ;; tapl examples, p451
-(define-type-alias Pair (λ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
+(define-type-alias Pair (λ ([A :: ★] [B :: ★]) (∀ ([X :: ★]) (→ (→ A B X) X))))
 
-;(check-type Pair : (→ ★ ★ ★))
-(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 (Pair X Y))))
+ (Λ ([X :: ★] [Y :: ★]) (λ ([x : X][y : Y]) (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ : (∀ ([X :: ★][Y :: ★]) (→ X Y (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 (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")
  : (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 : ★]) (→ (Pair X Y) X)))
+ (Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ : (∀ ([X :: ★][Y :: ★]) (→ (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)
  : (→ (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 : ★]) (→ (Pair X Y) Y)))
+ (Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ : (∀ ([X :: ★][Y :: ★]) (→ (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)
  : (→ (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)))
+;; 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 (Λ ([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/examples/tests/rackunit-kindchecking.rkt b/turnstile/examples/tests/rackunit-kindchecking.rkt
new file mode 100644
index 0000000..3c28455
--- /dev/null
+++ b/turnstile/examples/tests/rackunit-kindchecking.rkt
@@ -0,0 +1,26 @@
+#lang racket/base
+(require (for-syntax rackunit syntax/srcloc) rackunit macrotypes/typecheck
+         (only-in "../fomega2.rkt" current-kind-eval kindcheck?))
+(provide check-kind)
+
+(define-syntax (check-kind stx)
+  (syntax-parse stx #:datum-literals (⇒ ->)
+    ;; duplicate code to avoid redundant expansions
+    #;[(_ τ tag:id k-expected (~or ⇒ ->) v)
+     #:with τ+ (expand/df #'(add-expected τ k-expected))
+     #:with k (detach #'e+ (stx->datum #'tag))
+     #:fail-unless (kindcheck? #'k ((current-kind-eval) #'k-expected))
+                   (format
+                    "Type ~a [loc ~a:~a] has kind ~a, expected ~a"
+                    (syntax->datum #'τ) (syntax-line #'τ) (syntax-column #'τ)
+                    (type->str #'k) (type->str #'k-expected))
+     (syntax/loc stx (check-equal? τ+ (add-expected v k-expected)))]
+    [(_ τ tag:id k-expected)
+     #:with k (detach (expand/df #'(add-expected τ k-expected)) (stx->datum #'tag))
+     #:fail-unless
+     (kindcheck? #'k ((current-kind-eval) #'k-expected))
+     (format
+      "Type ~a [loc ~a:~a] has kind ~a, expected ~a"
+      (syntax->datum #'τ) (syntax-line #'τ) (syntax-column #'τ)
+      (type->str #'k) (type->str #'k-expected))
+     #'(void)]))
diff --git a/turnstile/examples/trivial.rkt b/turnstile/examples/trivial.rkt
index f8d86c8..7ef6585 100644
--- a/turnstile/examples/trivial.rkt
+++ b/turnstile/examples/trivial.rkt
@@ -120,7 +120,8 @@
            ((current-type=?) t1 #'t2*)]
           [_ #f])))
   (current-type=? new-type=?)
-  (current-typecheck-relation (current-type=?))
+  (current-typecheck-relation new-type=?)
+  (current-check-relation new-type=?)
 
   ;; current-type?
   ;; TODO: disabling type validation for now
@@ -146,6 +147,7 @@
            ((current-type-eval) #'(CCs- a b c (Int (#%datum- . e-)))))]
       [_ t+]))
   (current-type-eval new-teval)
+  (current-ev new-teval)
 
   ;; type inference helpers ---------------------------------------------------
   ;; A "B" is a type binding, eg (X ty) or (ty X)
diff --git a/turnstile/info.rkt b/turnstile/info.rkt
index c90d1ed..daa8182 100644
--- a/turnstile/info.rkt
+++ b/turnstile/info.rkt
@@ -6,18 +6,18 @@
 (define compile-omit-paths 
   '("examples/rosette"
     "examples/tests"
-    "examples/trivial.rkt"))
+    "examples/fomega3.rkt"
+    "examples/trivial.rkt")) ; needs typed racket
 
 (define test-include-paths
   '("examples/tests/mlish")) ; to include .mlish files
 
 (define test-omit-paths
   '("examples/rosette"
-    "examples/tests/fomega2-tests.rkt"
-    "examples/tests/fomega3-tests.rkt"
     "examples/tests/rosette"             ; needs rosette
     "examples/tests/trivial-test.rkt"    ; needs typed/racket
     "examples/tests/mlish/sweet-map.rkt" ; needs sweet-exp
+    "examples/tests/fomega3-tests.rkt"
     "examples/tests/mlish/bg/README.md"))
 
 (define test-timeouts