diff --git a/tapl/README.md b/tapl/README.md
index b71360e..56f02bc 100644
--- a/tapl/README.md
+++ b/tapl/README.md
@@ -12,4 +12,5 @@ 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
+       - fomega2.rkt
\ No newline at end of file
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
index 820357e..b886340 100644
--- a/tapl/fomega.rkt
+++ b/tapl/fomega.rkt
@@ -45,7 +45,7 @@
       [((~literal #%plain-app) arg ...)
        #:with (arg+ ...) (stx-map (current-type-eval) #'(arg ...))
        (syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
-      [(τ ...) (stx-map (current-type-eval) #'(τ ...))]
+      ;[(τ ...) (stx-map (current-type-eval) #'(τ ...))]
       [_ (sysf:type-eval τ)]))
   (current-type-eval type-eval))
 
diff --git a/tapl/fomega2.rkt b/tapl/fomega2.rkt
new file mode 100644
index 0000000..f6bcc08
--- /dev/null
+++ b/tapl/fomega2.rkt
@@ -0,0 +1,189 @@
+#lang racket/base
+(require "typecheck.rkt")
+(require (except-in "sysf.rkt" #%app λ Int #%datum → Λ inst ∀  + type-eval)
+         (prefix-in sysf: (only-in "sysf.rkt" #%app λ Int → ∀ type-eval)))
+(provide (rename-out [app/tc #%app] [λ/tc λ] [datum/tc #%datum]))
+(provide (except-out (all-from-out "sysf.rkt")
+                     sysf:Int sysf:→ sysf:∀
+                     sysf:#%app sysf:λ
+                     (for-syntax sysf:type-eval)))
+(provide Int → ∀ inst Λ
+         (for-syntax type-eval))
+
+;; same as fomega.rkt, except tyapp == #%app, tyλ = λ, and ⇒ = →
+
+;; System F_omega 
+;; Type relation:
+;; Types:
+;; - types from sysf.rkt
+;; Terms:
+;; - terms from sysf.rkt
+
+(provide define-type-alias)
+(define-syntax define-type-alias
+  (syntax-parser
+    [(_ alias:id τ:type)
+     ; must eval, otherwise undefined types will be allowed
+     #'(define-syntax alias
+         (syntax-parser
+           [x:id #'τ.norm]
+           [(_ x (... ...))
+            ((current-type-eval) (⊢ #'(#%plain-app τ.norm x (... ...)) #'★))]))]))
+
+(begin-for-syntax
+  ;; extend type-eval to handle tyapp
+  ;; - requires manually handling all other forms
+  (define (type-eval τ)
+;    (printf "eval: ~a\n" (syntax->datum τ))
+    (syntax-parse τ
+      [((~literal #%plain-app) τ_fn τ_arg ...)
+       #:with ((~literal #%plain-lambda) (tv ...) τ_body) ((current-type-eval) #'τ_fn)
+       #:with (τ_arg+ ...) (stx-map (current-type-eval) #'(τ_arg ...))
+       (substs #'(τ_arg+ ...) #'(tv ...) #'τ_body)]
+      [((~literal ∀) _ ...) ((current-type-eval) (sysf:type-eval τ))]
+      [((~literal →) _ ...) ((current-type-eval) (sysf:type-eval τ))]
+;      [((~literal ⇒) _ ...) ((current-type-eval) (sysf:type-eval τ))]
+;      [((~literal λ/tc) _ ...) (sysf:type-eval τ)]
+;      [((~literal app/tc) _ ...) ((current-type-eval) (sysf:type-eval τ))]
+      [((~literal #%plain-lambda) (x ...) τ_body ...)
+       #:with (τ_body+ ...) (stx-map (current-type-eval) #'(τ_body ...))
+       (syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'plain-lambda)]
+      [((~literal #%plain-app) arg ...)
+       #:with (arg+ ...) (stx-map (current-type-eval) #'(arg ...))
+       (syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
+      ;[(τ ...) (stx-map (current-type-eval) #'(τ ...))]
+      [_ (sysf:type-eval τ)]))
+  (current-type-eval type-eval))
+
+(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
+
+;; TODO: need some kind of "promote" abstraction,
+;; so I dont have to manually add kinds to all types
+(define-base-type Str)
+(provide String)
+(define-syntax String (syntax-parser [x:id (⊢ #'Str #'★)]))
+(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 (or
+             ; when used as →
+             (and (typecheck? #'k_res #'★)
+                  (same-types? #'(k ... k_res)))
+             ; when used as ⇒
+             (not (syntax-e (stx-ormap (λ (x) x) #'(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 #'★)
+     (⊢ #'(#%plain-lambda tvs- b.τ ... τ-) #;#'(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 τ:type ...)
+     #:with ([τ- k] ...) (infers+erase #'(τ ...))
+     #:with (e- ∀τ) (infer+erase #'e)
+     #:with ((~literal #%plain-lambda) (tv ...) k_tv ... τ_body) #'∀τ
+     #:when (typechecks? #'(k ...) #'(k_tv ...))
+     (⊢ #'e- (substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
+
+;; TODO: merge with regular λ and app?
+#;(define-syntax (tyλ stx)
+  (syntax-parse stx 
+    [(_ (b:typed-binding ...) τ)
+     #:with (tvs- τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
+     ;; b.τ's here are actually kinds
+     (⊢ #'(λ tvs- τ-) #'(⇒ b.τ ... k))]))
+
+#;(define-syntax (tyapp stx)
+  (syntax-parse stx
+    [(_ τ_fn τ_arg ...)
+     #:with [τ_fn- k_fn] (infer+erase #'τ_fn)
+     #:fail-unless (⇒? #'k_fn)
+                   (format "Kind error: Attempting to apply a non-tyλ with kind ~a\n"
+                           (syntax->datum #'τ_fn) (syntax->datum #'k_fn))
+     #:with ((~literal #%plain-app) _ k ... k_res) #'k_fn
+     #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...))
+     #:fail-unless (typechecks? #'(k_arg ...) #'(k ...))
+                   (string-append
+                    (format
+                     "Wrong number of args given to tyλ ~a, or args have wrong kind:\ngiven: "
+                     (syntax->datum #'τ_fn))
+                    (string-join
+                     (map
+                      (λ (τ+k) (format "~a : ~a" (car τ+k) (cadr τ+k)))
+                      (syntax->datum #'([τ_arg k_arg] ...)))
+                     ", ")
+                    "\nexpected arguments with type: "
+                    (string-join
+                     (map (λ (x) (format "~a" x)) (syntax->datum #'(k ...)))
+                     ", "))
+      ;; cant do type-subst here bc τ_fn might be a (forall) tyvar
+      ;#:with τ_res ((current-type-eval) #'(tyapply τ_fn- τ_arg- ...))
+     (⊢ #'(#%app τ_fn- τ_arg- ...) #'k_res)]))
+
+;; 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)
+     #:with (k ...) (stx-map (λ (t) (typeof (expand/df t))) #'(b.τ ...))
+     #:when (or
+             ; regular lambda
+             (stx-andmap ★? #'(k ...))
+             ; type-level lambda
+             (not (syntax-e (stx-ormap (λ (x) x) #'(k ...)))))
+     #:with (xs- e- τ_res) (infer/type-ctxt+erase #'(b ...) #'e)
+     (⊢ #'(λ xs- e-) #'(→ b.τ ... τ_res))]))
+
+(define-syntax (app/tc stx)
+  (syntax-parse stx
+    [(_ e_fn e_arg ...)
+     #:with [e_fn- τ_fn] (infer+erase #'e_fn)
+     ;; this is sysf:→?, it's not defined in fomega so import without prefix
+     #: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 ((~literal #%plain-app) _ τ ... τ_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)]))
+
+;; must override #%datum to use new kinded-Int, etc
+(define-syntax (datum/tc stx)
+  (syntax-parse stx
+    [(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)]
+    [(_ . s:str) (⊢ (syntax/loc stx (#%datum . s)) #'String)]
+    [(_ . x)
+     #:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
+     #'(#%datum . x)]))
\ No newline at end of file
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
index 3d2c6b7..aa812c6 100644
--- a/tapl/stx-utils.rkt
+++ b/tapl/stx-utils.rkt
@@ -6,6 +6,8 @@
 
 (define (stx-andmap f . stx-lsts)
   (apply andmap f (map syntax->list stx-lsts)))
+(define (stx-ormap f . stx-lsts)
+  (apply ormap f (map syntax->list stx-lsts)))
 
 (define (stx-flatten stxs)
   (apply append (stx-map syntax->list stxs)))
diff --git a/tapl/tests/fomega-tests.rkt b/tapl/tests/fomega-tests.rkt
index cf1a87b..8be99f4 100644
--- a/tapl/tests/fomega-tests.rkt
+++ b/tapl/tests/fomega-tests.rkt
@@ -121,33 +121,6 @@
          Int String) 1 "1"))
  : String ⇒ "1")
 
-;(check-type (λ ([x : (∀ ([t : ★]) t)]) x) : (→ (∀ ([t : ★]) t) (∀ ([t : ★]) t)))
-;(check-type (λ ([x : (∀ ([t : (⇒ ★ ★)]) (tyapp t Int))]) x) : Int #;(→ (∀ ([t : (⇒ ★ ★)]) t) (∀ ([t : (⇒ ★ ★)]) t)))
-
-;(check-type 1 : (tyapp (tyλ ([X : ★]) X) Int))
-;(check-not-type 1 : (tyapp (tyλ ([X : ★]) X) String))
-;
-;;(check-type (λ ([x : Int]) x) : (tyapp (tyλ ([X : ★]) (→ X X)) Int))
-;
-;; Mono Pair
-;#;(tyapp (tyλ ([Pair : (⇒ ★ ★)]) (λ ([p : (tyapp Pair Int)]) p))
-;      (tyλ ([X : ★]) (∀ ([P : ★]) (→ (→ X X P) P))))
-;
-;
-;;(check-type Int : ★)
-;;(check-type (→ Int Int) : ★)
-;;(typecheck-fail (→ →))
-;
-;(typecheck-fail (λ ([x : (→ →)]) x))
-;
-;(typecheck-fail (λ ([x : (∀ (t) t)]) x)) ; 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) (→ →)))
-;
 ;;; sysf tests wont work, unless augmented with kinds
 (check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
 
diff --git a/tapl/tests/fomega2-tests.rkt b/tapl/tests/fomega2-tests.rkt
new file mode 100644
index 0000000..4211059
--- /dev/null
+++ b/tapl/tests/fomega2-tests.rkt
@@ -0,0 +1,188 @@
+#lang s-exp "../fomega2.rkt"
+(require "rackunit-typechecking.rkt")
+
+(check-type Int : ★)
+(check-type String : ★)
+(typecheck-fail →)
+(check-type (→ Int Int) : ★)
+(typecheck-fail (→ →))
+(check-type 1 : Int)
+
+(check-type (∀ ([t : ★]) (→ t t)) : ★)
+(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
+
+(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)))
+;; applied f too early
+(typecheck-fail (inst
+                 (Λ ([yf : (→ ★ ★)]) (λ ([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
+(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 (Λ ([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/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
index 28d1a2f..a886da5 100644
--- a/tapl/tests/run-all-tests.rkt
+++ b/tapl/tests/run-all-tests.rkt
@@ -11,4 +11,5 @@
 (require "stlc+rec+sub-tests.rkt")
 
 (require "sysf-tests.rkt")
-(require "fomega-tests.rkt")
\ No newline at end of file
+(require "fomega-tests.rkt")
+(require "fomega2-tests.rkt")
\ No newline at end of file