diff --git a/stlc.rkt b/stlc.rkt
index 2e5278e..f10711b 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -2,9 +2,10 @@
 (require 
   racket/match
   (for-syntax racket/base syntax/parse syntax/parse/experimental/template 
-              racket/set syntax/id-table syntax/stx racket/list racket/syntax
+              racket/set syntax/stx racket/syntax
               "stx-utils.rkt")
-  (for-meta 2 racket/base syntax/parse))
+  (for-meta 2 racket/base syntax/parse)
+  "typecheck.rkt")
 (provide 
  (except-out
   (all-from-out racket/base) 
@@ -28,39 +29,9 @@
 ;; - user (recursive) function definitions
 ;; - user (recursive) (variant) type-definitions
 
-;; for types, just need the identifier bound
-(define-syntax-rule (define-builtin-type τ) (begin (define τ #f)  (provide τ)))
-(define-syntax-rule (define-builtin-types τ ...) (begin (define-builtin-type τ) ...))
-(define-builtin-types Int String Bool → Listof Unit)
-
-;; type environment
-(begin-for-syntax
-  (define base-type-env (hash))
-  ;; Γ : [Hashof var-symbol => type-stx]
-  ;; - can't use free-identifier=? for the hash table (or free-id-table)
-  ;;   because env must be set before expanding λ body (ie before going under λ)
-  ;;   so x's in the body won't be free-id=? to the one in the table
-  ;; use symbols instead of identifiers for now --- should be fine because
-  ;; I'm manually managing the environment
-  (define Γ (make-parameter base-type-env))
-  
-  ;; 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-and-provide-builtin-types Int String Bool → Listof Unit)
+(define-for-syntax (assert-Unit-type e) (assert-type e #'Unit))
+(define-for-syntax (assert-Int-type e) (assert-type e #'Int))
 
 ;; testing fns ----------------------------------------------------------------
 (require (for-syntax rackunit))
@@ -94,86 +65,6 @@
 (provide (rename-out [my-check-equal? check-equal?]))
 (define-syntax-rule (my-check-equal? x y) (check-equal? x y))
 
-(define-for-syntax (type=? τ1 τ2)
-;  (printf "type= ~a ~a\n" (syntax->datum τ1) (syntax->datum τ2))
-  (syntax-parse #`(#,τ1 #,τ2) #:literals (→)
-    [(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)
-          (= (length (syntax->list #'(τ1 ...))) (length (syntax->list #'(τ2 ...))))
-          (stx-andmap type=? #'(τ1 ...) #'(τ2 ...)))]
-    [_ #f]))
-
-;; return #t if (typeof e)=τ, else type error
-(begin-for-syntax
-  (define (assert-type e τ)
-    (or (type=? (typeof e) τ)
-         (error 'TYPE-ERROR "~a (~a:~a) has type ~a, but should have type ~a"
-               (syntax->datum e)
-               (syntax-line e) (syntax-column e)
-               (syntax->datum (typeof e))
-               (syntax->datum τ))))
-  (define (assert-Unit-type e) (assert-type e #'Unit))
-  (define (assert-Int-type e) (assert-type e #'Int)))
-
-;; type env and other helper fns ----------------------------------------------
-;; attaches type τ to e (as syntax property)
-(define-for-syntax (⊢ e τ) (syntax-property e 'type τ))
-
-;; retrieves type of τ (from syntax property)
-(define-for-syntax (typeof stx) (syntax-property stx 'type))
-
-(define-for-syntax (type-env-lookup x) (hash-ref (Γ) (syntax->datum x)))
-;; returns a new hash table extended with type associations x:τs
-(define-for-syntax (type-env-extend x:τs)
-  (define xs (stx-map stx-car x:τs))
-  (define τs (stx-map stx-cadr x:τs))
-  (apply hash-set* (Γ) (append-map (λ (x τ) (list (syntax->datum x) τ)) xs τs)))
-;; must be macro because type env must be extended first, before expandinb body
-(begin-for-syntax
-  (define-syntax (with-extended-type-env stx)
-    (syntax-parse stx
-      [(_ x-τs e)
-       #'(parameterize ([Γ (type-env-extend x-τs)]) e)])))
-
-;; expand/df ------------------------------------------------------------------
-;; depth-first expand
-(define-for-syntax (expand/df e [ctx #f])
-;  (printf "expanding: ~a\n" e)
-;  (printf "typeenv: ~a\n" (Γ))
-  (cond
-    ;; 1st case handles struct constructors that are not the same name as struct
-    ;; (should always be an identifier)
-    [(syntax-property e 'constructor-for) => (λ (Cons) 
-     (⊢ e (type-env-lookup Cons)))]
-    ;; 2nd case handles identifiers that are not struct constructors
-    [(identifier? e) (⊢ e (type-env-lookup e))] ; handle this here bc there's no #%var form
-    ;; local-expand must expand all the way down, ie have no stop-list, ie stop list can't be #f
-    ;; ow forms like lambda and app won't get properly assigned types
-    [else (local-expand e 'expression null ctx)]))
-(define-for-syntax (expand/df/module-ctx def)
-  (local-expand def 'module #f))
-(define-for-syntax (expand/df/mb-ctx def)
-  (local-expand def 'module-begin #f))
-
-
-
 ;; define-type ----------------------------------------------------------------
 (define-syntax (define-type stx)
   (syntax-parse stx #:datum-literals (variant)
diff --git a/typecheck.rkt b/typecheck.rkt
new file mode 100644
index 0000000..fb502ad
--- /dev/null
+++ b/typecheck.rkt
@@ -0,0 +1,120 @@
+#lang racket/base
+(require (for-syntax racket/base syntax/parse syntax/stx
+                     racket/set racket/list
+                     "stx-utils.rkt")
+         (for-meta 2 racket/base syntax/parse))
+(provide (all-defined-out)
+         (for-syntax (all-defined-out)))
+
+;; for types, just need the identifier bound
+(define-syntax-rule (define-and-provide-builtin-type τ) 
+  (begin (define τ #f) (provide τ)))
+(define-syntax-rule (define-and-provide-builtin-types τ ...) 
+  (begin (define-and-provide-builtin-type τ) ...))
+
+;; general type-checking functions
+
+(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 y:id) (free-identifier=? τ1 τ2)]
+    [((tycon1 τ1 ...) (tycon2 τ2 ...)) 
+     (and (free-identifier=? #'tycon1 #'tycon2)
+          (= (length (syntax->list #'(τ1 ...))) (length (syntax->list #'(τ2 ...))))
+          (stx-andmap type=? #'(τ1 ...) #'(τ2 ...)))]
+    [_ #f]))
+
+;; return #t if (typeof e)=τ, else type error
+(define-for-syntax (assert-type e τ)
+  (or (type=? (typeof e) τ)
+      (error 'TYPE-ERROR "~a (~a:~a) has type ~a, but should have type ~a"
+             (syntax->datum e)
+             (syntax-line e) (syntax-column e)
+             (syntax->datum (typeof e))
+             (syntax->datum τ))))
+
+;; attaches type τ to e (as syntax property)
+(define-for-syntax (⊢ e τ) (syntax-property e 'type τ))
+
+;; retrieves type of τ (from syntax property)
+(define-for-syntax (typeof stx) (syntax-property stx 'type))
+
+;; type environment -----------------------------------------------------------
+(begin-for-syntax
+  (define base-type-env (hash))
+  ;; Γ : [Hashof var-symbol => type-stx]
+  ;; - can't use free-identifier=? for the hash table (or free-id-table)
+  ;;   because env must be set before expanding λ body (ie before going under λ)
+  ;;   so x's in the body won't be free-id=? to the one in the table
+  ;; use symbols instead of identifiers for now --- should be fine because
+  ;; I'm manually managing the environment
+  (define Γ (make-parameter base-type-env))
+  
+  (define (type-env-lookup x) (hash-ref (Γ) (syntax->datum x)))
+
+  ;; returns a new hash table extended with type associations x:τs
+  (define (type-env-extend x:τs)
+    (define xs (stx-map stx-car x:τs))
+    (define τs (stx-map stx-cadr x:τs))
+    (apply hash-set* (Γ) (append-map (λ (x τ) (list (syntax->datum x) τ)) xs τs)))
+
+  ;; must be macro because type env must be extended first, before expandinb body
+  (define-syntax (with-extended-type-env stx)
+    (syntax-parse stx
+      [(_ x-τs e)
+       #'(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/τ τ)))))
+
+;; expand/df ------------------------------------------------------------------
+;; depth-first expand
+(define-for-syntax (expand/df e [ctx #f])
+;  (printf "expanding: ~a\n" e)
+;  (printf "typeenv: ~a\n" (Γ))
+  (cond
+    ;; 1st case handles struct constructors that are not the same name as struct
+    ;; (should always be an identifier)
+    [(syntax-property e 'constructor-for) => (λ (Cons) 
+     (⊢ e (type-env-lookup Cons)))]
+    ;; 2nd case handles identifiers that are not struct constructors
+    [(identifier? e) (⊢ e (type-env-lookup e))] ; handle this here bc there's no #%var form
+    ;; local-expand must expand all the way down, ie have no stop-list, ie stop list can't be #f
+    ;; ow forms like lambda and app won't get properly assigned types
+    [else (local-expand e 'expression null ctx)]))
+(define-for-syntax (expand/df/module-ctx def)
+  (local-expand def 'module #f))
+(define-for-syntax (expand/df/mb-ctx def)
+  (local-expand def 'module-begin #f))
+