diff --git a/tapl/README.md b/tapl/README.md
index f8bde6a..dc86988 100644
--- a/tapl/README.md
+++ b/tapl/README.md
@@ -6,12 +6,13 @@ A file extends its immediate parent file.
    - stlc+lit.rkt
      - ext-stlc.rkt
        - stlc+tup.rkt
-         - stlc+var.rkt
+         - stlc+reco+var.rkt
            - stlc+cons.rkt
              - stlc+box.rkt
            - stlc+rec-iso.rkt
+           - exist.rkt
      - stlc+sub.rkt
-       - stlc+rec+sub.rkt (also pull in tup from stlc+var.rkt)
+       - stlc+reco+sub.rkt (also pull in tup from stlc+reco+var.rkt)
      - sysf.rkt
        - fomega.rkt
        - fomega2.rkt
\ No newline at end of file
diff --git a/tapl/exist.rkt b/tapl/exist.rkt
new file mode 100644
index 0000000..1f105f5
--- /dev/null
+++ b/tapl/exist.rkt
@@ -0,0 +1,12 @@
+#lang racket/base
+(require "typecheck.rkt")
+(require (except-in "stlc+reco+var.rkt" #%app λ)
+         (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ)))
+(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
+(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app stlc:λ))
+ 
+;; existential types
+;; Types:
+;; - types from stlc+reco+var.rkt
+;; Terms:
+;; - terms from stlc+reco+var.rkt
diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt
index 7cf6243..14c9661 100644
--- a/tapl/stlc+cons.rkt
+++ b/tapl/stlc+cons.rkt
@@ -1,17 +1,17 @@
 #lang racket/base
 (require "typecheck.rkt")
-(require (prefix-in stlc: (only-in "stlc+var.rkt" #%app))
-         (except-in "stlc+var.rkt" #%app))
+(require (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app))
+         (except-in "stlc+reco+var.rkt" #%app))
 (provide (rename-out [stlc:#%app #%app] [cons/tc cons]))
-(provide (except-out (all-from-out "stlc+var.rkt") stlc:#%app))
+(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app))
 (provide nil isnil head tail)
 
 ;; Simply-Typed Lambda Calculus, plus cons
 ;; Types:
-;; - types from stlc+var.rkt
+;; - types from stlc+reco+var.rkt
 ;; - List constructor
 ;; Terms:
-;; - terms from stlc+var.rkt
+;; - terms from stlc+reco+var.rkt
 
 ;; TODO: enable HO use of list primitives
 
diff --git a/tapl/stlc+rec-iso.rkt b/tapl/stlc+rec-iso.rkt
new file mode 100644
index 0000000..67e97ab
--- /dev/null
+++ b/tapl/stlc+rec-iso.rkt
@@ -0,0 +1,52 @@
+#lang racket/base
+(require "typecheck.rkt")
+(require (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ type=?))
+         (except-in "stlc+reco+var.rkt" #%app λ type=?))
+(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
+(provide (except-out (all-from-out "stlc+reco+var.rkt")
+                     stlc:#%app stlc:λ (for-syntax stlc:type=?)))
+(provide μ fld unfld (for-syntax type=?))
+
+;; stlc + (iso) recursive types
+;; Types:
+;; - types from stlc+reco+var.rkt
+;; - μ
+;; Terms:
+;; - terms from stlc+reco+var.rkt
+;; - fld/unfld
+
+(begin-for-syntax
+  ;; extend to handle μ
+  (define (type=? τ1 τ2)
+    ;(printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
+    ;(printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2))
+    (syntax-parse (list τ1 τ2)
+      [(((~literal #%plain-lambda) (x:id ...) k1 ... t1)
+        ((~literal #%plain-lambda) (y:id ...) k2 ... t2))
+       #:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
+       #:with (z ...) (generate-temporaries #'(x ...))
+       ((current-type=?) (substs #'(z ...) #'(x ...) #'t1)
+                         (substs #'(z ...) #'(y ...) #'t2))]
+      [_ (stlc:type=? τ1 τ2)]))
+  (current-type=? type=?)
+  (current-typecheck-relation type=?))
+
+(define-syntax (μ stx)
+  (syntax-parse stx
+    [(_ (tv:id) τ_body)
+     #'(λ (tv) τ_body)]))
+
+(define-syntax (unfld stx)
+  (syntax-parse stx
+    [(_ τ:ann e)
+     #:with ((~literal #%plain-lambda) (tv:id) τ_body) #'τ.norm
+     #:with [e- τ_e] (infer+erase #'e)
+     #:when ((current-typecheck-relation) #'τ_e #'τ.norm)
+     (⊢ #'e- (subst #'τ.norm #'tv #'τ_body))]))
+(define-syntax (fld stx)
+  (syntax-parse stx
+    [(_ τ:ann e)
+     #:with ((~literal #%plain-lambda) (tv:id) τ_body) #'τ.norm
+     #:with [e- τ_e] (infer+erase #'e)
+     #:when ((current-typecheck-relation) #'τ_e (subst #'τ.norm #'tv #'τ_body))
+     (⊢ #'e- #'τ.norm)]))
\ No newline at end of file
diff --git a/tapl/stlc+rec+sub.rkt b/tapl/stlc+reco+sub.rkt
similarity index 86%
rename from tapl/stlc+rec+sub.rkt
rename to tapl/stlc+reco+sub.rkt
index 40ecbc8..1215835 100644
--- a/tapl/stlc+rec+sub.rkt
+++ b/tapl/stlc+reco+sub.rkt
@@ -1,15 +1,15 @@
 #lang racket/base
 (require "typecheck.rkt")
-;; want to use type=? and eval-type from stlc+var.rkt, not stlc+sub.rkt
+;; want to use type=? and eval-type from stlc+reco+var.rkt, not stlc+sub.rkt
 (require (except-in "stlc+sub.rkt" #%app #%datum sub? type=? type-eval)
          (prefix-in stlc: (only-in "stlc+sub.rkt" #%app #%datum sub?))
-         (except-in "stlc+var.rkt" #%app #%datum +)
-         (prefix-in var: (only-in "stlc+var.rkt" #%datum)))
+         (except-in "stlc+reco+var.rkt" #%app #%datum +)
+         (prefix-in var: (only-in "stlc+reco+var.rkt" #%datum)))
 (provide (rename-out [stlc:#%app #%app]
                      [datum/tc #%datum]))
 (provide (except-out (all-from-out "stlc+sub.rkt") stlc:#%app stlc:#%datum
                      (for-syntax stlc:sub?))
-         (except-out (all-from-out "stlc+var.rkt") var:#%datum))
+         (except-out (all-from-out "stlc+reco+var.rkt") var:#%datum))
 (provide (for-syntax sub?))
 
 ;; Simply-Typed Lambda Calculus, plus subtyping, plus records
diff --git a/tapl/stlc+var.rkt b/tapl/stlc+reco+var.rkt
similarity index 97%
rename from tapl/stlc+var.rkt
rename to tapl/stlc+reco+var.rkt
index d514cd6..f0db35b 100644
--- a/tapl/stlc+var.rkt
+++ b/tapl/stlc+reco+var.rkt
@@ -11,7 +11,7 @@
 (provide (for-syntax type=?))
 
 
-;; Simply-Typed Lambda Calculus, plus variants
+;; Simply-Typed Lambda Calculus, plus records and variants
 ;; Type relations:
 ;; - type=? extended to strings
 ;; define-type-alias (also provided to programmer)
diff --git a/tapl/tests/stlc+var-tests.rkt b/tapl/tests/exist-tests.rkt
similarity index 99%
rename from tapl/tests/stlc+var-tests.rkt
rename to tapl/tests/exist-tests.rkt
index 9675b05..6dfb462 100644
--- a/tapl/tests/stlc+var-tests.rkt
+++ b/tapl/tests/exist-tests.rkt
@@ -1,4 +1,4 @@
-#lang s-exp "../stlc+var.rkt"
+#lang s-exp "../exist.rkt"
 (require "rackunit-typechecking.rkt")
 
 ;; define-type-alias
diff --git a/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
index 8baa25a..649eb03 100644
--- a/tapl/tests/run-all-tests.rkt
+++ b/tapl/tests/run-all-tests.rkt
@@ -3,15 +3,16 @@
 (require "stlc+lit-tests.rkt")
 (require "ext-stlc-tests.rkt")
 (require "stlc+tup-tests.rkt")
-(require "stlc+var-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 "stlc+sub-tests.rkt")
-(require "stlc+rec+sub-tests.rkt")
+(require "stlc+reco+sub-tests.rkt")
 
 (require "sysf-tests.rkt")
+(require "exist-tests.rkt")
 (require "fomega-tests.rkt")
 (require "fomega2-tests.rkt")
\ No newline at end of file
diff --git a/tapl/tests/stlc+rec-iso-tests.rkt b/tapl/tests/stlc+rec-iso-tests.rkt
new file mode 100644
index 0000000..09154c6
--- /dev/null
+++ b/tapl/tests/stlc+rec-iso-tests.rkt
@@ -0,0 +1,231 @@
+#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))
+
+;; 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)
+(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)) ; 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/tapl/tests/stlc+rec+sub-tests.rkt b/tapl/tests/stlc+reco+sub-tests.rkt
similarity index 99%
rename from tapl/tests/stlc+rec+sub-tests.rkt
rename to tapl/tests/stlc+reco+sub-tests.rkt
index e0e538b..474ae32 100644
--- a/tapl/tests/stlc+rec+sub-tests.rkt
+++ b/tapl/tests/stlc+reco+sub-tests.rkt
@@ -1,4 +1,4 @@
-#lang s-exp "../stlc+rec+sub.rkt"
+#lang s-exp "../stlc+reco+sub.rkt"
 (require "rackunit-typechecking.rkt")
 
 ;; record subtyping tests
diff --git a/tapl/tests/stlc+reco+var-tests.rkt b/tapl/tests/stlc+reco+var-tests.rkt
new file mode 100644
index 0000000..241a42d
--- /dev/null
+++ b/tapl/tests/stlc+reco+var-tests.rkt
@@ -0,0 +1,181 @@
+#lang s-exp "../stlc+reco+var.rkt"
+(require "rackunit-typechecking.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 -----------------------------------------------------------
+(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)
+