diff --git a/tapl/README.md b/tapl/README.md
index ec323b8..b71360e 100644
--- a/tapl/README.md
+++ b/tapl/README.md
@@ -12,4 +12,4 @@ A file extends its immediate parent file.
      - stlc+sub.rkt
        - stlc+rec+sub.rkt (also pull in tup from stlc+var.rkt)
      - sysf.rkt
-       - Fomega.rkt
\ No newline at end of file
+       - fomega.rkt
\ No newline at end of file
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
index 919bd7d..1887886 100644
--- a/tapl/fomega.rkt
+++ b/tapl/fomega.rkt
@@ -1,13 +1,117 @@
 #lang racket/base
 (require "typecheck.rkt")
-(require (except-in "sysf.rkt" #%app)
-         (prefix-in stlc: (only-in "sysf.rkt" #%app)))
-(provide (rename-out [stlc:#%app #%app]))
-(provide (except-out (all-from-out "sysf.rkt") stlc:#%app))
- 
+(require (except-in "sysf.rkt" #%app λ + Λ inst Int → ∀ eval-τ type=?)
+         (prefix-in sysf: (only-in "sysf.rkt" Int → ∀ eval-τ type=?)))
+(provide (rename-out [app/tc #%app] [λ/tc λ]))
+(provide (except-out (all-from-out "sysf.rkt")
+                     sysf:Int sysf:→ sysf:∀
+                     (for-syntax sysf:type=? sysf:eval-τ)))
+(provide Int → ∀ inst Λ
+         (for-syntax eval-τ type=?))
+
 ;; System F_omega
 ;; Type relation:
 ;; Types:
 ;; - types from sysf.rkt
 ;; Terms:
 ;; - terms from sysf.rkt
+
+(begin-for-syntax
+  ;; Extend to handle ∀ with type annotations
+  (define (eval-τ τ [tvs #'()])
+    (syntax-parse τ
+      [((~literal ∀) (b:typed-binding ...) t-body)
+       #`(∀ (b ...) #,((current-τ-eval) #'t-body (stx-append tvs #'(b.x ...))))]
+      ;; need to manually handle type constructors now since they are macros
+      [((~literal →) t ...)
+       #`(→ #,@(stx-map (λ (ty) ((current-τ-eval) ty tvs)) #'(t ...)))]
+      [_ (sysf:eval-τ τ tvs)]))
+  (current-τ-eval eval-τ)
+
+  ;; extend to handle ∀ with kind annotations
+  (define (type=? τ1 τ2)
+    (syntax-parse (list τ1 τ2) #:literals (∀)
+      [((∀ (a:typed-binding ...) t1:type) (∀ (b:typed-binding ...) t2:type))
+       #:when (= (stx-length #'(a ...)) (stx-length #'(b ...)))
+       #:with (z ...) (generate-temporaries #'(a ...))
+       #:when (typechecks? #'(a.τ ...) #'(b.τ ...))
+       ((current-type=?) (substs #'(z ...) #'(a.x ...) #'t1)
+                         (substs #'(z ...) #'(b.x ...) #'t2))]
+      [_ (sysf:type=? τ1 τ2)]))
+  (current-type=? type=?)
+  (current-typecheck-relation type=?))
+
+(define-base-type ★)
+(define-type-constructor ⇒)
+
+;; for now, handle kind checking in the types themselves
+;; TODO: move kind checking to a common place (like #%app)?
+;; when expanding: check and erase kinds
+
+(define-syntax Int (syntax-parser [x:id (⊢ #'sysf:Int #'★)]))
+
+;; → in Fω is not first-class, can't pass it around
+(define-syntax (→ stx)
+  (syntax-parse stx
+    [(_ τ ... τ_res)
+     #:with ([τ- k] ... [τ_res- k_res]) (infers+erase #'(τ ... τ_res))
+     #:when (typecheck? #'k_res #'★)
+     #:when (same-types? #'(k ... k_res))
+     (⊢ #'(sysf:→ τ-  ... τ_res-) #'★)]))
+
+(define-syntax (∀ stx)
+  (syntax-parse stx
+    [(∀ (b:typed-binding ...) τ)
+     #:with (tvs- τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
+     #:when (typecheck? #'k #'★)
+     (⊢ #'(sysf:∀ tvs- τ-) #'★)]))
+     
+(define-syntax (Λ stx)
+  (syntax-parse stx
+    [(_ (b:typed-binding ...) e)
+     #:with ((tv- ...) e- τ) (infer/type-ctxt+erase #'(b ...) #'e)
+     (⊢ #'e- #'(∀ ([tv- : b.τ] ...) τ))]))
+(define-syntax (inst stx)
+  (syntax-parse stx
+    [(_ e τ ...)
+     #:with ([τ- k] ...) (infers+erase #'(τ ...))
+     #:with (e- τ_e) (infer+erase #'e)
+     #:with ((~literal ∀) (b:typed-binding ...) τ_body) #'τ_e
+     #:when (typechecks? #'(k ...) #'(b.τ ...))
+     (⊢ #'e- (substs #'(τ ...) #'(b.x ...) #'τ_body))]))
+
+;; must override #%app and λ and primops to use new →
+;; TODO: parameterize →?
+
+(define-primop + : (→ Int Int Int))
+
+(define-syntax (λ/tc stx)
+  (syntax-parse stx 
+    [(_ (b:typed-binding ...) e)
+     #:when (andmap ★? (stx-map (λ (t) (typeof (expand/df t))) #'(b.τ ...)))
+     #:with (xs- e- τ_res) (infer/type-ctxt+erase #'(b ...) #'e)
+     (⊢ #'(λ xs- e-) #'(→ b.τ ... τ_res))]))
+
+(define-syntax (app/tc stx)
+  (syntax-parse stx #:literals (→)
+    [(_ e_fn e_arg ...)
+     #:with (e_fn- ((~literal →) τ ... τ_res)) (infer+erase #'e_fn)
+;     #:fail-unless (→? #'τ_fn)
+;                   (format "Type error: Attempting to apply a non-function ~a with type ~a\n"
+;                           (syntax->datum #'e_fn) (syntax->datum #'τ_fn))
+;     #:with (→ τ ... τ_res) #'τ_fn
+     #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
+     #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
+                   (string-append
+                    (format
+                     "Wrong number of args given to function ~a, or args have wrong type:\ngiven: "
+                     (syntax->datum #'e_fn))
+                    (string-join
+                     (map (λ (e+τ) (format "~a : ~a" (car e+τ) (cadr e+τ))) (syntax->datum #'([e_arg τ_arg] ...)))
+                     ", ")
+                    "\nexpected arguments with type: "
+                    (string-join
+                     (map (λ (x) (format "~a" x)) (syntax->datum #'(τ ...)))
+                     ", "))
+     (⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))
+
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
index d18c999..8d1da6b 100644
--- a/tapl/stlc.rkt
+++ b/tapl/stlc.rkt
@@ -34,6 +34,8 @@
   ;; type equality = structurally recursive identifier equality
   ;; structurally checks for free-identifier=?
   (define (type=? τ1 τ2)
+;    (printf "t1 = ~a\n" (syntax->datum τ1))
+;    (printf "t2 = ~a\n" (syntax->datum τ2))
     (syntax-parse (list τ1 τ2)
       [(x:id y:id) (free-identifier=? τ1 τ2)]
       [((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))]
diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt
index 312cc23..cf8c8b4 100644
--- a/tapl/sysf.rkt
+++ b/tapl/sysf.rkt
@@ -24,8 +24,6 @@
 (begin-for-syntax
   ;; Extend to handle ∀, skip typevars
   (define (eval-τ τ [tvs #'()])
-;    (printf "~a\n" (syntax->datum τ))
-;    (printf "tvs: ~a\n" tvs)
     (syntax-parse τ
       [x:id #:when (stx-member τ tvs) τ]
       [((~literal ∀) ts t-body)
@@ -47,7 +45,7 @@
   ;; extend to handle ∀
   (define (type=? τ1 τ2)
     (syntax-parse (list τ1 τ2) #:literals (∀)
-      [((∀ (x ...) t1) (∀ (y ...) t2))
+      [((∀ (x:id ...) t1) (∀ (y:id ...) t2))
        #:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
        #:with (z ...) (generate-temporaries #'(x ...))
        ((current-type=?) (substs #'(z ...) #'(x ...) #'t1)
@@ -59,11 +57,12 @@
 (define-syntax (Λ stx)
   (syntax-parse stx
     [(_ (tv:id ...) e)
-     #:with (tvs+ e- τ) (infer/tvs+erase #'e #'(tv ...))
-     (⊢ #'e- #'(∀ tvs+ τ))]))
+     #:with (tvs- e- τ) (infer/tvs+erase #'e #'(tv ...))
+     (⊢ #'e- #'(∀ tvs- τ))]))
 (define-syntax (inst stx)
   (syntax-parse stx
     [(_ e τ ...)
      #:with (e- τ_e) (infer+erase #'e)
      #:with ((~literal ∀) (tv ...) τ_body) #'τ_e
-     (⊢ #'e- (substs #'(τ ...) #'(tv ...) #'τ_body))]))
\ No newline at end of file
+     #:with (τ+ ...) (stx-map (current-τ-eval) #'(τ ...))
+     (⊢ #'e- (substs #'(τ+ ...) #'(tv ...) #'τ_body))]))
\ No newline at end of file
diff --git a/tapl/tests/fomega-tests.rkt b/tapl/tests/fomega-tests.rkt
index 53bb133..d2e6fc7 100644
--- a/tapl/tests/fomega-tests.rkt
+++ b/tapl/tests/fomega-tests.rkt
@@ -1,42 +1,57 @@
 #lang s-exp "../fomega.rkt"
 (require "rackunit-typechecking.rkt")
 
-(check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ (t1) (∀ (t2) (→ t1 (→ t2 t2)))))
+(check-type Int : ★)
+(check-type (→ Int Int) : ★)
+(typecheck-fail (→ →))
 
-(check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ (t3) (∀ (t4) (→ t3 (→ t4 t4)))))
+(typecheck-fail (λ ([x : (→ →)]) x))
 
-(check-not-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ (t4) (∀ (t3) (→ t3 (→ t4 t4)))))
+(typecheck-fail (∀ (t) t)) ; missing kind annotation
+(check-type (∀ ([t : ★]) t) : ★)
+(check-type (∀ ([→ : ★]) →) : ★) ; should be ok
+(check-type (∀ ([t : ★]) (∀ ([s : ★]) (→ t s))) : ★)
+(check-type (∀ ([t : ★] [s : ★]) (→ t s)) : ★)
+;(check-type (∀ ([t : (⇒ ★ ★)] [s : ★]) (t s)) : ★) ; doesnt work yet
+(typecheck-fail (∀ (t) (→ →)))
 
-(check-type (inst (Λ (t) (λ ([x : t]) x)) Int) : (→ Int Int))
-(check-type (inst (Λ (t) 1) Bool) : Int)
+;; sysf tests wont work, must be augmented with kinds
+(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))
+(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/tapl/tests/stlc+lit-tests.rkt b/tapl/tests/stlc+lit-tests.rkt
index f1a763d..521ee75 100644
--- a/tapl/tests/stlc+lit-tests.rkt
+++ b/tapl/tests/stlc+lit-tests.rkt
@@ -8,6 +8,7 @@
 (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 (λ ([x : (→ →)]) x) : (→ (→ →) (→ →))) ; TODO: should this fail?
 (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
diff --git a/tapl/tests/sysf-tests.rkt b/tapl/tests/sysf-tests.rkt
index b93ae18..5f82262 100644
--- a/tapl/tests/sysf-tests.rkt
+++ b/tapl/tests/sysf-tests.rkt
@@ -11,7 +11,7 @@
             : (∀ (t4) (∀ (t3) (→ t3 (→ t4 t4)))))
 
 (check-type (inst (Λ (t) (λ ([x : t]) x)) Int) : (→ Int Int))
-(check-type (inst (Λ (t) 1) Bool) : 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