diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
index 331b346..1a84d10 100644
--- a/tapl/fomega.rkt
+++ b/tapl/fomega.rkt
@@ -22,10 +22,17 @@
 
 (define-syntax-category kind)
 (begin-for-syntax
-  (current-type? (λ (t) (or (type? t) (kind? (typeof t))))))
+  (current-kind? (λ (k) (or (#%type? k) (kind? k))))
+  ;; Try to keep "type?" remain 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) (★? (typeof t)) (∀★? (typeof t)) #;(kind? (typeof t))))))
 
-#;(provide define-type-alias)
-#;(define-syntax define-type-alias
+; must override
+(provide define-type-alias)
+(define-syntax define-type-alias
   (syntax-parser
     [(_ alias:id τ)
      #:with (τ- k_τ) (infer+erase #'τ)
@@ -33,18 +40,6 @@
      #'(define-syntax alias (syntax-parser [x:id #'τ-]))]))
 
 (begin-for-syntax
-  (define (type=? t1 t2)
-    (printf "t1 = ~a\n" (syntax->datum t1))
-    (printf "t2 = ~a\n" (syntax->datum t2))
-    (and (syntax-parse (list t1 t2) #:datum-literals (:)
-          [((~∀ ([tv1 : k1] ...) tbody1)
-            (~∀ ([tv2 : k2] ...) tbody2))
-           #:when (displayln "here")
-           (types=? #'(k1 ...) #'(k2 ...))]
-           [_ #t])
-         (sysf:type=? t1 t2)))
-  (current-type=? type=?)
-  (current-typecheck-relation (current-type=?))
   ;; extend type-eval to handle tyapp
   ;; - requires manually handling all other forms
   (define (type-eval τ)
@@ -72,6 +67,7 @@
 
 (define-base-kind ★)
 (define-kind-constructor ⇒ #:arity >= 1)
+(define-kind-constructor ∀★ #:arity >= 0)
 
 ;; for now, handle kind checking in the types themselves
 ;; TODO: move kind checking to a common place (like #%app)?
@@ -102,28 +98,29 @@
      #:with (tvs- τ_body- k_body) (infer/ctx+erase #'(b ...) #'τ_body)
      #:when (★? #'k_body)
      (⊢ (λ tvs- b.tag ... τ_body-) : ★)]))
+
 (define-syntax (∀ stx)
   (syntax-parse stx
     [(_ bvs:kind-ctx τ_body)
-;     #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body)
-;     #:when (★? #'k_body)
-     #:when (displayln ((current-type-eval) #'(sysf:∀ (bvs.x ...) τ_body)))
-     (⊢ #,((current-type-eval) #'(sysf:∀ (bvs.x ...) τ_body)) : (⇒ bvs.kind ...))]))
+     ;; cant re-use the expansion in sysf:∀ because it will give the bvs kind #%type
+     #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
+     ; expand so kind gets overwritten
+     (⊢ #,((current-type-eval) #'(sysf:∀ tvs- τ_body-)) : (∀★ bvs.kind ...))]))
 ;    (⊢ (λ tvs- b.tag ... τ_body-) : ★)]))
 (begin-for-syntax
   (define-syntax ~∀
     (pattern-expander
      (syntax-parser #:datum-literals (:)
        [(_ ([tv:id : k] ...) τ)
-        #:when (displayln "pat expand")
         #:with ∀τ (generate-temporary)
         #'(~and ∀τ
                 (~parse (~sysf:∀ (tv ...) τ) #'∀τ)
-                (~parse (~⇒ k ...) (typeof #'∀τ)))]
+                (~parse (~∀★ k ...) (typeof #'∀τ)))]
        [(_ . args)
+        #:with ∀τ (generate-temporary)
         #'(~and ∀τ
                 (~parse (~sysf:∀ (tv (... ...)) τ) #'∀τ)
-                (~parse (~⇒ k (... ...)) (typeof #'∀τ))
+                (~parse (~∀★ k (... ...)) (typeof #'∀τ))
                 (~parse args #'(([tv k] (... ...)) τ)))])))
   (define-syntax ~∀*
     (pattern-expander
@@ -134,7 +131,20 @@
            (~and any (~do
                       (type-error
                        #:src #'any
-                       #:msg "Expected ∀ type, got: ~a" #'any))))]))))
+                       #:msg "Expected ∀ type, got: ~a" #'any))))])))
+   (define (type=? t1 t2)
+    ;(printf "t1 = ~a\n" (syntax->datum t1))
+    ;(printf "t2 = ~a\n" (syntax->datum t2))
+     (or (and (★? t1) (#%type? t2))
+         (and (#%type? t1) (★? t2))
+         (and (syntax-parse (list t1 t2) #:datum-literals (:)
+                [((~∀ ([tv1 : k1]) tbody1)
+                  (~∀ ([tv2 : k2]) tbody2))
+                 (type=? #'k1 #'k2)]
+                [_ #t])
+              (sysf:type=? t1 t2))))
+  (current-type=? type=?)
+  (current-typecheck-relation (current-type=?)))
 
 #;(define-syntax (Λ stx)
   (syntax-parse stx
@@ -144,7 +154,7 @@
 (define-syntax (Λ stx)
   (syntax-parse stx
     [(_ bvs:kind-ctx e)
-     #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e)
+     #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
      (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))]))
 #;(define-syntax (inst stx)
   (syntax-parse stx
@@ -162,10 +172,13 @@
      (⊢ e- : #,(substs #'(τ ...) #'(tv ...) #'τ_body))]))
 (define-syntax (inst stx)
   (syntax-parse stx
-    [(_ e τ:type ...)
+    [(_ e τ ...)
      #:with (e- (([tv k] ...) τ_body)) (⇑ e as ∀)
      #:with ([τ- k_τ] ...) (infers+erase #'(τ ...) #:expand (current-type-eval))
-     #:when (typechecks? (stx-map typeof #'(k_τ ...)) #'(k ...))
+     #: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))]))
 
 ;; TODO: merge with regular λ and app?
@@ -173,6 +186,7 @@
   (syntax-parse stx 
     [(_ bvs:kind-ctx τ_body)
      #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
+     #:when ((current-kind?) #'k_body)
      (⊢ (λ tvs- τ_body-) : (⇒ bvs.kind ... k_body))]))
 #;(define-syntax (tyλ stx)
   (syntax-parse stx 
diff --git a/tapl/tests/fomega-tests.rkt b/tapl/tests/fomega-tests.rkt
index 36fca42..24aec02 100644
--- a/tapl/tests/fomega-tests.rkt
+++ b/tapl/tests/fomega-tests.rkt
@@ -1,204 +1,205 @@
 #lang s-exp "../fomega.rkt"
 (require "rackunit-typechecking.rkt")
 
-;(check-type Int : ★)
-(check-type Int : #%type)
-;(check-type String : ★)
-(check-type String : #%type)
+(check-type Int : ★)
+(check-type String : ★)
 (typecheck-fail →)
-;(check-type (→ Int Int) : ★)
-(check-type (→ Int Int) : #%type)
+(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 (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : #%type)
+(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)))
-((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (⇒ ★ ★)]) (λ ([x : X]) x)))
 (typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (⇒ ★ ★)]) (λ ([x : X]) x))))
 
-;(check-type (tyλ ([t : ★]) t) : (⇒ ★ ★))
-;(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★))
-;(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★)))
-;(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★)))
-;(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
-;(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★))
-;
-;(check-type (tyapp (tyλ ([t : ★]) t) Int) : ★)
-;(check-type (λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) : (→ Int Int))
-;(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
-;(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
-;(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
-;(typecheck-fail ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
-;
-;;; partial-apply →
-;(check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)
-;            : (⇒ ★ ★))
+(check-type (tyλ ([t : ★]) t) : (⇒ ★ ★))
+(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★))
+(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★)))
+(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★)))
+(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
+(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★))
+
+(check-type (tyapp (tyλ ([t : ★]) t) Int) : ★)
+(check-type (λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) : (→ Int Int))
+(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
+(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
+(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
+(typecheck-fail ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
+
+;; partial-apply →
+(check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)
+            : (⇒ ★ ★))
 ;; f's type must have kind ★
-;(typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f))
-;(check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) :
-;            (∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String))))
-;(check-type (inst
-;             (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
-;             (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
-;            : (→ (→ Int String) (→ Int String)))
-;(typecheck-fail
-; (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1)
-; #:with-msg "not a valid type: 1")
-;
-;;; applied f too early
-;(typecheck-fail (inst
-;                 (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
-;                 (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)))
-;(check-type ((inst
-;              (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
-;              (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
-;             (λ ([x : Int]) "int")) : (→ Int String))
-;(check-type (((inst
-;               (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
-;              (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
-;              (λ ([x : Int]) "int")) 1) : String ⇒ "int")
-;
-;;; tapl examples, p441
-;(typecheck-fail
-; (define-type-alias tmp 1)
-; #:with-msg "not a valid type: 1")
-;(define-type-alias Id (tyλ ([X : ★]) X))
-;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
-;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int))
-;(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int))
-;(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int (tyapp Id String)) Int))
-;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) (tyapp Id String)) Int))
-;(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) String) Int))
-;(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (→ Int String) Int))
-;(check-type (λ ([f : (→ Int String)]) 1) : (→ (tyapp Id (→ Int String)) Int))
-;(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (→ Int String)) Int))
-;(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int))
-;
-;;; tapl examples, p451
-;(define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
-;
+(typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f))
+(check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) :
+            (∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String))))
+(check-type (inst
+             (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+             (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+            : (→ (→ Int String) (→ Int String)))
+(typecheck-fail
+ (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1)
+ #:with-msg "not a valid type: 1")
+
+(typecheck-fail
+ (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
+ #:with-msg "Expected expression f to have → type")
+;; applied f too early
+(typecheck-fail
+ (inst
+  (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
+  (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+ #:with-msg "Expected expression f to have → type")
+(check-type ((inst
+              (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+              (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+             (λ ([x : Int]) "int")) : (→ Int String))
+(check-type (((inst
+               (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+              (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+              (λ ([x : Int]) "int")) 1) : String ⇒ "int")
+
+;; tapl examples, p441
+(typecheck-fail
+ (define-type-alias tmp 1)
+ #:with-msg "not a valid type: 1")
+(define-type-alias Id (tyλ ([X : ★]) X))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int))
+(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int (tyapp Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) (tyapp Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) String) Int))
+(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (tyapp Id (→ Int String)) Int))
+(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (→ Int String)) Int))
+(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int))
+
+;; tapl examples, p451
+(define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
+
 ;(check-type Pair : (⇒ ★ ★ ★))
-;
-;(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
-;; parametric pair constructor
-;(check-type
-; (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
-; : (∀ ([X : ★][Y : ★]) (→ X Y (tyapp Pair X Y))))
-;; concrete Pair Int String constructor
-;(check-type
-; (inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
-;       Int String)
-; : (→ Int String (tyapp Pair Int String)))
+(check-type Pair : (⇒ ★ ★ (∀★ ★)))
+
+(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
+; parametric pair constructor
+(check-type
+ (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ : (∀ ([X : ★][Y : ★]) (→ X Y (tyapp Pair X Y))))
+; concrete Pair Int String constructor
+(check-type
+ (inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+       Int String)
+ : (→ Int String (tyapp Pair Int String)))
 ;; Pair Int String value
-;(check-type
-; ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
-;       Int String) 1 "1")
-; : (tyapp Pair Int String))
+(check-type
+ ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+       Int String) 1 "1")
+ : (tyapp Pair Int String))
 ;; fst: parametric
-;(check-type
-; (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
-; : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) X)))
+(check-type
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) X)))
 ;; fst: concrete Pair Int String accessor
-;(check-type
-; (inst
-;  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
-;  Int String)
-; : (→ (tyapp Pair Int String) Int))
+(check-type
+ (inst
+  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+  Int String)
+ : (→ (tyapp Pair Int String) Int))
 ;; apply fst
-;(check-type
-; ((inst
-;   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
-;   Int String)
-;  ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
-;         Int String) 1 "1"))
-; : Int ⇒ 1)
+(check-type
+ ((inst
+   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+   Int String)
+  ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+         Int String) 1 "1"))
+ : Int ⇒ 1)
 ;; snd
-;(check-type
-; (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
-; : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) Y)))
-;(check-type
-; (inst
-;  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
-;  Int String)
-; : (→ (tyapp Pair Int String) String))
-;(check-type
-; ((inst
-;   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
-;   Int String)
-;  ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
-;         Int String) 1 "1"))
-; : String ⇒ "1")
-;
-;;;; sysf tests wont work, unless augmented with kinds
-;(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
-;
-;(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
-;(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
-;(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
-;
-;(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
-;            : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
-;
-;(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
-;            : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
-;
-;(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
-;            : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
-;
-;(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
-;(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
-;; first inst should be discarded
-;(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
-;; second inst is discarded
-;(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
-;
-;;; polymorphic arguments
-;(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
-;(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
-;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
-;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
-;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
-;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
-;(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
-;(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
-;(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
-;(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
-;(check-type
-; (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
-;(check-type
-; ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
-; : Int ⇒ 10)
-;(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
-;(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
-;(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
-;             (Λ ([s : ★]) (λ ([y : s]) y)))
-;             : Int ⇒ 10)
-;
-;
-;;; previous tests -------------------------------------------------------------
-;(check-type 1 : Int)
-;(check-not-type 1 : (→ Int Int))
+(check-type
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) Y)))
+(check-type
+ (inst
+  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+  Int String)
+ : (→ (tyapp Pair Int String) String))
+(check-type
+ ((inst
+   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+   Int String)
+  ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+         Int String) 1 "1"))
+ : String ⇒ "1")
+
+;; sysf tests wont work, unless augmented with kinds
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
+
+(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
+
+(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
+
+(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
+
+(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
+(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
+; first inst should be discarded
+(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
+; second inst is discarded
+(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
+
+;; polymorphic arguments
+(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
+(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
+(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
+(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
+(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
+(check-type
+ (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
+(check-type
+ ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
+ : Int ⇒ 10)
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
+(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
+             (Λ ([s : ★]) (λ ([y : s]) y)))
+             : Int ⇒ 10)
+
+
+;; previous tests -------------------------------------------------------------
+(check-type 1 : Int)
+(check-not-type 1 : (→ Int Int))
 ;(typecheck-fail #f) ; unsupported literal
-;(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
-;(check-not-type (λ ([x : Int]) x) : Int)
-;(check-type (λ ([x : Int]) x) : (→ Int Int))
-;(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
-;(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
-;(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
-;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
-;(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
-;(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
-;            : (→ (→ Int Int Int) Int Int Int))
-;(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
-;(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
-;(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
-;(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
-;(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
+(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
+            : (→ (→ Int Int Int) Int Int Int))
+(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index e64fd1f..8122f1a 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -11,7 +11,7 @@
  (for-syntax (all-defined-out)) (all-defined-out)
  (for-syntax
   (all-from-out racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt"))
- (for-meta 2 (all-from-out racket/base syntax/parse)))
+ (for-meta 2 (all-from-out racket/base syntax/parse racket/syntax)))
 
 ;; type checking functions/forms
 
@@ -122,12 +122,12 @@
                      #'(τ_e (... ...)))
             #'res])]))
   ;; infers the type and erases types in an expression
-  (define (infer+erase e)
-    (define e+ (expand/df e))
+  (define (infer+erase e #:expand [expand-fn expand/df])
+    (define e+ (expand-fn e))
     (list e+ (typeof e+)))
   ;; infers the types and erases types in multiple expressions
-  (define (infers+erase es)
-    (stx-map infer+erase es))
+  (define (infers+erase es #:expand [expand-fn expand/df])
+    (stx-map (λ (e) (infer+erase e #:expand expand-fn)) 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.
@@ -137,7 +137,7 @@
   ;; the types before typechecking, which is acceptable
   (define (infer es #:ctx [ctx null] #:tvctx [tvctx null]
                  #:octx [octx tvctx] #:tag [tag 'unused]
-                 #:expand [expand expand/df])
+                 #:expand [expand-fn expand/df])
     (syntax-parse ctx #:datum-literals (:)
       [([x : τ] ...) ; dont expand yet bc τ may have references to tvs
        #:with ([tv : k] ...) tvctx
@@ -158,16 +158,18 @@
           ((~literal #%plain-lambda) xs+
            ((~literal let-values) () ((~literal let-values) ()
             ((~literal #%expression) e+) ... (~literal void))))))))
-       (expand
+       (expand-fn
         #`(λ (tv ...)
             (let-syntax ([tv (make-rename-transformer (assign-type (assign-type #'tv #'k) #'ok #:tag '#,tag))] ...)
               (λ (x ...)
                 (let-syntax ([x (make-rename-transformer (assign-type #'x #'τ))] ...)
                   (#%expression e) ... void)))))
-       ;#:when (stx-map displayln #'(e+ ...))
-           ;   #:when (displayln (stx-map typeof #'(e+ ...)))
+;       #:when (stx-map displayln #'(e+ ...))
+;       #:when (displayln (stx-map typeof #'(e+ ...)))
        (list #'tvs+ #'xs+ #'(e+ ...)
-             (stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
+             (stx-map ; check is when trying to combine #%type and kinds
+              (λ (t) (or (false? t) (syntax-local-introduce t)))
+              (stx-map typeof #'(e+ ...))))]
       [([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvctx tvctx)]))
 
   ;; fns derived from infer ---------------------------------------------------
@@ -176,11 +178,11 @@
   ;; shorter names
   ; ctx = type env for bound vars in term e, etc
   ; can also use for bound tyvars in type e
-  (define (infer/ctx+erase ctx e)
-    (syntax-parse (infer (list e) #:ctx ctx)
+  (define (infer/ctx+erase ctx e #:expand [expand-fn expand/df])
+    (syntax-parse (infer (list e) #:ctx ctx #:expand expand-fn)
       [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
-  (define (infers/ctx+erase ctx es #:expand [expand expand/df])
-    (stx-cdr (infer es #:ctx ctx #:expand expand)))
+  (define (infers/ctx+erase ctx es #:expand [expand-fn expand/df])
+    (stx-cdr (infer es #:ctx ctx #:expand expand-fn)))
   ; tyctx = kind env for bound type vars in term e
   (define (infer/tyctx+erase ctx e)
     (syntax-parse (infer (list e) #:tvctx ctx)
@@ -313,54 +315,54 @@
 #;(define #%type void)
 #;(define-for-syntax (mk-type t) (assign-type t #'#%type))
 
-#;(define-syntax (define-base-type stx)
-  (syntax-parse stx
-    [(_ τ:id)
-     #:with τ? (format-id #'τ "~a?" #'τ)
-     #:with τ-internal (generate-temporary #'τ)
-     #:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
-     #:with τ-cls (generate-temporary #'τ)
-     #:with τ-expander (format-id #'τ "~~~a" #'τ)
-     #'(begin
-         (provide τ (for-syntax τ? inferτ+erase τ-expander))
-         (define τ-internal
-           (λ () (raise (exn:fail:type:runtime
-                         (format "~a: Cannot use type at run time" 'τ)
-                         (current-continuation-marks)))))
-         (define-syntax (τ stx)
-           (syntax-parse stx
-             [x:id (add-orig #'(#%type (τ-internal)) #'τ)]))
-         (begin-for-syntax
-           ; expanded form of τ
-           (define-syntax-class τ-cls
-             (pattern ((~literal #%plain-type) ((~literal #%plain-app) ty))))
-           (define (τ? t)
-             (syntax-parse ((current-type-eval) t)
-               [expanded-type
-                #:declare expanded-type τ-cls
-                (typecheck? #'expanded-type.ty #'τ-internal)]))
-           ; base type pattern expanders should be identifier macros but
-           ; parsing them is ambiguous, so handle and pass through other args
-           (define-syntax τ-expander
-             (pattern-expander
-              (syntax-parser
-                [ty:id #'((~literal #%plain-type)
-                          ((~literal #%plain-app)
-                           (~literal τ-internal)))]
-                [(_ . rst)
-                 #'(((~literal #%plain-type)
-                     ((~literal #%plain-app)
-                      (~literal τ-internal))) . rst)])))
-           (define (inferτ+erase e)
-             (syntax-parse (infer+erase e) #:context e
-               [(e- expanded-type)
-                #:declare expanded-type τ-cls
-                #:fail-unless (typecheck? #'expanded-type.ty #'τ-internal)
-                              (format
-                               "~a (~a:~a): Expected type of expression ~v to be ~a, got: ~a"
-                               (syntax-source e) (syntax-line e) (syntax-column e)
-                               (syntax->datum e) (type->str #'τ) (type->str #'expanded-type))
-                #'e-]))))]))
+;#;(define-syntax (define-base-type stx)
+;  (syntax-parse stx
+;    [(_ τ:id)
+;     #:with τ? (format-id #'τ "~a?" #'τ)
+;     #:with τ-internal (generate-temporary #'τ)
+;     #:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
+;     #:with τ-cls (generate-temporary #'τ)
+;     #:with τ-expander (format-id #'τ "~~~a" #'τ)
+;     #'(begin
+;         (provide τ (for-syntax τ? inferτ+erase τ-expander))
+;         (define τ-internal
+;           (λ () (raise (exn:fail:type:runtime
+;                         (format "~a: Cannot use type at run time" 'τ)
+;                         (current-continuation-marks)))))
+;         (define-syntax (τ stx)
+;           (syntax-parse stx
+;             [x:id (add-orig #'(#%type (τ-internal)) #'τ)]))
+;         (begin-for-syntax
+;           ; expanded form of τ
+;           (define-syntax-class τ-cls
+;             (pattern ((~literal #%plain-type) ((~literal #%plain-app) ty))))
+;           (define (τ? t)
+;             (syntax-parse ((current-type-eval) t)
+;               [expanded-type
+;                #:declare expanded-type τ-cls
+;                (typecheck? #'expanded-type.ty #'τ-internal)]))
+;           ; base type pattern expanders should be identifier macros but
+;           ; parsing them is ambiguous, so handle and pass through other args
+;           (define-syntax τ-expander
+;             (pattern-expander
+;              (syntax-parser
+;                [ty:id #'((~literal #%plain-type)
+;                          ((~literal #%plain-app)
+;                           (~literal τ-internal)))]
+;                [(_ . rst)
+;                 #'(((~literal #%plain-type)
+;                     ((~literal #%plain-app)
+;                      (~literal τ-internal))) . rst)])))
+;           (define (inferτ+erase e)
+;             (syntax-parse (infer+erase e) #:context e
+;               [(e- expanded-type)
+;                #:declare expanded-type τ-cls
+;                #:fail-unless (typecheck? #'expanded-type.ty #'τ-internal)
+;                              (format
+;                               "~a (~a:~a): Expected type of expression ~v to be ~a, got: ~a"
+;                               (syntax-source e) (syntax-line e) (syntax-column e)
+;                               (syntax->datum e) (type->str #'τ) (type->str #'expanded-type))
+;                #'e-]))))]))
 
 (define-syntax define-basic-checked-id-stx
   (syntax-parser #:datum-literals (:)
@@ -373,7 +375,7 @@
      #'(begin
          (provide τ (for-syntax τ? τ-expander))
          (begin-for-syntax
-           (define (τ? t) (typecheck? t #'τ-internal))
+           (define (τ? t) (and (identifier? t) (free-identifier=? t #'τ-internal)))
            (define (inferτ+erase e)
              (syntax-parse (infer+erase e) #:context e
                [(e- e_τ)
@@ -430,10 +432,9 @@
                          #,(if (attribute has-bvs?)
                                #'(~parse pat #'(bvs rst))
                                #'(~parse pat #'rst)))]
-                [(_ (~optional (~and (~fail #:unless #,(attribute has-bvs?))
-                                  (bv (... ...)))
-                            #:defaults ([(bv 1) null])) . pat)
-                 #'((~literal #%plain-lambda) (bv (... ...))
+                [(_ (~optional (~and (~fail #:unless #,(attribute has-bvs?)) bvs-pat)
+                               #:defaults ([bvs-pat #'()])) . pat)
+                 #'((~literal #%plain-lambda) bvs-pat
                     ((~literal #%plain-app) (~literal τ-internal) . pat))])))
            (define-syntax τ-expander*
              (pattern-expander
@@ -453,7 +454,8 @@
              (and (stx-pair? t)
                   (syntax-parse t
                     [((~literal #%plain-lambda) bvs ((~literal #%plain-app) tycon . _))
-                     (typecheck? #'tycon #'τ-internal)]))))
+                     (typecheck? #'tycon #'τ-internal)]
+                    [_ #f]))))
 ;           #;(define (τ-get t)
 ;             (syntax-parse t
 ;               [(τ-expander . pat) #'pat]))
@@ -918,7 +920,7 @@
                   #%tag define-base-name define-name-cons)
          (define #%tag void)
          (begin-for-syntax
-           (define (#%tag? t) (typecheck? t #'#%tag))
+           (define (#%tag? t) (and (identifier? t) (free-identifier=? t #'#%tag)))
            (define (is-name? t) (#%tag? (typeof t)))
            (define current-is-name? (make-parameter is-name?))
            (define (mk-name t) (assign-type t #'#%tag))