diff --git a/macrotypes/examples/exist.rkt b/macrotypes/examples/exist.rkt
index 1df2a28..eda84a9 100644
--- a/macrotypes/examples/exist.rkt
+++ b/macrotypes/examples/exist.rkt
@@ -22,26 +22,25 @@
    (⊢ e- : ∃τ.norm)])
 
 (define-typed-syntax open #:datum-literals (<=)
-  [(open ([(tv:id x:id) <= e_packed]) e)
-   #:with [e_packed- ((τ_abstract) (τ_body))] (⇑ e_packed as ∃)
+  [(open [x:id <= e_packed with X:id] e)
      ;; The subst below appears to be a hack, but it's not really.
      ;; It's the (TaPL) type rule itself that is fast and loose.
      ;; Leveraging the macro system's management of binding reveals this.
      ;; 
      ;; Specifically, here is the TaPL Unpack type rule, fig24-1, p366:
-     ;; Γ ⊢ t_1 : {∃X,T_12}
-     ;; Γ,X,x:T_12 ⊢ t_2 : T_2
+     ;; Γ ⊢ e_packed : {∃X,τ_body}
+     ;; Γ,X,x:τ_body ⊢ e : τ_e
      ;; ------------------------------
-     ;; Γ ⊢ let {X,x}=t_1 in t_2 : T_2
+     ;; Γ ⊢ (open [x <= e_packed with X] e) : τ_e
      ;;
      ;; There's *two* separate binders, the ∃ and the let,
      ;; which the rule conflates.
      ;;
      ;; Here's the rule rewritten to distinguish the two binding positions:
-     ;; Γ ⊢ t_1 : {∃X_1,T_12}
-     ;; Γ,X_???,x:T_12 ⊢ t_2 : T_2
+     ;; Γ ⊢ e_packed : {∃X_1,τ_body}
+     ;; Γ,X_???,x:τ_body ⊢ e : τ_e
      ;; ------------------------------
-     ;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
+     ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e
      ;;
      ;; The X_1 binds references to X in T_12.
      ;; The X_2 binds references to X in t_2.
@@ -49,26 +48,28 @@
      ;;
      ;; A first guess might be to replace X_??? with both X_1 and X_2,
      ;; so all the potentially referenced type vars are bound.
-     ;; Γ ⊢ t_1 : {∃X_1,T_12}
-     ;; Γ,X_1,X_2,x:T_12 ⊢ t_2 : T_2
+     ;; Γ ⊢ e_packed : {∃X_1,τ_body}
+     ;; Γ,X_1,X_2,x:τ_body ⊢ e : τ_e
      ;; ------------------------------
-     ;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
+     ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e
      ;;
      ;; But this example demonstrates that the rule above doesnt work:
-     ;; (open ([x : X_2 (pack (Int 0) as (∃ (X_1) X_1))])
+     ;; (open [x <= (pack (Int 0) as (∃ (X_1) X_1)) with X_2]
      ;;   ((λ ([y : X_2]) y) x)
      ;; Here, x has type X_1, y has type X_2, but they should be the same thing,
      ;; so we need to replace all X_1's with X_2
      ;;
      ;; Here's the fixed rule, which is implemented here
      ;;
-     ;; Γ ⊢ t_1 : {∃X_1,T_12}
-     ;; Γ,X_2,x:[X_2/X_1]T_12 ⊢ t_2 : T_2
+     ;; Γ ⊢ e_packed : {∃X_1,τ_body}
+     ;; Γ,X_2:#%type,x:[X_2/X_1]τ_body ⊢ e : τ_e
      ;; ------------------------------
-     ;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
+     ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e
      ;;
-   #:with [_ (x-) (e-) (τ_e)]
+   #:with [e_packed- (~∃ (Y) τ_body)] (infer+erase #'e_packed)
+   #:with τ_x (subst #'X #'Y #'τ_body)
+   #:with [(X-) (x-) (e-) (τ_e)]
           (infer #'(e)
-                 #:tvctx #'([tv : #%type])
-                 #:ctx   #`([x : #,(subst #'tv #'τ_abstract #'τ_body)]))
+                 #:tvctx #'([X : #%type])
+                 #:ctx   #`([x : τ_x]))
    (⊢ (let- ([x- e_packed-]) e-) : τ_e)])
diff --git a/macrotypes/examples/fomega.rkt b/macrotypes/examples/fomega.rkt
index 8113ab6..f6c3b4a 100644
--- a/macrotypes/examples/fomega.rkt
+++ b/macrotypes/examples/fomega.rkt
@@ -89,14 +89,14 @@
 
 (define-typed-syntax inst
   [(inst e τ ...)
-   #:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀)
+   #:with [e- τ_e] (infer+erase #'e)
+   #:with (~∀ (tv ...) τ_body) #'τ_e
+   #:with (~∀★ k ...) (typeof #'τ_e)
    #: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))])
+   #:fail-unless (typechecks? #'(k_τ ...) #'(k ...))
+   (typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...))
+   #:with τ_inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
+   (⊢ e- : τ_inst)])
 
 ;; TODO: merge with regular λ and app?
 ;; - see fomega2.rkt
diff --git a/macrotypes/examples/sysf.rkt b/macrotypes/examples/sysf.rkt
index 0a29fcd..71871c7 100644
--- a/macrotypes/examples/sysf.rkt
+++ b/macrotypes/examples/sysf.rkt
@@ -16,14 +16,11 @@
 
 (define-typed-syntax Λ
   [(Λ (tv:id ...) e)
-   #:with ((tv- ...) e- τ) (infer/tyctx+erase #'([tv : #%type] ...) #'e)
+   #:with [(tv- ...) e- τ] (infer/tyctx+erase #'([tv : #%type] ...) #'e)
    (⊢ e- : (∀ (tv- ...) τ))])
 (define-typed-syntax inst
   [(inst e τ:type ...)
-   #:with (e- (tvs (τ_body))) (⇑ e as ∀)
-   ;#:with [e- (~and t (~∀ tvs τ_body))] (infer+erase #'e)
-   ;#:with (_ Xs τ_orig) (get-orig #'t) ; doesnt work with implicit lifted→
-   ;#:with new-orig (substs #'(τ ...) #'Xs #'τ_orig)
-   ;(⊢ e- : #,(add-orig (substs #'(τ.norm ...) #'tvs #'τ_body) #'new-orig))]
-   (⊢ e- : #,(substs #'(τ.norm ...) #'tvs #'τ_body))]
-  [(_ e) #'e])
+   #:with [e- (~∀ tvs τ_body)] (infer+erase #'e)
+   #:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body)
+   (⊢ e- : τ_inst)]
+  [(inst e) #'e])
diff --git a/macrotypes/examples/tests/exist-tests.rkt b/macrotypes/examples/tests/exist-tests.rkt
new file mode 100644
index 0000000..cf56abc
--- /dev/null
+++ b/macrotypes/examples/tests/exist-tests.rkt
@@ -0,0 +1,370 @@
+#lang s-exp "../exist.rkt"
+(require "rackunit-typechecking.rkt")
+
+(check-type (pack (Int 0) as (∃ (X) X)) : (∃ (X) X))
+(check-type (pack (Int 0) as (∃ (X) X)) : (∃ (Y) Y))
+(typecheck-fail (pack (Int 0) as (∃ (X) Y)))
+(check-type (pack (Bool #t) as (∃ (X) X)) : (∃ (X) X))
+(typecheck-fail (pack (Int #t) as (∃ (X) X)))
+
+(check-type (pack (Int (pack (Int 0) as (∃ (X) X))) as (∃ (Y) (∃ (X) X)))
+            : (∃ (Y) (∃ (X) X)))
+(check-type (pack (Int +) as (∃ (X) (→ X Int Int))) : (∃ (X) (→ X Int Int)))
+(check-type (pack (Int (pack (Int +) as (∃ (X) (→ X Int Int))))
+                  as (∃ (Y) (∃ (X) (→ X Y Int))))
+            : (∃ (Y) (∃ (X) (→ X Y Int))))
+(check-not-type (pack (Int (pack (Int +) as (∃ (X) (→ X Int Int))))
+                      as (∃ (Y) (∃ (X) (→ X Y Int))))
+                : (∃ (X) (∃ (X) (→ X X Int))))
+
+; cant typecheck bc X has local scope, and no X elimination form
+;(check-type (open [x <= (pack (Int 0) as (∃ (X) X)) with X] x) : X) 
+
+(check-type 0 : Int)
+(check-type (+ 0 1) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (+ x 1)) 0) : Int ⇒ 1)
+(typecheck-fail (open [x <= (pack (Int 0) as (∃ (X) X)) with] (+ x 1))) ; can't use as Int
+
+(check-type (λ ([x : (∃ (X) X)]) x) : (→ (∃ (X) X) (∃ (Y) Y)))
+(check-type ((λ ([x : (∃ (X) X)]) x) (pack (Int 0) as (∃ (Z) Z)))
+            : (∃ (X) X) ⇒ 0)
+(check-type ((λ ([x : (∃ (X) X)]) x) (pack (Bool #t) as (∃ (Z) Z)))
+            : (∃ (X) X) ⇒ #t)
+
+;; example where the two binding X's are conflated, see exist.rkt for explanation
+(check-type (open [x <= (pack (Int 0) as (∃ (X) X)) with X] ((λ ([y : X]) 1) x))
+            : Int ⇒ 1)
+            
+(check-type
+ (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
+       as (∃ (X) (× [a : X] [f : (→ X X)])))
+ : (∃ (X) (× [a : X] [f : (→ X X)])))
+
+(define p4
+  (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
+        as (∃ (X) (× [a : X] [f : (→ X Int)]))))
+(check-type p4 : (∃ (X) (× [a : X] [f : (→ X Int)])))
+
+(check-not-type (open [x <= p4 with X] (proj x a)) : Int) ; type is X, not Int
+; type is (→ X X), not (→ Int Int)
+(check-not-type (open [x <= p4 with X] (proj x f)) : (→ Int Int))
+(typecheck-fail (open [x <= p4 with X] (+ 1 (proj x a))))
+(check-type (open [x <= p4 with X] ((proj x f) (proj x a))) : Int ⇒ 6)
+(check-type (open [x <= p4 with X] ((λ ([y : X]) ((proj x f) y)) (proj x a))) : Int ⇒ 6)
+
+(check-type
+ (open [x <= (pack (Int 0) as (∃ (Y) Y)) with X]
+       ((λ ([y : X]) 1) x))
+ : Int ⇒ 1)
+
+(check-type
+ (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
+       as (∃ (X) (× [a : Int] [f : (→ Int Int)])))
+ : (∃ (X) (× [a : Int] [f : (→ Int Int)])))
+
+(typecheck-fail
+ (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
+       as (∃ (X) (× [a : Int] [f : (→ Bool Int)]))))
+
+(typecheck-fail
+ (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
+       as (∃ (X) (× [a : X] [f : (→ X Bool)]))))
+
+(check-type
+ (pack (Bool (tup [a = #t] [f = (λ ([x : Bool]) (if x 1 2))]))
+       as (∃ (X) (× [a : X] [f : (→ X Int)])))
+ : (∃ (X) (× [a : X] [f : (→ X Int)])))
+
+(define counterADT
+  (pack (Int (tup [new = 1]
+                  [get = (λ ([i : Int]) i)]
+                  [inc = (λ ([i : Int]) (+ i 1))]))
+        as (∃ (Counter) (× [new : Counter]
+                           [get : (→ Counter Int)]
+                           [inc : (→ Counter Counter)]))))
+(check-type counterADT :
+            (∃ (Counter) (× [new : Counter]
+                            [get : (→ Counter Int)]
+                            [inc : (→ Counter Counter)])))
+(typecheck-fail
+ (open [counter <= counterADT with Counter]
+       (+ (proj counter new) 1))
+ #:with-msg "expected: +Int, Int\n *given: +Counter, Int\n *expressions: \\(proj counter new\\), 1")
+(typecheck-fail
+ (open [counter <= counterADT with Counter]
+       ((λ ([x : Int]) x) (proj counter new)))
+ #:with-msg "expected: +Int\n *given: +Counter\n *expressions: \\(proj counter new\\)")
+(check-type
+ (open [counter <= counterADT with Counter]
+       ((proj counter get) ((proj counter inc) (proj counter new))))
+ : Int ⇒ 2)
+
+ (check-type
+  (open [counter <= counterADT with Counter]
+        (let ([inc (proj counter inc)]
+              [get (proj counter get)])
+          (let ([add3 (λ ([c : Counter]) (inc (inc (inc c))))])
+            (get (add3 (proj counter new))))))
+  : Int ⇒ 4)
+
+(check-type
+ (open [counter <= counterADT with Counter]
+       (let ([get (proj counter get)]
+             [inc (proj counter inc)]
+             [new (λ () (proj counter new))])
+         (letrec ([(is-even? : (→ Int Bool))
+                   (λ ([n : Int])
+                     (or (zero? n)
+                      (is-odd? (sub1 n))))]
+                  [(is-odd? : (→ Int Bool))
+                   (λ ([n : Int])
+                     (and (not (zero? n))
+                          (is-even? (sub1 n))))])
+           (open [flipflop <=
+                  (pack (Counter (tup [new = (new)]
+                                      [read = (λ ([c : Counter]) (is-even? (get c)))]
+                                      [toggle = (λ ([c : Counter]) (inc c))]
+                                      [reset = (λ ([c : Counter]) (new))]))
+                        as (∃ (FlipFlop) (× [new : FlipFlop]
+                                            [read : (→ FlipFlop Bool)]
+                                            [toggle : (→ FlipFlop FlipFlop)]
+                                            [reset : (→ FlipFlop FlipFlop)])))
+                  with FlipFlop]
+                 (let ([read (proj flipflop read)]
+                       [togg (proj flipflop toggle)])
+                   (read (togg (togg (togg (togg (proj flipflop new)))))))))))
+ : Bool ⇒ #f)
+
+(define counterADT2
+  (pack ((× [x : Int])
+         (tup [new = (tup [x = 1])]
+              [get = (λ ([i : (× [x : Int])]) (proj i x))]
+              [inc = (λ ([i : (× [x : Int])]) (tup [x = (+ 1 (proj i x))]))]))
+        as (∃ (Counter) (× [new : Counter]
+                           [get : (→ Counter Int)]
+                           [inc : (→ Counter Counter)]))))
+(check-type counterADT2 :
+            (∃ (Counter) (× [new : Counter]
+                            [get : (→ Counter Int)]
+                            [inc : (→ Counter Counter)])))
+
+;; same as above, but with different internal counter representation
+(check-type
+ (open [counter <= counterADT2 with Counter]
+       (let ([get (proj counter get)]
+             [inc (proj counter inc)]
+             [new (λ () (proj counter new))])
+         (letrec ([(is-even? : (→ Int Bool))
+                   (λ ([n : Int])
+                     (or (zero? n)
+                      (is-odd? (sub1 n))))]
+                  [(is-odd? : (→ Int Bool))
+                   (λ ([n : Int])
+                     (and (not (zero? n))
+                          (is-even? (sub1 n))))])
+           (open [flipflop <=
+                  (pack (Counter (tup [new = (new)]
+                                      [read = (λ ([c : Counter]) (is-even? (get c)))]
+                                      [toggle = (λ ([c : Counter]) (inc c))]
+                                      [reset = (λ ([c : Counter]) (new))]))
+                        as (∃ (FlipFlop) (× [new : FlipFlop]
+                                            [read : (→ FlipFlop Bool)]
+                                            [toggle : (→ FlipFlop FlipFlop)]
+                                            [reset : (→ FlipFlop FlipFlop)])))
+                  with
+                  FlipFlop]
+                 (let ([read (proj flipflop read)]
+                       [togg (proj flipflop toggle)])
+                   (read (togg (togg (togg (togg (proj flipflop new)))))))))))
+ : Bool ⇒ #f)
+
+;; err cases
+(typecheck-fail
+ (pack (Int 1) as Int)
+ #:with-msg
+ "Expected ∃ type, got: Int")
+(typecheck-fail
+ (open [x <= 2 with X] 3)
+ #:with-msg
+ "Expected ∃ type, got: Int")
+
+;; previous tets from stlc+reco+var-tests.rkt ---------------------------------
+;; define-type-alias
+(define-type-alias Integer Int)
+(define-type-alias ArithBinOp (→ Int Int Int))
+;(define-type-alias C Complex) ; error, Complex undefined
+
+(check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer)
+(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int)
+(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Integer)
+(check-type + : ArithBinOp)
+(check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int))
+
+;; records (ie labeled tuples)
+(check-type "Stephen" : String)
+(check-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+            (× [name : String] [phone : Int] [male? : Bool]))
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
+            : String ⇒ "Stephen")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
+            : String ⇒ "Stephen")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone)
+            : Int ⇒ 781)
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) male?)
+            : Bool ⇒ #t)
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [my-name : String] [phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [name : String] [my-phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [name : String] [phone : Int] [is-male? : Bool]))
+
+;; variants
+(check-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit]))
+(check-not-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit] [tea : Unit]))
+(typecheck-fail ((λ ([x : (∨ [coffee : Unit] [tea : Unit])]) x)
+                 (var coffee = (void) as (∨ [coffee : Unit]))))
+(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) : (∨ [coffee : Unit] [tea : Unit]))
+(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
+            : (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
+
+(typecheck-fail
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+   [coffee x => 1])) ; not enough clauses
+(typecheck-fail
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+   [coffee x => 1]
+   [teaaaaaa x => 2])) ; wrong clause
+(typecheck-fail
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+   [coffee x => 1]
+   [tea x => 2]
+   [coke x => 3])) ; too many clauses
+(typecheck-fail
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+   [coffee x => "1"]
+   [tea x => 2])) ; mismatched branch types
+(check-type
+ (case (var coffee = 1 as (∨ [coffee : Int] [tea : Unit]))
+   [coffee x => x]
+   [tea x => 2]) : Int ⇒ 1)
+(define-type-alias Drink (∨ [coffee : Int] [tea : Unit] [coke : Bool]))
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
+(check-type
+ (case ((λ ([d : Drink]) d)
+        (var coffee = 1 as (∨ [coffee : Int] [tea : Unit] [coke : Bool])))
+   [coffee x => (+ (+ x x) (+ x x))]
+   [tea x => 2]
+   [coke y => 3])
+ : Int ⇒ 4)
+
+(check-type
+ (case ((λ ([d : Drink]) d) (var coffee = 1 as Drink))
+   [coffee x => (+ (+ x x) (+ x x))]
+   [tea x => 2]
+   [coke y => 3])
+ : Int ⇒ 4)
+
+;; previous tests: ------------------------------------------------------------
+;; tests for tuples -----------------------------------------------------------
+;; old tuple syntax not supported here
+;(check-type (tup 1 2 3) : (× Int Int Int))
+;(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int)))
+;(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int)))
+;(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int)))
+;(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int)))
+;(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit)))
+;
+;(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1)
+;(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2")
+;(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f)
+;(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large
+;(typecheck-fail (proj 1 2)) ; not tuple
+
+;; ext-stlc.rkt tests ---------------------------------------------------------
+;; should still pass
+
+;; new literals and base types
+(check-type "one" : String) ; literal now supported
+(check-type #f : Bool) ; literal now supported
+
+(check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type
+
+;; Unit
+(check-type (void) : Unit)
+(check-type void : (→ Unit))
+(typecheck-fail ((λ ([x : Unit]) x) 2))
+(typecheck-fail ((λ ([x : Unit])) void))
+(check-type ((λ ([x : Unit]) x) (void)) : Unit)
+
+;; begin
+(typecheck-fail (begin))
+(check-type (begin 1) : Int)
+;(typecheck-fail (begin 1 2 3))
+(check-type (begin (void) 1) : Int ⇒ 1)
+
+;;ascription
+(typecheck-fail (ann 1 : Bool))
+(check-type (ann 1 : Int) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
+
+; let
+(check-type (let () (+ 1 1)) : Int ⇒ 2)
+(check-type (let ([x 10]) (+ 1 2)) : Int)
+(typecheck-fail (let ([x #f]) (+ x 1)))
+(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
+(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier
+
+(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
+(typecheck-fail (let* ([x #t] [y (+ x 1)]) 1))
+
+; letrec
+(typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y))
+(typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x))
+
+(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
+
+;; recursive
+(check-type
+ (letrec ([(countdown : (→ Int String))
+           (λ ([i : Int])
+             (if (= i 0)
+                 "liftoff"
+                 (countdown (- i 1))))])
+   (countdown 10)) : String ⇒ "liftoff")
+
+;; mutually recursive
+(check-type
+ (letrec ([(is-even? : (→ Int Bool))
+           (λ ([n : Int])
+             (or (zero? n)
+                 (is-odd? (sub1 n))))]
+          [(is-odd? : (→ Int Bool))
+           (λ ([n : Int])
+             (and (not (zero? n))
+                  (is-even? (sub1 n))))])
+   (is-odd? 11)) : Bool ⇒ #t)
+
+;; tests from stlc+lit-tests.rkt --------------------------
+; most should pass, some failing may now pass due to added types/forms
+(check-type 1 : Int)
+;(check-not-type 1 : (Int → Int))
+;(typecheck-fail "one") ; literal now supported
+;(typecheck-fail #f) ; literal now supported
+(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 now valid type, but arg has wrong type
+;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
+            : (→ (→ Int Int Int) Int Int Int))
+(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+
diff --git a/macrotypes/examples/tests/fomega-tests.rkt b/macrotypes/examples/tests/fomega-tests.rkt
new file mode 100644
index 0000000..61eab8b
--- /dev/null
+++ b/macrotypes/examples/tests/fomega-tests.rkt
@@ -0,0 +1,211 @@
+#lang s-exp "../fomega.rkt"
+(require "rackunit-typechecking.rkt")
+
+(check-type Int : ★)
+(check-type String : ★)
+(typecheck-fail →)
+(check-type (→ Int Int) : ★)
+(typecheck-fail (→ →))
+(typecheck-fail (→ 1))
+(check-type 1 : Int)
+
+(typecheck-fail (tyλ ([x : ★]) 1) #:with-msg "not a valid type: 1")
+
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+(check-not-type (Λ ([X : ★]) (λ ([x : X]) x)) :
+                (∀ ([X : (∀★ ★)]) (→ X X)))
+
+;(check-type (∀ ([t : ★]) (→ t t)) : ★)
+(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
+(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
+
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+
+(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
+            : (∀ ([X : ★]) (→ X X)))
+(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (⇒ ★ ★)]) (λ ([x : X]) x))))
+
+(check-type (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 "inst: type mismatch\n *expected: +★\n *given: +Int\n *expressions: 1")
+
+(typecheck-fail
+ (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
+ #:with-msg "Expected → type, got: \\(tyapp tyf String\\)")
+;; 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 → type, got: \\(tyapp tyf String\\)")
+(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 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))
+;; 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)))
+;; 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))
+;; 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 : ★]) (→ (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)
diff --git a/macrotypes/examples/tests/fomega2-tests.rkt b/macrotypes/examples/tests/fomega2-tests.rkt
new file mode 100644
index 0000000..a3eeaec
--- /dev/null
+++ b/macrotypes/examples/tests/fomega2-tests.rkt
@@ -0,0 +1,203 @@
+#lang s-exp "../fomega2.rkt"
+(require "rackunit-typechecking.rkt")
+
+(check-type Int : ★)
+(check-type String : ★)
+(typecheck-fail →)
+(check-type (→ Int Int) : ★)
+(typecheck-fail (→ →))
+(typecheck-fail (→ 1))
+(check-type 1 : Int)
+
+;; 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-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+
+(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
+            : (∀ ([X : ★]) (→ X X)))
+(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (→ ★ ★)]) (λ ([x : X]) x))))
+
+(check-type (λ ([t : ★]) t) : (→ ★ ★))
+(check-type (λ ([t : ★] [s : ★]) t) : (→ ★ ★ ★))
+(check-type (λ ([t : ★]) (λ ([s : ★]) t)) : (→ ★ (→ ★ ★)))
+(check-type (λ ([t : (→ ★ ★)]) t) : (→ (→ ★ ★) (→ ★ ★)))
+(check-type (λ ([t : (→ ★ ★ ★)]) t) : (→ (→ ★ ★ ★) (→ ★ ★ ★)))
+(check-type (λ ([arg : ★] [res : ★]) (→ arg res)) : (→ ★ ★ ★))
+
+(check-type ((λ ([t : ★]) t) Int) : ★)
+(check-type (λ ([x : ((λ ([t : ★]) t) Int)]) x) : (→ Int Int))
+(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
+(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
+(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
+(typecheck-fail ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
+
+;; partial-apply →
+(check-type ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)
+            : (→ ★ ★))
+; f's type must have kind ★
+(typecheck-fail (λ ([f : ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)]) f))
+(check-type (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) :
+            (∀ ([tyf : (→ ★ ★)]) (→ (tyf String) (tyf String))))
+(check-type (inst
+             (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+             ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+            : (→ (→ Int String) (→ Int String)))
+(typecheck-fail
+ (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1))
+ ;#:with-msg "not a valid type: 1")
+
+;; applied f too early
+(typecheck-fail (inst
+                 (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
+                 ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)))
+(check-type ((inst
+              (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+              ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+             (λ ([x : Int]) "int")) : (→ Int String))
+(check-type (((inst
+               (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+              ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+              (λ ([x : Int]) "int")) 1) : String ⇒ "int")
+
+;; tapl examples, p441
+(typecheck-fail
+ (define-type-alias tmp 1))
+ ;#:with-msg "not a valid type: 1")
+(define-type-alias Id (λ ([X : ★]) X))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (Id String)) Int))
+(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int (Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) (Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) String) Int))
+(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (Id (→ Int String)) Int))
+(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (→ Int String)) Int))
+(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (Id (→ Int String))) Int))
+
+;; tapl examples, p451
+(define-type-alias Pair (λ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
+
+;(check-type Pair : (→ ★ ★ ★))
+(check-type Pair : (→ ★ ★ (∀★ ★)))
+
+(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
+; parametric pair constructor
+(check-type
+ (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ : (∀ ([X : ★][Y : ★]) (→ X Y (Pair X Y))))
+; concrete Pair Int String constructor
+(check-type
+ (inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+       Int String)
+ : (→ Int String (Pair Int String)))
+; Pair Int String value
+(check-type
+ ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+       Int String) 1 "1")
+ : (Pair Int String))
+; fst: parametric
+(check-type
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ : (∀ ([X : ★][Y : ★]) (→ (Pair X Y) X)))
+; fst: concrete Pair Int String accessor
+(check-type
+ (inst
+  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+  Int String)
+ : (→ (Pair Int String) Int))
+; apply fst
+(check-type
+ ((inst
+   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+   Int String)
+  ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+         Int String) 1 "1"))
+ : Int ⇒ 1)
+; snd
+(check-type
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ : (∀ ([X : ★][Y : ★]) (→ (Pair X Y) Y)))
+(check-type
+ (inst
+  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+  Int String)
+ : (→ (Pair Int String) String))
+(check-type
+ ((inst
+   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+   Int String)
+  ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+         Int String) 1 "1"))
+ : String ⇒ "1")
+
+;;; sysf tests wont work, unless augmented with kinds
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
+
+(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
+
+(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
+
+(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
+
+(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
+(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
+; first inst should be discarded
+(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
+; second inst is discarded
+(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
+
+;; polymorphic arguments
+(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
+(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
+(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
+(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
+(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
+(check-type
+ (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
+(check-type
+ ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
+ : Int ⇒ 10)
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
+(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
+             (Λ ([s : ★]) (λ ([y : s]) y)))
+             : Int ⇒ 10)
+
+
+;; previous tests -------------------------------------------------------------
+(check-type 1 : Int)
+(check-not-type 1 : (→ Int Int))
+;(typecheck-fail #f) ; unsupported literal
+(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
+(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
+            : (→ (→ Int Int Int) Int Int Int))
+(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
diff --git a/macrotypes/examples/tests/fomega3-tests.rkt b/macrotypes/examples/tests/fomega3-tests.rkt
new file mode 100644
index 0000000..9a98ede
--- /dev/null
+++ b/macrotypes/examples/tests/fomega3-tests.rkt
@@ -0,0 +1,200 @@
+#lang s-exp "../fomega3.rkt"
+(require "rackunit-typechecking.rkt")
+
+(check-type Int : ★)
+(check-type String : ★)
+(typecheck-fail →)
+(check-type (→ Int Int) : ★)
+(typecheck-fail (→ →))
+(typecheck-fail (→ 1))
+(check-type 1 : Int)
+
+;(check-type (∀ ([t : ★]) (→ t t)) : ★)
+(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
+(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
+
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+
+(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
+            : (∀ ([X : ★]) (→ X X)))
+(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (→ ★ ★)]) (λ ([x : X]) x))))
+
+(check-type (λ ([t : ★]) t) : (→ ★ ★))
+(check-type (λ ([t : ★] [s : ★]) t) : (→ ★ ★ ★))
+(check-type (λ ([t : ★]) (λ ([s : ★]) t)) : (→ ★ (→ ★ ★)))
+(check-type (λ ([t : (→ ★ ★)]) t) : (→ (→ ★ ★) (→ ★ ★)))
+(check-type (λ ([t : (→ ★ ★ ★)]) t) : (→ (→ ★ ★ ★) (→ ★ ★ ★)))
+(check-type (λ ([arg : ★] [res : ★]) (→ arg res)) : (→ ★ ★ ★))
+
+(check-type ((λ ([t : ★]) t) Int) : ★)
+(check-type (λ ([x : ((λ ([t : ★]) t) Int)]) x) : (→ Int Int))
+(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
+(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
+(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
+(typecheck-fail ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
+
+;; partial-apply →
+(check-type ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)
+            : (→ ★ ★))
+; f's type must have kind ★
+(typecheck-fail (λ ([f : ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)]) f))
+(check-type (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) :
+            (∀ ([tyf : (→ ★ ★)]) (→ (tyf String) (tyf String))))
+(check-type (inst
+             (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+             ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+            : (→ (→ Int String) (→ Int String)))
+(typecheck-fail
+ (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1))
+ ;#:with-msg "not a valid type: 1")
+
+;; applied f too early
+(typecheck-fail (inst
+                 (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
+                 ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)))
+(check-type ((inst
+              (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+              ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+             (λ ([x : Int]) "int")) : (→ Int String))
+(check-type (((inst
+               (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+              ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+              (λ ([x : Int]) "int")) 1) : String ⇒ "int")
+
+;; tapl examples, p441
+(typecheck-fail
+ (define-type-alias tmp 1))
+ ;#:with-msg "not a valid type: 1")
+(define-type-alias Id (λ ([X : ★]) X))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (Id String)) Int))
+(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int (Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) (Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) String) Int))
+(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (Id (→ Int String)) Int))
+(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (→ Int String)) Int))
+(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (Id (→ Int String))) Int))
+
+;; tapl examples, p451
+(define-type-alias Pair (λ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
+
+;(check-type Pair : (→ ★ ★ ★))
+(check-type Pair : (→ ★ ★ (∀★ ★)))
+
+(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
+; parametric pair constructor
+(check-type
+ (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ : (∀ ([X : ★][Y : ★]) (→ X Y (Pair X Y))))
+; concrete Pair Int String constructor
+(check-type
+ (inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+       Int String)
+ : (→ Int String (Pair Int String)))
+; Pair Int String value
+(check-type
+ ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+       Int String) 1 "1")
+ : (Pair Int String))
+; fst: parametric
+(check-type
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ : (∀ ([X : ★][Y : ★]) (→ (Pair X Y) X)))
+; fst: concrete Pair Int String accessor
+(check-type
+ (inst
+  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+  Int String)
+ : (→ (Pair Int String) Int))
+; apply fst
+(check-type
+ ((inst
+   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+   Int String)
+  ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+         Int String) 1 "1"))
+ : Int ⇒ 1)
+; snd
+(check-type
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ : (∀ ([X : ★][Y : ★]) (→ (Pair X Y) Y)))
+(check-type
+ (inst
+  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+  Int String)
+ : (→ (Pair Int String) String))
+(check-type
+ ((inst
+   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+   Int String)
+  ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+         Int String) 1 "1"))
+ : String ⇒ "1")
+
+;;; sysf tests wont work, unless augmented with kinds
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
+
+(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
+
+(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
+
+(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
+
+(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
+(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
+; first inst should be discarded
+(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
+; second inst is discarded
+(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
+
+;; polymorphic arguments
+(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
+(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
+(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
+(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
+(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
+(check-type
+ (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
+(check-type
+ ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
+ : Int ⇒ 10)
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
+(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
+             (Λ ([s : ★]) (λ ([y : s]) y)))
+             : Int ⇒ 10)
+
+
+;; previous tests -------------------------------------------------------------
+(check-type 1 : Int)
+(check-not-type 1 : (→ Int Int))
+;(typecheck-fail #f) ; unsupported literal
+(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
+(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
+            : (→ (→ Int Int Int) Int Int Int))
+(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
diff --git a/macrotypes/examples/tests/fsub-tests.rkt b/macrotypes/examples/tests/fsub-tests.rkt
new file mode 100644
index 0000000..4b4deb6
--- /dev/null
+++ b/macrotypes/examples/tests/fsub-tests.rkt
@@ -0,0 +1,153 @@
+#lang s-exp "../fsub.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; examples from tapl ch26, bounded quantification
+;; (same tests from stlc+reco+sub.rkt, but last one should not typecheck)
+(check-type (λ ([x : (× [a : Int])]) x) : (→ (× [a : Int]) (× [a : Int])))
+
+(define ra (tup [a = 0]))
+(check-type ((λ ([x : (× [a : Int])]) x) ra)
+            : (× [a : Int]) ⇒ (tup [a = 0]))
+(define rab (tup [a = 0][b = #t]))
+(check-type ((λ ([x : (× [a : Int])]) x) rab)
+            : (× [a : Int]) ⇒ (tup [a = 0][b = #t]))
+
+(check-type (proj ((λ ([x : (× [a : Int])]) x) rab) a)
+            : Int ⇒ 0)
+
+(check-type (Λ ([X <: Top]) (λ ([x : X]) x)) : (∀ ([X <: Top]) (→ X X)))
+(check-type (inst (Λ ([X <: Top]) (λ ([x : X]) x)) (× [a : Int][b : Bool]))
+            : (→ (× [a : Int][b : Bool]) (× [a : Int][b : Bool])))
+
+(check-type (proj ((inst (Λ ([X <: Top]) (λ ([x : X]) x))
+                         (× [a : Int][b : Bool]))
+                   rab) b)
+            : Bool ⇒ #t)
+
+(define f2 (λ ([x : (× [a : Nat])]) (tup [orig = x] [asucc = (+ 1 (proj x a))])))
+(check-type f2 : (→ (× [a : Nat]) (× [orig : (× [a : Nat])] [asucc : Nat])))
+(check-type (f2 ra) : (× [orig : (× [a : Nat])][asucc : Nat]))
+(check-type (f2 rab) : (× [orig : (× [a : Nat])][asucc : Nat]))
+
+; check expose properly called for primops
+(define fNat (Λ ([X <: Nat]) (λ ([x : X]) (+ x 1))))
+(check-type fNat : (∀ ([X <: Nat]) (→ X Nat)))
+
+;; check type constructors properly call expose
+(define f2poly
+  (Λ ([X <: (× [a : Nat])])
+     (λ ([x : X])
+       (tup [orig = x][asucc = (+ (proj x a) 1)]))))
+
+(check-type f2poly : (∀ ([X <: (× [a : Nat])]) (→ X (× [orig : X][asucc : Nat]))))
+
+; inst f2poly with (× [a : Nat])
+(check-type (inst f2poly (× [a : Nat]))
+            : (→ (× [a : Nat])
+                 (× [orig : (× [a : Nat])][asucc : Nat])))
+(check-type ((inst f2poly (× [a : Nat])) ra)
+            : (× [orig : (× [a : Nat])][asucc : Nat])
+            ⇒ (tup [orig = ra][asucc = 1]))
+
+(check-type ((inst f2poly (× [a : Nat])) rab)
+            : (× [orig : (× [a : Nat])][asucc : Nat])
+            ⇒ (tup [orig = rab][asucc = 1]))
+
+(typecheck-fail (proj (proj ((inst f2poly (× [a : Nat])) rab) orig) b))
+
+;; inst f2poly with (× [a : Nat][b : Bool])
+(check-type (inst f2poly (× [a : Nat][b : Bool]))
+            : (→ (× [a : Nat][b : Bool])
+                 (× [orig : (× [a : Nat][b : Bool])][asucc : Nat])))
+(typecheck-fail ((inst f2poly (× [a : Nat][b : Bool])) ra))
+
+(check-type ((inst f2poly (× [a : Nat][b : Bool])) rab)
+            : (× [orig : (× [a : Nat][b : Bool])][asucc : Nat])
+            ⇒ (tup [orig = rab][asucc = 1]))
+
+(check-type (proj (proj ((inst f2poly (× [a : Nat][b : Bool])) rab) orig) b)
+            : Bool ⇒ #t)
+
+;; make sure inst still checks args
+(typecheck-fail (inst (Λ ([X <: Nat]) 1) Int))
+
+; ch28
+(define f (Λ ([X <: (→ Nat Nat)]) (λ ([y : X]) (y 5))))
+(check-type f : (∀ ([X <: (→ Nat Nat)]) (→ X Nat)))
+(check-type (inst f (→ Nat Nat)) : (→ (→ Nat Nat) Nat))
+(check-type (inst f (→ Int Nat)) : (→ (→ Int Nat) Nat))
+(typecheck-fail (inst f (→ Nat Int)))
+(check-type ((inst f (→ Int Nat)) (λ ([z : Int]) 5)) : Nat)
+(check-type ((inst f (→ Int Nat)) (λ ([z : Num]) 5)) : Nat)
+(typecheck-fail ((inst f (→ Int Nat)) (λ ([z : Nat]) 5)))
+
+
+;; old sysf tests -------------------------------------------------------------
+;; old syntax no longer valid
+;(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))
+;; strings and boolean literals now ok
+;(typecheck-fail "one") ; unsupported literal
+;(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))
+;; edited from sysf test to handle subtyping
+(check-type ((λ ([f : (→ Nat Nat Nat)] [x : Nat] [y : Nat]) (f x y)) + 1 2) : Num ⇒ 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 : Nat]) (+ x x)) 10) : Num ⇒ 20)
diff --git a/macrotypes/examples/tests/run-all-tests.rkt b/macrotypes/examples/tests/run-all-tests.rkt
new file mode 100644
index 0000000..bbb6f14
--- /dev/null
+++ b/macrotypes/examples/tests/run-all-tests.rkt
@@ -0,0 +1,37 @@
+#lang racket
+
+;; stlc and extensions
+(require "stlc-tests.rkt")
+(require "stlc+lit-tests.rkt")
+(require "ext-stlc-tests.rkt")
+(require "stlc+tup-tests.rkt")
+(require "stlc+reco+var-tests.rkt")
+(require "stlc+cons-tests.rkt")
+(require "stlc+box-tests.rkt")
+
+(require "stlc+rec-iso-tests.rkt")
+
+(require "exist-tests.rkt")
+
+;; subtyping
+(require "stlc+sub-tests.rkt")
+(require "stlc+reco+sub-tests.rkt")
+
+;; system F
+(require "sysf-tests.rkt")
+
+(require "fsub-tests.rkt") ; sysf + reco-sub
+
+;; F_omega
+(require "fomega-tests.rkt")
+(require "fomega2-tests.rkt")
+(require "fomega3-tests.rkt")
+
+(require "stlc+occurrence-tests.rkt")
+(require "stlc+overloading-tests.rkt")
+
+;; type inference
+(require "infer-tests.rkt")
+
+;; type and effects
+(require "stlc+effect-tests.rkt")
diff --git a/macrotypes/examples/tests/stlc+rec-iso-tests.rkt b/macrotypes/examples/tests/stlc+rec-iso-tests.rkt
new file mode 100644
index 0000000..edf533a
--- /dev/null
+++ b/macrotypes/examples/tests/stlc+rec-iso-tests.rkt
@@ -0,0 +1,247 @@
+#lang s-exp "../stlc+rec-iso.rkt"
+(require "rackunit-typechecking.rkt")
+
+(define-type-alias IntList (μ (X) (∨ [nil : Unit] [cons : (× Int X)])))
+(define-type-alias ILBody (∨ [nil : Unit] [cons : (× Int IntList)]))
+
+;; nil
+(define nil (fld {IntList} (var nil = (void) as ILBody)))
+(check-type nil : IntList)
+
+;; cons
+(define cons (λ ([n : Int] [lst : IntList]) (fld {IntList} (var cons = (tup n lst) as ILBody))))
+(check-type cons : (→ Int IntList IntList))
+(check-type (cons 1 nil) : IntList)
+(typecheck-fail (cons 1 2))
+(typecheck-fail (cons "1" nil))
+
+;; isnil
+(define isnil
+  (λ ([lst : IntList])
+    (case (unfld {IntList} lst)
+      [nil n => #t]
+      [cons p => #f])))
+(check-type isnil : (→ IntList Bool))
+(check-type (isnil nil) : Bool ⇒ #t)
+(check-type (isnil (cons 1 nil)) : Bool ⇒ #f)
+(typecheck-fail (isnil 1))
+(typecheck-fail (isnil (cons 1 2)))
+(check-type (λ ([f : (→ IntList Bool)]) (f nil)) : (→ (→ IntList Bool) Bool))
+(check-type ((λ ([f : (→ IntList Bool)]) (f nil)) isnil) : Bool ⇒ #t)
+
+;; hd
+(define hd
+  (λ ([lst : IntList])
+    (case (unfld {IntList} lst)
+      [nil n => 0]
+      [cons p => (proj p 0)])))
+(check-type hd : (→ IntList Int))
+(check-type (hd nil) : Int ⇒ 0)
+(typecheck-fail (hd 1))
+(check-type (hd (cons 11 nil)) : Int ⇒ 11)
+
+;; tl
+(define tl
+  (λ ([lst : IntList])
+    (case (unfld {IntList} lst)
+      [nil n => lst]
+      [cons p => (proj p 1)])))
+(check-type tl : (→ IntList IntList))
+(check-type (tl nil) : IntList ⇒ nil)
+(check-type (tl (cons 1 nil)) : IntList ⇒ nil)
+(check-type (tl (cons 1 (cons 2 nil))) : IntList ⇒ (cons 2 nil))
+(typecheck-fail (tl 1))
+
+;; some typecheck failure msgs
+(typecheck-fail
+ (fld {Int} 1)
+ #:with-msg
+ "Expected μ type, got: Int")
+(typecheck-fail
+ (unfld {Int} 1)
+ #:with-msg
+ "Expected μ type, got: Int")
+
+;; previous stlc+var tests ----------------------------------------------------
+;; define-type-alias
+(define-type-alias Integer Int)
+(define-type-alias ArithBinOp (→ Int Int Int))
+;(define-type-alias C Complex) ; error, Complex undefined
+
+(check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer)
+(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int)
+(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Integer)
+(check-type + : ArithBinOp)
+(check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int))
+
+;; records (ie labeled tuples)
+; no records, only tuples
+(check-type "Stephen" : String)
+;(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+;            (× [: "name" String] [: "phone" Int] [: "male?" Bool]))
+;(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+;            : String ⇒ "Stephen")
+;(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+;            : String ⇒ "Stephen")
+;(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone")
+;            : Int ⇒ 781)
+;(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
+;            : Bool ⇒ #t)
+;(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+;                (× [: "my-name" String] [: "phone" Int] [: "male?" Bool]))
+;(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+;                (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
+;(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+;                (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
+
+;; variants
+(check-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit]))
+(check-not-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit] [tea : Unit]))
+(typecheck-fail ((λ ([x : (∨ [coffee : Unit] [tea : Unit])]) x)
+                 (var coffee = (void) as (∨ [coffee : Unit]))))
+(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) : (∨ [coffee : Unit] [tea : Unit]))
+(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
+            : (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
+
+(typecheck-fail
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+   [coffee x => 1])) ; not enough clauses
+(typecheck-fail
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+   [coffee x => 1]
+   [teaaaaaa x => 2])) ; wrong clause
+(typecheck-fail
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+   [coffee x => 1]
+   [tea x => 2]
+   [coke x => 3])) ; too many clauses
+(typecheck-fail
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+   [coffee x => "1"]
+   [tea x => 2])) ; mismatched branch types
+(check-type
+ (case (var coffee = 1 as (∨ [coffee : Int] [tea : Unit]))
+   [coffee x => x]
+   [tea x => 2]) : Int ⇒ 1)
+(define-type-alias Drink (∨ [coffee : Int] [tea : Unit] [coke : Bool]))
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
+(check-type
+ (case ((λ ([d : Drink]) d)
+        (var coffee = 1 as (∨ [coffee : Int] [tea : Unit] [coke : Bool])))
+   [coffee x => (+ (+ x x) (+ x x))]
+   [tea x => 2]
+   [coke y => 3])
+ : Int ⇒ 4)
+
+(check-type
+ (case ((λ ([d : Drink]) d) (var coffee = 1 as Drink))
+   [coffee x => (+ (+ x x) (+ x x))]
+   [tea x => 2]
+   [coke y => 3])
+ : Int ⇒ 4)
+
+;; previous tests: ------------------------------------------------------------
+;; tests for tuples -----------------------------------------------------------
+(check-type (tup 1 2 3) : (× Int Int Int))
+(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int)))
+(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int)))
+(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int)))
+(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int)))
+(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit)))
+
+(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1)
+(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2")
+(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f)
+(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large
+(typecheck-fail
+ (proj 1 2)
+ #:with-msg
+ "Expected × type, got: Int")
+
+;; ext-stlc.rkt tests ---------------------------------------------------------
+;; should still pass
+
+;; new literals and base types
+(check-type "one" : String) ; literal now supported
+(check-type #f : Bool) ; literal now supported
+
+(check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type
+
+;; Unit
+(check-type (void) : Unit)
+(check-type void : (→ Unit))
+(typecheck-fail ((λ ([x : Unit]) x) 2))
+(typecheck-fail ((λ ([x : Unit])) void))
+(check-type ((λ ([x : Unit]) x) (void)) : Unit)
+
+;; begin
+(typecheck-fail (begin))
+(check-type (begin 1) : Int)
+;(typecheck-fail (begin 1 2 3))
+(check-type (begin (void) 1) : Int ⇒ 1)
+
+;;ascription
+(typecheck-fail (ann 1 : Bool))
+(check-type (ann 1 : Int) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
+
+; let
+(check-type (let () (+ 1 1)) : Int ⇒ 2)
+(check-type (let ([x 10]) (+ 1 2)) : Int)
+(typecheck-fail (let ([x #f]) (+ x 1)))
+(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
+(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier
+
+(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
+(typecheck-fail (let* ([x #t] [y (+ x 1)]) 1))
+
+; letrec
+(typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y))
+(typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x))
+
+(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
+
+;; recursive
+(check-type
+ (letrec ([(countdown : (→ Int String))
+           (λ ([i : Int])
+             (if (= i 0)
+                 "liftoff"
+                 (countdown (- i 1))))])
+   (countdown 10)) : String ⇒ "liftoff")
+
+;; mutually recursive
+(check-type
+ (letrec ([(is-even? : (→ Int Bool))
+           (λ ([n : Int])
+             (or (zero? n)
+                 (is-odd? (sub1 n))))]
+          [(is-odd? : (→ Int Bool))
+           (λ ([n : Int])
+             (and (not (zero? n))
+                  (is-even? (sub1 n))))])
+   (is-odd? 11)) : Bool ⇒ #t)
+
+;; tests from stlc+lit-tests.rkt --------------------------
+; most should pass, some failing may now pass due to added types/forms
+(check-type 1 : Int)
+;(check-not-type 1 : (Int → Int))
+;(typecheck-fail "one") ; literal now supported
+;(typecheck-fail #f) ; literal now supported
+(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 now valid type, but arg has wrong type
+;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
+            : (→ (→ Int Int Int) Int Int Int))
+(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+
diff --git a/macrotypes/examples/tests/stlc+reco+sub-tests.rkt b/macrotypes/examples/tests/stlc+reco+sub-tests.rkt
new file mode 100644
index 0000000..c08e02d
--- /dev/null
+++ b/macrotypes/examples/tests/stlc+reco+sub-tests.rkt
@@ -0,0 +1,113 @@
+#lang s-exp "../stlc+reco+sub.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; record subtyping tests
+(check-type "coffee" : String)
+(check-type (tup [coffee = 3]) : (× [coffee : Int])) ; element subtyping
+(check-type (var coffee = 3 as (∨ [coffee : Nat])) : (∨ [coffee : Int])) ; element subtyping
+;err
+(typecheck-fail
+ (var cooffee = 3 as (∨ [coffee : Nat]))
+ #:with-msg "cooffee field does not exist")
+(check-type (tup [coffee = 3]) : (× [coffee : Nat]))
+(check-type (tup [coffee = 3]) : (× [coffee : Top]))
+(check-type (var coffee = 3 as (∨ [coffee : Int])) : (∨ [coffee : Top])) ; element subtyping (twice)
+(check-type (tup [coffee = 3]) : (× [coffee : Num]))
+(check-not-type (tup [coffee = -3]) : (× [coffee : Nat]))
+(check-type (tup [coffee = -3]) : (× [coffee : Num]))
+(check-type (tup [coffee = -3] [tea = 3]) : (× [coffee : Int])) ; width subtyping
+(check-type (tup [coffee = -3] [tea = 3]) : (× [coffee : Num])) ; width+element subtyping
+
+;; record + fns
+(check-type (tup [plus = +]) : (× [plus : (→ Num Num Num)]))
+(check-type + : (→ Num Num Num))
+(check-type (tup [plus = +]) : (× [plus : (→ Int Num Num)]))
+(check-type (tup [plus = +]) : (× [plus : (→ Int Num Top)]))
+(check-type (tup [plus = +] [mul = *]) : (× [plus : (→ Int Num Top)]))
+
+;; examples from tapl ch26, bounded quantification
+(check-type (λ ([x : (× [a : Int])]) x) : (→ (× [a : Int]) (× [a : Int])))
+
+(check-type ((λ ([x : (× [a : Int])]) x) (tup [a = 0]))
+            : (× [a : Int]) ⇒ (tup [a = 0]))
+(check-type ((λ ([x : (× [a : Int])]) x) (tup [a = 0][b = #t]))
+            : (× [a : Int]) ⇒ (tup [a = 0][b = #t]))
+
+(check-type (proj ((λ ([x : (× [a : Int])]) x) (tup [a = 0][b = #t])) a)
+            : Int ⇒ 0)
+
+;; this should work! but needs bounded quantification, see fsub.rkt
+(typecheck-fail (proj ((λ ([x : (× [a : Int])]) x) (tup [a = 0][b = #t])) b))
+
+; conditional
+(check-not-type (λ ([x : Int]) (if #t 1 -1)) : (→ Int Nat))
+(check-type (λ ([x : Int]) (if #t 1 -1)) : (→ Int Int))
+(check-not-type (λ ([x : Int]) (if #t -1 1)) : (→ Int Nat))
+(check-type (λ ([x : Int]) (if #t -1 1)) : (→ Int Int))
+(check-type (λ ([x : Bool]) (if x "1" 1)) : (→ Bool Top))
+
+;; previous record tests ------------------------------------------------------
+;; records (ie labeled tuples)
+(check-type "Stephen" : String)
+(check-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+            (× [name : String] [phone : Int] [male? : Bool]))
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
+            : String ⇒ "Stephen")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
+            : String ⇒ "Stephen")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone)
+            : Int ⇒ 781)
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) male?)
+            : Bool ⇒ #t)
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [my-name : String] [phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [name : String] [my-phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+                (× [name : String] [phone : Int] [is-male? : Bool]))
+
+
+;; previous basic subtyping tests ------------------------------------------------------
+(check-type 1 : Top)
+(check-type 1 : Num)
+(check-type 1 : Int)
+(check-type 1 : Nat)
+(check-type -1 : Top)
+(check-type -1 : Num)
+(check-type -1 : Int)
+(check-not-type -1 : Nat)
+(check-type ((λ ([x : Top]) x) 1) : Top ⇒ 1)
+(check-type ((λ ([x : Top]) x) -1) : Top ⇒ -1)
+(check-type ((λ ([x : Num]) x) -1) : Num ⇒ -1)
+(check-type ((λ ([x : Int]) x) -1) : Int ⇒ -1)
+(typecheck-fail ((λ ([x : Nat]) x) -1))
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([x : Int]) x) : (→ Int Num)) ; covariant output
+(check-not-type (λ ([x : Int]) x) : (→ Int Nat))
+(check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input
+(check-not-type (λ ([x : Int]) x) : (→ Num Int))
+
+;; previous tests -------------------------------------------------------------
+;; some change due to more specific types
+(check-type 1 : Int)
+(check-not-type 1 : (→ Int Int))
+;(typecheck-fail "one") ; unsupported literal
+;(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)
+; Bool now defined
+;(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)
+;; changed test
+(check-type ((λ ([f : (→ Num Num Num)] [x : Int] [y : Int]) (f x y)) + 1 2) : Num ⇒ 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) : Num ⇒ 20)
diff --git a/macrotypes/examples/tests/stlc+sub-tests.rkt b/macrotypes/examples/tests/stlc+sub-tests.rkt
new file mode 100644
index 0000000..752ed5c
--- /dev/null
+++ b/macrotypes/examples/tests/stlc+sub-tests.rkt
@@ -0,0 +1,63 @@
+#lang s-exp "../stlc+sub.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; subtyping tests
+(check-type 1 : Top)
+(check-type 1 : Num)
+(check-type 1 : Int)
+(check-type 1 : Nat)
+(check-type -1 : Top)
+(check-type -1 : Num)
+(check-type -1 : Int)
+(check-not-type -1 : Nat)
+(check-type ((λ ([x : Top]) x) 1) : Top ⇒ 1)
+(check-type ((λ ([x : Top]) x) -1) : Top ⇒ -1)
+(check-type ((λ ([x : Num]) x) -1) : Num ⇒ -1)
+(check-type ((λ ([x : Int]) x) -1) : Int ⇒ -1)
+(typecheck-fail ((λ ([x : Nat]) x) -1))
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([x : Int]) x) : (→ Int Num)) ; covariant output
+(check-not-type (λ ([x : Int]) x) : (→ Int Nat))
+(check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input
+(check-not-type (λ ([x : Int]) x) : (→ Num Int))
+
+(check-type ((λ ([f : (→ Int Int)]) (f -1)) add1) : Int ⇒ 0)
+(check-type ((λ ([f : (→ Nat Int)]) (f 1)) add1) : Int ⇒ 2)
+(typecheck-fail ((λ ([f : (→ Num Int)]) (f 1.1)) add1))
+(check-type ((λ ([f : (→ Nat Num)]) (f 1)) add1) : Num ⇒ 2)
+(typecheck-fail ((λ ([f : (→ Num Num)]) (f 1.1)) add1))
+
+(check-type + : (→ Num Num Num))
+(check-type + : (→ Int Num Num))
+(check-type + : (→ Int Int Num))
+(check-not-type + : (→ Top Int Num))
+(check-not-type + : (→ Top Int Int))
+(check-type + : (→ Nat Int Top))
+
+;; previous tests -------------------------------------------------------------
+;; some change due to more specific types
+(check-type 1 : Int)
+(check-not-type 1 : (→ Int Int))
+(check-type "one" : String) 
+(check-type #f : Bool)
+(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 : Sym]) x) 1)) ; Sym is not valid type
+(typecheck-fail (λ ([x : Sym]) x)) ; Sym 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)
+;; changed test
+(check-type ((λ ([f : (→ Num Num Num)] [x : Int] [y : Int]) (f x y)) + 1 2) : Num ⇒ 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) : Num ⇒ 20)
+
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-not-type (λ ([x : Int] [y : Int]) x) : (→ Int Int))
+(check-not-type (λ ([x : Int]) x) : (→ Int Int Int Int))
diff --git a/macrotypes/examples/tests/sysf-tests.rkt b/macrotypes/examples/tests/sysf-tests.rkt
new file mode 100644
index 0000000..3aed40d
--- /dev/null
+++ b/macrotypes/examples/tests/sysf-tests.rkt
@@ -0,0 +1,76 @@
+#lang s-exp "../sysf.rkt"
+(require "rackunit-typechecking.rkt")
+
+(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))
+
+;; inst err
+(typecheck-fail
+ (inst 1 Int)
+ #:with-msg
+ "Expected ∀ type, got: 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)
+
+; ∀ errs
+(typecheck-fail (λ ([x : (∀ (y) (+ 1 y))]) x))
+
+;; previous tests -------------------------------------------------------------
+(check-type 1 : Int)
+(check-not-type 1 : (→ Int Int))
+(typecheck-fail "one") ; unsupported literal
+(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)