diff --git a/macrotypes/examples/fomega.rkt b/macrotypes/examples/fomega.rkt
index edbe824..4dfeb83 100644
--- a/macrotypes/examples/fomega.rkt
+++ b/macrotypes/examples/fomega.rkt
@@ -1,5 +1,5 @@
 #lang s-exp macrotypes/typecheck
-(extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst)
+(extends "sysf.rkt" #:except #%datum ∀ ∀- ~∀ ∀? Λ inst)
 (reuse String #%datum #:from "stlc+reco+var.rkt")
 
 ;; System F_omega
diff --git a/macrotypes/examples/fomega2.rkt b/macrotypes/examples/fomega2.rkt
index cceb550..b8185b0 100644
--- a/macrotypes/examples/fomega2.rkt
+++ b/macrotypes/examples/fomega2.rkt
@@ -1,5 +1,5 @@
 #lang s-exp macrotypes/typecheck
-(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
@@ -16,23 +16,25 @@
 ;; - #%datum from stlc+reco+var
 
 (provide define-type-alias
-         ★ ∀★ ∀
-         Λ inst)
+         ★ ∀★ ∀ →
+         λ #%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
-  (current-kind? (λ (k) (or (#%type? k) (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)))))
+  (define old-kind? (current-kind?))
+  (current-kind? (λ (k) (or (#%type? k) (old-kind? k))))
+
+  ;; well-formed types, eg not types with kind →
+  ;; must allow kinds as types, for →
+  (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
@@ -42,6 +44,13 @@
      #'(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 ∀★)
@@ -72,30 +81,71 @@
   
   (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 (:)
+      [((~∀ ([tv1 : k1]) tbody1)
+        (~∀ ([tv2 : k2]) tbody2))
+       ((current-kind=?) #'k1 #'k2)]
+      [_ (old-type=? t1 t2)]))
   (current-type=? type=?)
-  (current-typecheck-relation (current-type=?)))
+  (current-typecheck-relation (current-type=?))
+
+  (define old-kind=? (current-kind=?))
+  (define (new-kind=? k1 k2)
+    (or (and (★? k1) (#%type? k2))
+        (and (#%type? k1) (★? k2))
+        (old-kind=? k1 k2)))
+  (current-kind=? new-kind=?)
+  (current-kindcheck-relation (current-kind=?)))
 
 (define-typed-syntax Λ
   [(_ bvs:kind-ctx e)
    #:with ((tv- ...) e- τ_e)
           (infer/ctx+erase #'bvs #'e)
-   (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
+   (⊢ e- : (∀ ([tv- :: bvs.kind] ...) τ_e))])
 
 (define-typed-syntax inst
-  [(_ e τ ...)
-   #:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀)
-   #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
-   #:when (stx-andmap 
-           (λ (t k) (or ((current-kind?) k)
-                        (type-error #:src t #:msg "not a valid type: ~a" t)))
-           #'(τ ...) #'(k_τ ...))
-   #:when (typechecks? #'(k_τ ...) #'(k ...))
-   (⊢ e- : #,(substs #'(τ- ...) #'(tv ...) #'τ_body))])
+  [(_ e τ:any-type ...)
+;   #:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀)
+   #:with [e- τ_e] (infer+erase #'e)
+   #:with (~∀ (tv ...) τ_body) #'τ_e
+   #:with (~∀★ k ...) (kindof #'τ_e)
+;   #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
+   #:with (k_τ ...) (stx-map kindof #'(τ.norm ...))
+   #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...))
+                 (typecheck-fail-msg/multi 
+                  #'(k ...) #'(k_τ ...) #'(τ ...))
+   #:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body)
+   (⊢ e- : τ_inst)])
+
+;; extend λ to also work as a type
+(define-typed-syntax λ
+  [(_ bvs:kind-ctx τ)           ; type
+   #:with (Xs- τ- k_res) (infer/ctx+erase #'bvs #'τ #:tag '::)
+   (⊢ (λ- Xs- τ-) :: (→ bvs.kind ... k_res))]
+  [(_ . rst) #'(sysf:λ . rst)]) ; term
+
+;; extend #%app to also work as a type
+(define-typed-syntax #%app
+  [(_ τ_fn τ_arg ...) ; type
+;   #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
+   #:with [τ_fn- k_fn] (infer+erase #'τ_fn #:tag '::)
+   #:when (syntax-e #'k_fn) ; non-false
+   #:with (~→ k_in ... k_out ~!) #'k_fn
+   #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...) #:tag '::)
+   #:fail-unless (kindchecks? #'(k_arg ...) #'(k_in ...))
+                 (string-append
+                  (format 
+                   "~a (~a:~a) Arguments to function ~a have wrong kinds(s), "
+                   (syntax-source stx) (syntax-line stx) (syntax-column stx)
+                   (syntax->datum #'τ_fn))
+                  "or wrong number of arguments:\nGiven:\n"
+                  (string-join
+                   (map (λ (e t) (format "  ~a : ~a" e t)) ; indent each line
+                        (syntax->datum #'(τ_arg ...))
+                        (stx-map type->str #'(k_arg ...)))
+                   "\n" #:after-last "\n")
+                  (format "Expected: ~a arguments with type(s): "
+                          (stx-length #'(k_in ...)))
+                  (string-join (stx-map type->str #'(k_in ...)) ", "))
+   (⊢ (#%app- τ_fn- τ_arg- ...) :: k_out)]
+  [(_ . rst) #'(sysf:#%app . rst)]) ; term
diff --git a/macrotypes/examples/tests/fomega2-tests.rkt b/macrotypes/examples/tests/fomega2-tests.rkt
index a3eeaec..78ab66c 100644
--- a/macrotypes/examples/tests/fomega2-tests.rkt
+++ b/macrotypes/examples/tests/fomega2-tests.rkt
@@ -1,10 +1,11 @@
 #lang s-exp "../fomega2.rkt"
 (require "rackunit-typechecking.rkt")
+(require "rackunit-typechecking-fomega2.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)
@@ -12,63 +13,64 @@
 ;; this should error but it doesnt
 #;(λ ([x : ★]) 1)
 
-;(check-type (∀ ([t : ★]) (→ t t)) : ★)
-(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
-(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
+;(check-kind (∀ ([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)) : (→ ★ ★ ★))
+;; λ 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))
+ (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,105 @@
 (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-kind 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)))
+(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/macrotypes/examples/tests/rackunit-typechecking-fomega2.rkt b/macrotypes/examples/tests/rackunit-typechecking-fomega2.rkt
new file mode 100644
index 0000000..3c28455
--- /dev/null
+++ b/macrotypes/examples/tests/rackunit-typechecking-fomega2.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/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
index 240877f..e545bb5 100644
--- a/macrotypes/typecheck.rkt
+++ b/macrotypes/typecheck.rkt
@@ -54,7 +54,8 @@
     [(_ . stuff)
      (syntax/loc this-syntax
        (#%module-begin
-        (provide #%module-begin #%top-interaction #%top require only-in) ; useful racket forms
+        ; provide some useful racket forms
+        (provide #%module-begin #%top-interaction #%top require only-in)
         . stuff))]))
 
 (struct exn:fail:type:runtime exn:fail:user ())
@@ -401,9 +402,10 @@
                 [(_ . ts)
                  #:with t-expanders (stx-map mk-~ #'ts)
                  #:with t?s (stx-map mk-? #'ts)
+                 #:with t-s (filter identifier-binding (stx-map mk-- #'ts))
                  (expand-export
                   (syntax/loc stx (combine-out
-                                   (combine-out . ts)
+                                   (combine-out . ts) (combine-out . t-s)
                                    (for-syntax (combine-out . t-expanders) . t?s)))
                   modes)]))))
          (define-syntax define-base-type
diff --git a/turnstile/examples/fomega.rkt b/turnstile/examples/fomega.rkt
index 00e8309..6746138 100644
--- a/turnstile/examples/fomega.rkt
+++ b/turnstile/examples/fomega.rkt
@@ -1,5 +1,5 @@
 #lang turnstile/lang
-(extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst)
+(extends "sysf.rkt" #:except #%datum ∀ ∀- ~∀ ∀? Λ inst)
 (reuse String #%datum #:from "stlc+reco+var.rkt")
 
 ;; System F_omega
diff --git a/turnstile/examples/tests/rackunit-typechecking.rkt b/turnstile/examples/tests/rackunit-typechecking.rkt
index 4c60084..356618c 100644
--- a/turnstile/examples/tests/rackunit-typechecking.rkt
+++ b/turnstile/examples/tests/rackunit-typechecking.rkt
@@ -4,6 +4,7 @@
          check-equal/rand
          (rename-out [typecheck-fail check-stx-err]))
 
+
 (begin-for-syntax
   (define (add-esc s) (string-append "\\" s))
   (define escs (map add-esc '("(" ")" "[" "]")))