diff --git a/tapl/fsub.rkt b/tapl/fsub.rkt
index 2f7a4e0..f85c639 100644
--- a/tapl/fsub.rkt
+++ b/tapl/fsub.rkt
@@ -2,14 +2,14 @@
 (require "typecheck.rkt")
 (require (except-in "sysf.rkt" #%app #%datum + ∀ Λ inst type=?)
          (prefix-in sysf: (only-in "sysf.rkt" #%app ∀ Λ inst type=?))
-         (except-in "stlc+reco+sub.rkt" #%app + type=?)
-         (prefix-in stlc: (only-in "stlc+reco+sub.rkt" type=?)))
-(provide (rename-out [sysf:#%app #%app]))
+         (except-in "stlc+reco+sub.rkt" #%app + type=? sub?)
+         (prefix-in stlc: (only-in "stlc+reco+sub.rkt" type=? sub?)))
+(provide (rename-out [sysf:#%app #%app]) (for-syntax sub?))
 (provide (except-out (all-from-out "sysf.rkt")
                      sysf:#%app sysf:∀ sysf:Λ sysf:inst
                      (for-syntax sysf:type=?))
          (except-out (all-from-out "stlc+reco+sub.rkt")
-                     (for-syntax stlc:type=?)))
+                     (for-syntax stlc:type=? stlc:sub?)))
 (provide ∀ Λ inst)
  
 ;; System F<:
@@ -27,6 +27,9 @@
            (if sub (expose sub) t)]
           [else t]))
   (current-promote expose)
+  (define (sub? t1 t2)
+    (stlc:sub? (expose t1) (expose t2)))
+  (current-sub? sub?)
   ;; extend to handle new ∀
   (define (type=? τ1 τ2)
     (syntax-parse (list τ1 τ2)
diff --git a/tapl/notes.txt b/tapl/notes.txt
index f099a7e..faab94b 100644
--- a/tapl/notes.txt
+++ b/tapl/notes.txt
@@ -1,3 +1,13 @@
+2015-07-24
+When to canonicalize (ie, eval) types:
+- calling eval before matching is too late
+  - wont catch things like unbound types
+- syntax-class evaling is too eager
+  - sometimes get error when you shouldnt or wrong erro
+    - eg type (-> 1 2)
+- I think the right place is to have \vdash eval
+  - and rackunit testing forms
+
 2015-06-30
 when extending a typed language, use prefix-in for identifiers:
 - that are extended, eg #%datum in ext-stlc.rkt
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
index 74a3255..ee1219f 100644
--- a/tapl/stlc.rkt
+++ b/tapl/stlc.rkt
@@ -44,7 +44,33 @@
     (or (null? τs-lst)
         (andmap (λ (τ) ((current-type=?) (car τs-lst) τ)) (cdr τs-lst)))))
 
-(define-type-constructor →)
+;(define-type-constructor →)
+
+;;; when defining a type constructor tycon, can't define tycon as both
+;;; - an appliable constructor (ie a macro)
+;;; - and a syntax class
+;;; alternate solution: automatically define a tycon-match function
+;(define-syntax define-tycon
+;  (syntax-parser
+;    [(_ (τ arg ...))
+;     #:with pat (generate-temporary) ; syntax-class name
+;     #:with fn (generate-temporary) ; need a runtime id for expansion
+;     #'(begin
+;         (begin-for-syntax
+;           (define-syntax-class pat
+;             (pattern (arg ...))))
+;         (define-syntax τ
+;           (syntax-parser
+;             [x:id #'pat]
+;             [(_ x ( ... ...)) #'(fn x (... ...))])))]))
+;(define-tycon (→ τ ... τ_res))
+;
+;(define-for-syntax match-type-as
+;  (syntax-parser
+;    [( τ pat)
+;     #:with 
+
+(define-tycon (→ τ_in ... τ_out))
 
 (define-syntax (λ/tc stx)
   (syntax-parse stx 
@@ -55,37 +81,42 @@
 (define-syntax (app/tc stx)
   (syntax-parse stx
     [(_ e_fn e_arg ...)
-     #:with (e_fn- τ_fn) (infer+erase #'e_fn)
-     #:fail-unless (→? #'τ_fn)
-                   (format "Type error: Attempting to apply a non-function ~a with type ~a\n"
-                           (syntax->datum #'e_fn) (syntax->datum #'τ_fn))
-     #:with (τ ... τ_res) (→-args #'τ_fn)
+     #:with (e_fn- (τ_in ... τ_out)) (→-match+erase #'e_fn)
+     ;#:with (e_fn- τ_fn) (infer+erase #'e_fn)
+     ;#:with (e_fn- (τ_in ... τ_out)) (match+erase #'e_fn)
+;     #:fail-unless (→? #'τ_fn)
+;                   (format "Type error: Attempting to apply a non-function ~a with type ~a\n"
+;                           (syntax->datum #'e_fn) (syntax->datum #'τ_fn))
+     ;#:with (τ_in ... τ_out) (→-match #'τ_fn)
      #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
-     #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
+;     #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
+;                   (string-append
+;                    (format
+;                     "Wrong number of args given to function ~a:\ngiven: "
+;                     (syntax->datum #'e_fn))
+;                    (string-join
+;                     (map
+;                      (λ (e t) (format "~a : ~a" e t))
+;                      (syntax->datum #'(e_arg ...))
+;                      (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
+;                     ", ")
+;                    (format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
+     #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
                    (string-append
-                    (format
-                     "Wrong number of args given to function ~a:\ngiven: "
-                     (syntax->datum #'e_fn))
+                    (format "Arguments to function ~a have wrong type(s), "
+                            (syntax->datum #'e_fn))
+                    "or wrong number of arguments:\n"
+                    "given: "
                     (string-join
                      (map
                       (λ (e t) (format "~a : ~a" e t))
                       (syntax->datum #'(e_arg ...))
                       (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
                      ", ")
-                    (format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
-     #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
-                   (string-append
-                    (format
-                     "Arguments to function ~a have wrong type:\ngiven: "
-                     (syntax->datum #'e_fn))
+                    "\n"
+                    (format "expected ~a arguments with type(s): "
+                            (stx-length #'(τ_in ...)))
                     (string-join
-                     (map
-                      (λ (e t) (format "~a : ~a" e t))
-                      (syntax->datum #'(e_arg ...))
-                      (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
-                     ", ")
-                    "\nexpected arguments with type: "
-                    (string-join
-                     (map ~a (syntax->datum #`#,(stx-map get-orig #'(τ ...))))
+                     (map ~a (syntax->datum #`#,(stx-map get-orig #'(τ_in ...))))
                      ", "))
-     (⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))
+     (⊢ #'(#%app e_fn- e_arg- ...) #'τ_out)]))
diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt
index 4dae073..8f7b9a2 100644
--- a/tapl/tests/rackunit-typechecking.rkt
+++ b/tapl/tests/rackunit-typechecking.rkt
@@ -7,7 +7,7 @@
     [(_ e : τ ⇒ v) #'(check-type-and-result e : τ ⇒ v)]
     [(_ e : τ-expected:type)
      #:with τ (typeof (expand/df #'e))
-     #:fail-unless (typecheck? #'τ #'τ-expected.norm)
+     #:fail-unless (typecheck? #'τ ((current-type-eval) #'τ-expected))
      (format
       "Expression ~a [loc ~a:~a] has type ~a, expected ~a"
       (syntax->datum #'e) (syntax-line #'e) (syntax-column #'e)
@@ -18,7 +18,7 @@
   (syntax-parse stx #:datum-literals (:)
     [(_ e : not-τ:type)
      #:with τ (typeof (expand/df #'e))
-     #:fail-when (typecheck? #'τ #'not-τ.norm)
+     #:fail-when (typecheck? #'τ ((current-type-eval) #'not-τ.norm))
      (format
       "(~a:~a) Expression ~a should not have type ~a"
       (syntax-line stx) (syntax-column stx)
@@ -27,12 +27,24 @@
 
 (define-syntax (typecheck-fail stx)
   (syntax-parse stx #:datum-literals (:)
-    [(_ e)
+    [(_ e (~optional (~seq #:with-msg msg-pat:str) #:defaults ([msg-pat ""])))
      #:when (check-exn
-             exn:fail?
-             (λ () (expand/df #'e))
+             (λ (ex) (or (exn:fail? ex) (exn:test:check? ex)))
+             (λ ()
+               (with-handlers
+                   ; check err msg matches
+                   ([exn:fail?
+                     (λ (ex)
+                       (unless (regexp-match? (syntax-e #'msg-pat) (exn-message ex))
+                         (printf
+                          (string-append
+                           "ERROR: wrong err msg produced by expression ~v:\n"
+                           "expected msg matching pattern ~v, got:\n ~v")
+                          (syntax->datum #'e) (syntax-e #'msg-pat) (exn-message ex)))
+                       (raise ex))])
+                 (expand/df #'e)))
              (format
-              "Expected type check failure but expression ~a has valid type."
+              "Expected type check failure but expression ~a has valid type, OR wrong err msg received."
               (syntax->datum #'e)))
      #'(void)]))
 
diff --git a/tapl/tests/stlc+lit-tests.rkt b/tapl/tests/stlc+lit-tests.rkt
index b91f79d..fd86b3b 100644
--- a/tapl/tests/stlc+lit-tests.rkt
+++ b/tapl/tests/stlc+lit-tests.rkt
@@ -3,24 +3,56 @@
 
 (check-type 1 : Int)
 (check-not-type 1 : (→ Int Int))
-(typecheck-fail "one") ; unsupported literal
-(typecheck-fail #f) ; unsupported literal
+
+(typecheck-fail "one" #:with-msg "Unsupported literal")
+(typecheck-fail #f #:with-msg "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))
-(typecheck-fail (λ ([x : →]) x))
-(typecheck-fail (λ ([x : (→ →)]) x))
-(typecheck-fail (λ ([x : (→)]) x))
+
+(typecheck-fail
+ (λ ([x : →]) x)
+ #:with-msg "Improper usage of type constructor →: →, expected pattern")
+(typecheck-fail
+ (λ ([x : (→ →)]) x)
+ #:with-msg "Improper usage of type constructor →: →, expected pattern")
+(typecheck-fail
+ (λ ([x : (→)]) x)
+ #:with-msg "Improper usage of type constructor →: \\(→\\), expected pattern")
+
 (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 Bool)]) x)) ; 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
+
+(typecheck-fail ((λ ([x : Bool]) x) 1)
+                #:with-msg "Bool: unbound identifier")
+(typecheck-fail (λ ([x : (→ Bool Bool)]) x)
+                #:with-msg "Bool: unbound identifier")
+(typecheck-fail (λ ([x : Bool]) x)
+                #:with-msg "Bool: unbound identifier")
+(typecheck-fail (λ ([f : Int]) (f 1 2))
+                #:with-msg
+                "didn't match expected type pattern: \\(→ τ_in ... τ_out\\)")
+
 (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
+
+(typecheck-fail
+ (+ 1 (λ ([x : Int]) x))
+ #:with-msg
+ "Arguments to function \\+ have wrong type.+given: 1 : Int.+→.+expected 2 arguments with type.+Int\\, Int")
+(typecheck-fail
+ (λ ([x : (→ Int Int)]) (+ x x))
+  #:with-msg
+ "Arguments to function \\+ have wrong type.+given: x.+→.+expected 2 arguments with type.+Int\\, Int")
+(typecheck-fail
+ ((λ ([x : Int] [y : Int]) y) 1)
+ #:with-msg "Arguments to function.+have.+wrong number of arguments")
+
 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+
+(typecheck-fail (λ ([x : (→ 1 2)]) x)
+                #:with-msg "Improperly formatted type annotation")
+(typecheck-fail (λ ([x : 1]) x)
+                #:with-msg "Improperly formatted type annotation")
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index ebb44ac..e4aadbb 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -1,6 +1,7 @@
 #lang racket/base
 (require
-  (for-syntax racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt"))
+  (for-syntax racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt")
+  (for-meta 2 racket/base syntax/parse))
 (provide 
  (for-syntax (all-defined-out)) (all-defined-out)
  (for-syntax
@@ -40,6 +41,70 @@
   (define (get-orig τ)
     (car (reverse (or (syntax-property τ 'orig) (list τ))))))
 
+(begin-for-syntax
+  (define-syntax (match-type stx)
+    (syntax-parse stx
+      [(_ ty tycon cls)
+       #'(syntax-parse ty ;((current-type-eval) ty)
+         [((~literal #%plain-app) t . args)
+          #:declare args cls
+          #:fail-unless (typecheck? #'t #'tycon)
+          (format "Type error: expected ~a type, got ~a"
+                  (syntax->datum #'τ) (syntax->datum ty))
+          #'args]
+         [_ #f
+          #;(type-error #:src ty
+                      #:msg "~a didn't match expected type pattern: ~a"
+                      ty pat)])])))
+
+(define-syntax define-tycon
+  (syntax-parser
+    [(_ (τ:id . pat))
+     #:with τ-match (format-id #'τ "~a-match" #'τ)
+     #:with τ? (format-id #'τ "~a?" #'τ)
+     #:with τ-match+erase (format-id #'τ "~a-match+erase" #'τ)
+     #:with pat-class (generate-temporary #'τ) ; syntax-class name
+     #:with tycon (generate-temporary #'τ) ; need a runtime id for expansion
+     #'(begin
+         (provide τ)
+         (begin-for-syntax
+           (define-syntax-class pat-class
+             (pattern pat))
+           (define (τ-match ty)
+             (or (match-type ty tycon pat-class)
+                 (type-error #:src ty
+                      #:msg "~a didn't match expected type pattern: ~a"
+                      ty (quote-syntax (τ . pat))))
+             #;(syntax-parse ty
+               [((~literal #%plain-app) t . args)
+                #:declare args pat-class
+                #:fail-unless (typecheck? #'t #'tycon)
+                (format "Type error: expected ~a type, got ~a"
+                        (syntax->datum #'τ) (syntax->datum ty))
+                #'args]
+               [_ (type-error #:src ty
+                              #:msg "~a didn't match expected type pattern: ~a"
+                              ty (quote-syntax (τ . pat)))]))
+           ; predicate version of τ-match
+           (define (τ? ty) (match-type ty tycon pat-class))
+           ;; expression version of τ-match
+           (define (τ-match+erase e)
+             (syntax-parse (infer+erase e)
+               [(e- τ)
+                #:with τ_matched (τ-match #'τ)
+                #'(e- τ_matched)])))
+         (define tycon (λ _ (raise (exn:fail:type:runtime
+                                    (format "~a: Cannot use type at run time" 'τ)
+                                    (current-continuation-marks)))))
+         (define-syntax (τ stx)
+           (syntax-parse stx
+             [(_ . pat) #'(tycon . pat)]
+             [_
+              (type-error #:src stx
+                          #:msg "Improper usage of type constructor ~a: ~a, expected pattern ~a"
+                          #'τ stx (quote-syntax (τ . pat)))]))
+         )]))
+
 ;; TODO: refine this to enable specifying arity information
 ;; type constructors currently must have 1+ arguments
 (define-syntax (define-type-constructor stx)
@@ -49,6 +114,7 @@
      #:with τ-ref (format-id #'τ "~a-ref" #'τ)
      #:with τ-num-args (format-id #'τ "~a-num-args" #'τ)
      #:with τ-args (format-id #'τ "~a-args" #'τ)
+     #:with τ-match (format-id #'τ "~a-match" #'τ)
      #:with tmp (generate-temporary #'τ)
      #`(begin
          ;; TODO: define syntax class instead of these separate tycon fns
@@ -102,17 +168,32 @@
   (define-syntax-class type
     ;; stx = surface syntax, as written
     ;; norm = canonical form for the type
-    (pattern stx:expr
-     #:with norm ((current-type-eval) #'stx)
-     #:with τ #'norm)) ; backwards compat
+    (pattern tycon:id
+     #:when (procedure? (syntax-local-value #'tycon (λ _ #f)))
+     #:with norm #f ; should this be #f?
+     #:with τ #f)
+    (pattern T:id
+     #:with norm #'T ;((current-type-eval) #'T)
+     #:with τ #'norm) ; backwards compat
+    (pattern (t:type ...)
+     #:with norm #'(t ...) ;((current-type-eval) #'(t ...))
+     #:with τ #'norm) ; backwards compat
+    (pattern any
+     #:with norm #f #:with τ #f
+     #:fail-when #t
+     (format "~a is not a valid type" (syntax->datum #'any))))
+
   (define-syntax-class typed-binding #:datum-literals (:)
     (pattern [x:id : stx:type] #:with τ #'stx.τ)
     (pattern (~and any (~not [x:id : τ:type]))
      #:with x #f
      #:with τ #f
      #:fail-when #t
-     (format "Improperly formatted type annotation: ~a; should have shape [x : τ]"
-             (syntax->datum #'any))))
+     (format
+      (string-append
+       "Improperly formatted type annotation: ~a; should have shape [x : τ], "
+       "where τ is a valid type.")
+      (syntax->datum #'any))))
   (define (brace? stx)
     (define paren-shape/#f (syntax-property stx 'paren-shape))
     (and paren-shape/#f (char=? paren-shape/#f #\{)))
@@ -129,20 +210,12 @@
   ;; must eval here, to catch unbound types
   (define (⊢ e τ #:tag [tag 'type])
     (syntax-property e tag (syntax-local-introduce ((current-type-eval) τ))))
+    ;(syntax-property e tag τ))
   
   ;; typeof : Syntax -> Type or #f
   ;; Retrieves type of given stx, or #f if input has not been assigned a type.
   (define (typeof stx #:tag [tag 'type]) (syntax-property stx tag))
   
-  ;; infers type and erases types in a single expression,
-  ;; in the context of the given bindings and their types
-  (define (infer/type-ctxt+erase x+τs e)
-    (syntax-parse (infer (list e) #:ctx x+τs)
-      [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
-  ;; infers type and erases types in multiple expressions,
-  ;; in the context of (one set of) given bindings and their tpyes
-  (define (infers/type-ctxt+erase ctxt es)
-    (stx-cdr (infer es #:ctx ctxt))) ; drop (empty) tyvars from result
   ;; infers the type and erases types in an expression
   (define (infer+erase e)
     (define e+ (expand/df e))
@@ -150,10 +223,6 @@
   ;; infers the types and erases types in multiple expressions
   (define (infers+erase es)
     (stx-map infer+erase es))
-  ;; infers and erases types in an expression, in the context of given type vars
-  (define (infer/tvs+erase e tvs)
-    (syntax-parse (infer (list e) #:tvs tvs)
-      [(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
 
   ;; This is the main "infer" function. All others are defined in terms of this.
   ;; It should be named infer+erase but leaving it for now for backward compat.
@@ -167,14 +236,14 @@
        #:with (e ...) es
        #:with
        ; old expander pattern
-       ((~literal #%plain-lambda) tvs+
+       #;((~literal #%plain-lambda) tvs+
         ((~literal #%expression)
          ((~literal #%plain-lambda) xs+
           ((~literal letrec-syntaxes+values) stxs1 ()
             ((~literal letrec-syntaxes+values) stxs2 ()
               ((~literal #%expression) e+) ...)))))
        ; new expander pattern
-       #;((~literal #%plain-lambda) tvs+
+       ((~literal #%plain-lambda) tvs+
         ((~literal #%expression)
          ((~literal #%plain-lambda) xs+
           ((~literal let-values) ()
@@ -189,11 +258,26 @@
              (stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
       [([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvs tvs)]))
 
+  ;; fns derived from infer ---------------------------------------------------
+  ;; some are syntactic shortcuts, some are for backwards compat
+  
+  ;; infers type and erases types in a single expression,
+  ;; in the context of the given bindings and their types
+  (define (infer/type-ctxt+erase x+τs e)
+    (syntax-parse (infer (list e) #:ctx x+τs)
+      [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
+  ;; infers type and erases types in multiple expressions,
+  ;; in the context of (one set of) given bindings and their tpyes
+  (define (infers/type-ctxt+erase ctxt es)
+    (stx-cdr (infer es #:ctx ctxt))) ; drop (empty) tyvars from result
+  ;; infers and erases types in an expression, in the context of given type vars
+  (define (infer/tvs+erase e tvs)
+    (syntax-parse (infer (list e) #:tvs tvs)
+      [(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
+
   (define current-typecheck-relation (make-parameter #f))
   (define (typecheck? t1 t2)
-    ((current-typecheck-relation)
-     ((current-promote) t1)
-     ((current-promote) t2)))
+    ((current-typecheck-relation) t1 t2))
   (define (typechecks? τs1 τs2)
     (and (= (stx-length τs1) (stx-length τs2))
          (stx-andmap typecheck? τs1 τs2)))