diff --git a/stlc-tests.rkt b/stlc-tests.rkt
index cd464e4..7e5f556 100644
--- a/stlc-tests.rkt
+++ b/stlc-tests.rkt
@@ -62,8 +62,10 @@
                        : Int => 6)
 
 ; define
-(define (g [y : Int]) (+ (f y) 1))
-(define (f [x : Int]) (+ x 1))
+(define (g [y : Int]) : Int
+  (+ (f y) 1))
+(define (f [x : Int]) : Int
+  (+ x 1))
 (check-type-and-result (f 10) : Int => 11)
 (check-type-and-result (g 100) : Int => 102)
 (check-not-type (f 10) : String)
@@ -77,8 +79,9 @@
 (check-type-error (if 1 2 3))
 
 ;;; recursive fn
-(define (add1 [x : Int]) (+ x 1))
-(define (map [f : (→ Int Int)] [lst : (Listof Int)])
+(define (add1 [x : Int]) : Int
+  (+ x 1))
+(define (map [f : (→ Int Int)] [lst : (Listof Int)]) : (Listof Int)
   (if (null? {Int} lst)
       (null {Int})
       (cons {Int} (f (first {Int} lst)) (map f (rest {Int} lst)))))
@@ -89,9 +92,9 @@
                 : (Listof String))
 
 ;; recursive types
-(define (a [x : Int]) (b x))
-(define (b [x : Int]) (a x))
-(define (ff [x : Int]) (ff x))
+(define (a [x : Int]) : Int (b x))
+(define (b [x : Int]) : Int (a x))
+(define (ff [x : Int]) : Int (ff x))
 
 ;; define-type (non parametric)
 (define-type MaybeInt (variant (None) (Just Int)))
@@ -99,7 +102,7 @@
 (check-type (Just 10) : MaybeInt)
 (check-type-error (Just "ten"))
 (check-type-error (Just (None)))
-(define (maybeint->bool [maybint : MaybeInt])
+(define (maybeint->bool [maybint : MaybeInt]) : Bool
   (cases maybint
    [None () #f]
    [Just (x) #t]))
@@ -116,7 +119,7 @@
 (check-type-and-result (Cons 1 (Null)) : IntList => (Cons 1 (Null)))
 (check-type-error (Cons "one" (Null)))
 (check-type-error (Cons 1 2))
-(define (map/IntList [f : (→ Int Int)] [lst : IntList])
+(define (map/IntList [f : (→ Int Int)] [lst : IntList]) : IntList
   (cases lst
     [Null () (Null)]
     [Cons (x xs) (Cons (f x) (map/IntList f xs))]))
@@ -126,7 +129,7 @@
                        : IntList => (Cons 3 (Cons 2 (Null))))
 (check-type-error (map/IntList (λ ([n : Int]) #f) (Null)))
 (define-type BoolList (variant (BoolNull) (BoolCons Bool BoolList)))
-(define (map/BoolList [f : (→ Bool Int)] [lst : BoolList])
+(define (map/BoolList [f : (→ Bool Int)] [lst : BoolList]) : IntList
   (cases lst
     [BoolNull () (Null)]
     [BoolCons (x xs) (Cons (f x) (map/BoolList f xs))]))
diff --git a/stlc.rkt b/stlc.rkt
index 4fad91a..442201f 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -43,7 +43,7 @@
      #'(begin
          (struct Cons (x ...) #:transparent) ...)]))
 (define-syntax (cases stx)
-  (syntax-parse stx
+  (syntax-parse stx #:literals (→)
     [(_ e [Cons (x ...) body ... body_result] ...)
      #:with e+ (expand/df #'e)
      #:with (Cons+ ...) (stx-map expand/df #'(Cons ...))
@@ -188,9 +188,10 @@
 ;; define, module-begin -------------------------------------------------------
 (define-syntax (define/tc stx)
   (syntax-parse stx #:datum-literals (:)
-    [(_ (f:id [x:id : τ] ...) e ...)
-     #:with τ_result (generate-temporary #'f)
-     #:when (fvs (set-add (fvs) (syntax->datum #'τ_result)))
+    [(_ (f:id [x:id : τ] ...) : τ_result e ...)
+;     #:with τ_result (generate-temporary #'f)
+;     #:when (fvs (set-add (fvs) (syntax->datum #'τ_result)))
+;     #:when (fv=>f (fv=>f-set #'τ_result #'f))
      #:when (Γ (type-env-extend #'([f (→ τ ... τ_result)])))
      #'(define f (λ/tc ([x : τ] ...) e ...))]
     [(_ x:id e) #'(define x e)]))
@@ -206,7 +207,7 @@
   ;; Similarly, I had to define the define-type pattern below to avoid explicitly
   ;; mentioning define-type on the rhs, otherwise it would again lock in the stlc
   ;; version of define-type.
-  (define-syntax-class maybe-def #:datum-literals (: define variant define-type)
+  (define-syntax-class maybe-def #:datum-literals (define variant define-type)
     (pattern define-fn
              #:with (define (f x ...) body ...) #'define-fn
              #:attr fndef #'(define-fn)
@@ -264,7 +265,7 @@
                            (letrec-values ([f v] ...) e ... (void)))))
         (define #,(datum->syntax stx 'runtime-env)
           (for/hash ([x:τ '#,(map (λ (xτ) (cons (car xτ) (syntax->datum (cdr xτ))))
-                                  (hash->list (do-subst (Γ))))])
+                                  (hash->list (Γ)))]);(do-subst (Γ))))])
             (values (car x:τ) (cdr x:τ))))
         ))]))
 
diff --git a/sysf-tests.rkt b/sysf-tests.rkt
index 7842628..e23599e 100644
--- a/sysf-tests.rkt
+++ b/sysf-tests.rkt
@@ -6,4 +6,18 @@
 (check-type (Just {Int} 1) : (Maybe Int))
 (check-type-error (Just {Int} #f))
 (check-not-type (Just {Int} 1) : (Maybe Bool))
-(check-type (λ {X} ([x : X]) x) : (∀ (X) (→ X X)))
\ No newline at end of file
+(check-type (λ {X} ([x : X]) x) : (∀ (X) (→ X X)))
+(check-type-error ((λ ([x : X]) x) 1))
+
+;; lists
+(define-type (Listof X) (variant (Null) (Cons X (Listof X))))
+(check-type (Null {Int}) : (Listof Int))
+(check-type (Cons {Int} 1 (Null {Int})) : (Listof Int))
+(define (map {A B} [f : (→ A B)] [lst : (Listof A)]) : (Listof B)
+  (cases {A} lst
+    [Null () (Null {B})]
+    [Cons (x xs) (Cons {B} (f {A B} x) (map {A B} f xs))]))
+(define (add1 [x : Int]) : Int (+ x 1))
+(check-type-and-result 
+ (map {Int Int} add1 (Cons {Int} 1 (Cons {Int} 2 (Null {Int}))))
+ : (Listof Int) => (Cons {Int} 2 (Cons {Int} 3 (Null {Int}))))
\ No newline at end of file
diff --git a/sysf.rkt b/sysf.rkt
index a68067c..ce8f429 100644
--- a/sysf.rkt
+++ b/sysf.rkt
@@ -1,5 +1,6 @@
 #lang racket/base
 (require 
+  racket/match
   (for-syntax 
    racket/base syntax/parse syntax/parse/experimental/template
    syntax/stx racket/syntax racket/set
@@ -9,16 +10,22 @@
 (require 
   (except-in 
    "stlc.rkt" 
-   define-type begin #%app λ
+   define-type cases begin #%app λ define
    check-type-error check-type check-type-and-result check-not-type check-equal?))
-(require (prefix-in stlc: (only-in "stlc.rkt" #%app define-type λ begin)))
+(require 
+  (prefix-in stlc: 
+    (only-in 
+     "stlc.rkt" 
+     define-type cases begin #%app λ define)))
 (provide (all-from-out "stlc.rkt"))
 (provide 
- define-type
+ define-type cases
  (rename-out 
   [stlc:begin begin]
   [app/tc #%app]
-  [λ/tc λ]))
+  [λ/tc λ] [define/tc define]))
+
+(define-and-provide-builtin-types ∀)
 
 ;; define-type ----------------------------------------------------------------
 (define-syntax (define-type stx)
@@ -30,6 +37,34 @@
          (struct Cons (x ...) #:transparent) ...)]
     [(_ any ...) #'(stlc:define-type any ...)]))
 
+;; cases ----------------------------------------------------------------------
+(define-syntax (cases stx)
+  (syntax-parse stx #:literals (∀)
+    [(_ τs e [Cons (x ...) body ... body_result] ...)
+     #:when (curly-parens? #'τs)
+     #:with e+ (expand/df #'e)
+     #:with (Cons+ ...) (stx-map expand/df #'(Cons ...))
+     #:with ((∀ Xs ∀body) ...) (stx-map typeof #'(Cons+ ...))
+     #:with ((→ τ ... τ_Cons) ...) 
+            (stx-map (λ (forall) (apply-forall forall #'τs)) #'((∀ Xs ∀body) ...))
+     #:when (stx-andmap (λ (τ) (assert-type #'e+ τ)) #'(τ_Cons ...))
+     #:with ((lam (x+ ...) body+ ... body_result+) ...) 
+            (stx-map (λ (bods xs τs) 
+                       (with-extended-type-env 
+                        (stx-map list xs τs)
+                        (expand/df #`(λ #,xs #,@bods))))
+                     #'((body ... body_result) ...)
+                     #'((x ...) ...)
+                     #'((τ ...) ...))
+     #:when (stx-andmap (λ (bods) (stx-andmap assert-Unit-type bods)) #'((body+ ...) ...))
+     #:with (τ_result ...) (stx-map typeof #'(body_result+ ...))
+     #:when (or (null? (syntax->list #'(τ_result ...)))
+                (andmap (λ (τ) (type=? τ (car (syntax->list #'(τ_result ...)))))
+                        (cdr (syntax->list #'(τ_result ...)))))
+     (⊢ (syntax/loc stx (match e+ [(Cons+ x+ ...) body+ ... body_result+] ...))
+        (car (syntax->list #'(τ_result ...))))]
+    [(_ any ...) #:when (displayln "stlc:cases") #'(stlc:cases any ...)]))
+
 ;; lambda ---------------------------------------------------------------------
 (define-syntax (λ/tc stx)
   (syntax-parse stx #:datum-literals (:)
@@ -56,6 +91,20 @@
      (⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(∀ τs (→ τ ... τ_body)))]
     [(_ any ...) #'(stlc:λ any ...)]))
 
+; define ----------------------------------------------------------------------
+(define-syntax (define/tc stx)
+  (syntax-parse stx #:datum-literals (:)
+    ;; most of the code from this case, except for the curly? check,
+    ;; is copied from stlc:define
+    [(_ (f:id τs [x:id : τ] ...) : τ_result e ...)
+     #:when (curly-parens? #'τs)
+;     #:with τ_result (generate-temporary #'f)
+;     #:when (fvs (set-add (fvs) (syntax->datum #'τ_result)))
+;     #:when (fv=>f (fv=>f-set #'τ_result #'f))
+     #:when (Γ (type-env-extend #'([f (∀ τs (→ τ ... τ_result))])))
+     #'(define f (λ/tc τs ([x : τ] ...) e ...))]
+    [(_ any ...) #'(stlc:define any ...)]))
+
 ; #%app -----------------------------------------------------------------------
 (define-syntax (app/tc stx)
   (syntax-parse stx #:literals (→ void)
@@ -66,6 +115,10 @@
      #:with (→ τ_arg ... τ_res) (apply-forall (typeof #'e_fn+) #'τs)
      #:when (stx-andmap assert-type #'(e_arg+ ...) #'(τ_arg ...))
      (⊢ (syntax/loc stx (#%app e_fn+ e_arg+ ...)) #'τ_res)]
+    ;; handle type apply of non-poly fn here; just pass through
+    [(_ e_fn τs e_arg ...)
+     #:when (curly-parens? #'τs)
+     #'(stlc:#%app e_fn e_arg ...)]
     [(_ any ...) #'(stlc:#%app any ...)]))
 
 ;; testing fns ----------------------------------------------------------------
diff --git a/typecheck.rkt b/typecheck.rkt
index e499253..9f234d9 100644
--- a/typecheck.rkt
+++ b/typecheck.rkt
@@ -17,22 +17,22 @@
 (define-for-syntax (type=? τ1 τ2)
 ;  (printf "type= ~a ~a\n" (syntax->datum τ1) (syntax->datum τ2))
   (syntax-parse #`(#,τ1 #,τ2)
-    [(x:id τ)
-     #:when (and (set-member? (fvs) (syntax->datum #'x))
-                 (hash-has-key? (fvs-subst) (syntax->datum #'x)))
-     (type=? (hash-ref (fvs-subst) (syntax->datum #'x)) #'τ)]
-    [(x:id τ)
-     #:when (set-member? (fvs) (syntax->datum #'x))
-     #:when (fvs-subst (fvs-subst-set #'x #'τ))
-     #t]
-    [(τ x:id)
-     #:when (and (set-member? (fvs) (syntax->datum #'x))
-                 (hash-has-key? (fvs-subst) (syntax->datum #'x)))
-     (type=? (hash-ref (fvs-subst) (syntax->datum #'x)) #'τ)]
-    [(τ x:id)
-     #:when (set-member? (fvs) (syntax->datum #'x))
-     #:when (fvs-subst (fvs-subst-set #'x #'τ))
-     #t]
+;    [(x:id τ)
+;     #:when (and (set-member? (fvs) (syntax->datum #'x))
+;                 (hash-has-key? (fvs-subst) (syntax->datum #'x)))
+;     (type=? (hash-ref (fvs-subst) (syntax->datum #'x)) #'τ)]
+;    [(x:id τ)
+;     #:when (set-member? (fvs) (syntax->datum #'x))
+;     #:when (fvs-subst (fvs-subst-set #'x #'τ))
+;     #t]
+;    [(τ x:id)
+;     #:when (and (set-member? (fvs) (syntax->datum #'x))
+;                 (hash-has-key? (fvs-subst) (syntax->datum #'x)))
+;     (type=? (hash-ref (fvs-subst) (syntax->datum #'x)) #'τ)]
+;    [(τ x:id)
+;     #:when (set-member? (fvs) (syntax->datum #'x))
+;     #:when (fvs-subst (fvs-subst-set #'x #'τ))
+;     #t]
     [(x:id y:id) (free-identifier=? τ1 τ2)]
     [((tycon1 τ1 ...) (tycon2 τ2 ...)) 
      (and (free-identifier=? #'tycon1 #'tycon2)
@@ -42,6 +42,7 @@
 
 ;; return #t if (typeof e)=τ, else type error
 (define-for-syntax (assert-type e τ)
+;  (printf "~a has type ~a; expected: ~a\n" (syntax->datum e) (syntax->datum (typeof e)) (syntax->datum τ))
   (or (type=? (typeof e) τ)
       (error 'TYPE-ERROR "~a (~a:~a) has type ~a, but should have type ~a"
              (syntax->datum e)
@@ -81,22 +82,25 @@
        #'(parameterize ([Γ (type-env-extend x-τs)]) e)]))
 
   ;; generated type vars
-  (define fvs (make-parameter (set)))
-  (define fvs-subst (make-parameter (hash)))
-  (define (fvs-subst-set x τ)
-    (hash-set (fvs-subst) (syntax->datum x) τ))
-  (define (do-subst/τ τ)
-    (syntax-parse τ
-      [x:id
-       #:when (set-member? (fvs) (syntax->datum #'x))
-       (hash-ref (fvs-subst) (syntax->datum #'x) #'???)]
-      [τ:id #'τ]
-      [(tycon τ ...)
-       #:with (τ-subst ...) (stx-map do-subst/τ #'(τ ...))
-       #'(tycon τ-subst ...)]))
-  (define (do-subst h)
-    (for/hash ([(x τ) (in-hash h)])
-      (values x (do-subst/τ τ)))))
+;  (define fvs (make-parameter (set)))
+;  (define fv=>f (make-parameter (hash)))
+;  (define (fv=>f-set fv f) (hash-set (fv=>f) (syntax->datum fv) f))
+;  (define fvs-subst (make-parameter (hash)))
+;  (define (fvs-subst-set x τ)
+;    (hash-set (fvs-subst) (syntax->datum x) τ))
+;  (define (do-subst/τ τ)
+;    (syntax-parse τ
+;      [x:id
+;       #:when (set-member? (fvs) (syntax->datum #'x))
+;       (hash-ref (fvs-subst) (syntax->datum #'x) #'???)]
+;      [τ:id #'τ]
+;      [(tycon τ ...)
+;       #:with (τ-subst ...) (stx-map do-subst/τ #'(τ ...))
+;       #'(tycon τ-subst ...)]))
+;  (define (do-subst h)
+;    (for/hash ([(x τ) (in-hash h)])
+;      (values x (do-subst/τ τ)))))
+)
 
 ;; apply-forall ---------------------------------------------------------------
 (define-for-syntax (apply-forall ∀τ τs)