diff --git a/macrotypes/examples/ext-stlc.rkt b/macrotypes/examples/ext-stlc.rkt
index 2d9dce4..5b8f44e 100644
--- a/macrotypes/examples/ext-stlc.rkt
+++ b/macrotypes/examples/ext-stlc.rkt
@@ -1,6 +1,6 @@
 #lang s-exp macrotypes/typecheck
 (extends "stlc+lit.rkt" #:except #%datum)
-(provide (for-syntax current-join))
+(provide ⊔ (for-syntax current-join))
  
 ;; Simply-Typed Lambda Calculus, plus extensions (TAPL ch11)
 ;; Types:
@@ -38,16 +38,19 @@
 
 (define-typed-syntax and
   [(and e1 e2)
-   #:with e1- (⇑ e1 as Bool)
-   #:with e2- (⇑ e2 as Bool)
+   #:with Bool* ((current-type-eval) #'Bool)
+   #:with [e1- τ_e1] (infer+erase #'e1)
+   #:with [e2- τ_e2] (infer+erase #'e2)
+   #:fail-unless (typecheck? #'τ_e1 #'Bool*) (typecheck-fail-msg/1 #'Bool* #'τ_e1 #'e1)
+   #:fail-unless (typecheck? #'τ_e2 #'Bool*) (typecheck-fail-msg/1 #'Bool* #'τ_e2 #'e2)
    (⊢ (and- e1- e2-) : Bool)])
   
 (define-typed-syntax or
   [(or e ...)
-   #:with (e- ...) (⇑s (e ...) as Bool)
-;   #:with e1- (⇑ e1 as Bool)
-;   #:with e2- (⇑ e2 as Bool)
-;   (⊢ (or- e1- e2-) : Bool)])
+   #:with ([_ Bool*] ...) #`([e #,((current-type-eval) #'Bool)] ...)
+   #:with ([e- τ_e] ...) (infers+erase #'(e ...))
+   #:fail-unless (typechecks? #'(τ_e ...) #'(Bool* ...))
+   (typecheck-fail-msg/multi #'(Bool* ...) #'(τ_e ...) #'(e ...))
    (⊢ (or- e- ...) : Bool)])
 
 (begin-for-syntax 
@@ -60,17 +63,22 @@
             #:msg  "branches have incompatible types: ~a and ~a" x y))
         x))))
 
+(define-syntax ⊔
+  (syntax-parser
+    [(⊔ τ1 τ2 ...)
+     (for/fold ([τ ((current-type-eval) #'τ1)])
+               ([τ2 (in-list (stx-map (current-type-eval) #'[τ2 ...]))])
+       ((current-join) τ τ2))]))
+
 (define-typed-syntax if
   [(if e_tst e1 e2)
    #:with τ-expected (get-expected-type stx)
-;   #:with e_tst- (⇑ e_tst as Bool)
    #:with [e_tst- _] (infer+erase #'e_tst)
    #:with e1_ann #'(add-expected e1 τ-expected)
    #:with e2_ann #'(add-expected e2 τ-expected)
    #:with (e1- τ1) (infer+erase #'e1_ann)
    #:with (e2- τ2) (infer+erase #'e2_ann)
-   #:with τ-out ((current-join) #'τ1 #'τ2)
-   (⊢ (if- e_tst- e1- e2-) : τ-out)])
+   (⊢ (if- e_tst- e1- e2-) : (⊔ τ1 τ2))])
 
 (define-base-type Unit)
 (define-primop void : (→ Unit))
@@ -86,8 +94,7 @@
   [(ann e : ascribed-τ:type)
    #:with (e- τ) (infer+erase #'(add-expected e ascribed-τ.norm))
    #:fail-unless (typecheck? #'τ #'ascribed-τ.norm)
-                 (format "~a does not have type ~a\n"
-                         (syntax->datum #'e) (syntax->datum #'ascribed-τ))
+   (typecheck-fail-msg/1 #'ascribed-τ.norm #'τ #'e)
    (⊢ e- : ascribed-τ)])
 
 (define-typed-syntax let
@@ -96,9 +103,8 @@
    #:with ((e- τ) ...) (infers+erase #'(e ...))
    #:with ((x- ...) e_body- τ_body) (infer/ctx+erase #'([x τ] ...) #'(add-expected e_body τ-expected))
    #:fail-unless (or (not (syntax-e #'τ-expected)) ; no expected type
-                      (typecheck? #'τ_body ((current-type-eval) #'τ-expected)))
-     (format "let body has type ~a, which does not match expected type ~a"
-             (type->str #'τ_body) (type->str #'τ-expected))
+                     (typecheck? #'τ_body ((current-type-eval) #'τ-expected)))
+   (typecheck-fail-msg/1 #'τ-expected #'τ_body #'e_body)
    (⊢ (let- ([x- e-] ...) e_body-) : τ_body)])
 
 ; dont need to manually transfer expected type
@@ -118,17 +124,7 @@
    #:with ((x- ...) (e- ... e_body-) (τ ... τ_body))
           (infers/ctx+erase #'(b ...) #'((add-expected e b.type) ... e_body))
    #:fail-unless (typechecks? #'(b.type ...) #'(τ ...))
-                 (type-error #:src stx
-                  #:msg (string-append
-                  "letrec: type check fail, args have wrong type:\n"
-                  (string-join
-                   (stx-map
-                    (λ (e τ τ-expect)
-                      (format
-                       "~a has type ~a, expected ~a"
-                       (syntax->datum e) (type->str τ) (type->str τ-expect)))
-                    #'(e ...) #'(τ ...) #'(b.type ...))
-                   "\n")))
-  (⊢ (letrec- ([x- e-] ...) e_body-) : τ_body)])
+   (typecheck-fail-msg/multi #'(b.type ...) #'(τ ...) #'(e ...))
+   (⊢ (letrec- ([x- e-] ...) e_body-) : τ_body)])
 
 
diff --git a/macrotypes/examples/mlish.rkt b/macrotypes/examples/mlish.rkt
index 8c5dbcb..eca45bc 100644
--- a/macrotypes/examples/mlish.rkt
+++ b/macrotypes/examples/mlish.rkt
@@ -116,9 +116,14 @@
 
   (define (raise-app-poly-infer-error stx expected-tys given-tys e_fn)
     (type-error #:src stx
-     #:msg (mk-app-err-msg stx #:expected expected-tys #:given given-tys
-            #:note (format "Could not infer instantiation of polymorphic function ~a."
-                           (syntax->datum (get-orig e_fn))))))
+     #:msg (format
+            (string-append
+             "Could not infer instantiation of polymorphic function ~s.\n"
+             "  expected: ~a\n"
+             "  given:    ~a")
+            (syntax->datum (get-orig e_fn))
+            (string-join (stx-map type->str expected-tys) ", ")
+            (string-join (stx-map type->str given-tys) ", "))))
 
   ;; covariant-Xs? : Type -> Bool
   ;; Takes a possibly polymorphic type, and returns true if all of the
@@ -459,14 +464,13 @@
               #:when (stx-null? #'(τ ...))
               #:with τ-expected (syntax-property #'C 'expected-type)
               #:fail-unless (syntax-e #'τ-expected)
-                            (raise
-                              (exn:fail:type:infer
-                                (string-append
-                                  (format "TYPE-ERROR: ~a (~a:~a): "
-                                          (syntax-source stx) (syntax-line stx) (syntax-column stx))
-                                  (format "cannot infer type of ~a; add annotations" 
-                                          (syntax->datum #'C)))
-                                (current-continuation-marks)))
+              (raise
+               (exn:fail:type:infer
+                (format "~a (~a:~a): ~a: ~a"
+                         (syntax-source stx) (syntax-line stx) (syntax-column stx)
+                         (syntax-e #'C)
+                         (no-expected-type-fail-msg))
+                (current-continuation-marks)))
               #:with (NameExpander τ-expected-arg (... ...)) ((current-type-eval) #'τ-expected)
               #'(C {τ-expected-arg (... ...)})]
              [_:id (⊢ StructName (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...))))] ; HO fn
@@ -483,9 +487,7 @@
                         (infer+erase (set-stx-prop/preserved e 'expected-type τ_e)))
                       #'(e_arg ...) #'(τ_in.norm (... ...)))
               #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in.norm (... ...)))
-                           (mk-app-err-msg (syntax/loc stx (#%app C e_arg ...))
-                            #:expected #'(τ_in.norm (... ...)) #:given #'(τ_arg ...)
-                            #:name (format "constructor ~a" 'Cons))
+              (typecheck-fail-msg/multi #'(τ_in.norm (... ...)) #'(τ_arg ...) #'(e_arg ...))
               (⊢ (StructName e_arg- ...) : (Name τ_X (... ...)))]
              [(C . args) ; no type annotations, must infer instantiation
               #:with StructName/ty 
@@ -834,19 +836,18 @@
 
 ; all λs have type (?∀ (X ...) (→ τ_in ... τ_out))
 (define-typed-syntax λ
-  [(λ (x:id ...+) body)
+  [(λ (x:id ...) body)
    #:with (~?∀ Xs expected) (get-expected-type stx)
-   #:do [(unless (→? #'expected)
-           (type-error #:src stx #:msg "λ parameters must have type annotations"))]
+   #:fail-unless (→? #'expected)
+   (no-expected-type-fail-msg)
    #:with (~ext-stlc:→ arg-ty ... body-ty) #'expected
-   #:do [(unless (stx-length=? #'[x ...] #'[arg-ty ...])
-           (type-error #:src stx #:msg
-                       (format "expected a function of ~a arguments, got one with ~a arguments"
-                               (stx-length #'[arg-ty ...] #'[x ...]))))]
-   #`(?Λ Xs (ext-stlc:λ ([x : arg-ty] ...) #,(add-expected-ty #'body #'body-ty)))]
-  [(λ args body)
+   #:fail-unless (stx-length=? #'[x ...] #'[arg-ty ...])
+   (format "expected a function of ~a arguments, got one with ~a arguments"
+           (stx-length #'[arg-ty ...]) (stx-length #'[x ...]))
+   #`(?Λ Xs (ext-stlc:λ ([x : arg-ty] ...) (add-expected body body-ty)))]
+  [(λ (~and args ([_ (~datum :) ty] ...)) body)
    #:with (~?∀ () (~ext-stlc:→ arg-ty ... body-ty)) (get-expected-type stx)
-   #`(?Λ () (ext-stlc:λ args #,(add-expected-ty #'body #'body-ty)))]
+   #`(?Λ () (ext-stlc:λ args (add-expected body body-ty)))]
   [(λ (~and x+tys ([_ (~datum :) ty] ...)) . body)
    #:with Xs (compute-tyvars #'(ty ...))
    ;; TODO is there a way to have λs that refer to ids defined after them?
@@ -856,64 +857,32 @@
 ;; #%app --------------------------------------------------
 (define-typed-syntax mlish:#%app #:export-as #%app
   [(_ e_fn . e_args)
-   ;; ) compute fn type (ie ∀ and →) 
+   ;; compute fn type (ie ∀ and →) 
    #:with [e_fn- (~?∀ Xs (~ext-stlc:→ . tyX_args))] (infer+erase #'e_fn)
-   (cond 
-    [(stx-null? #'Xs)
-     (syntax-parse #'(e_args tyX_args)
-       [((e_arg ...) (τ_inX ... _))
-        #:fail-unless (stx-length=? #'(e_arg ...) #'(τ_inX ...))
-                      (mk-app-err-msg stx #:expected #'(τ_inX ...) 
-                                      #:note "Wrong number of arguments.")
-        #:with e_fn/ty (⊢ e_fn- : (ext-stlc:→ . tyX_args))
-        #'(ext-stlc:#%app e_fn/ty (add-expected e_arg τ_inX) ...)])]
-    [else
-     ;; ) solve for type variables Xs
-     (define/with-syntax ((e_arg- ...) Xs* cs) (solve #'Xs #'tyX_args stx))
-     ;; ) instantiate polymorphic function type
-     (syntax-parse (inst-types/cs #'Xs* #'cs #'tyX_args)
-      [(τ_in ... τ_out) ; concrete types
-       #:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)
-       ;; ) arity check
-       #:fail-unless (stx-length=? #'(τ_in ...) #'e_args)
-                     (mk-app-err-msg stx #:expected #'(τ_in ...)
-                      #:note "Wrong number of arguments.")
-       ;; ) compute argument types
-       #:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))
-       ;; ) typecheck args
-       #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
-                     (mk-app-err-msg stx 
-                      #:given #'(τ_arg ...)
-                      #:expected 
-                      (stx-map 
-                        (lambda (tyin) 
-                          (define old-orig (get-orig tyin))
-                          (define new-orig
-                            (and old-orig
-                                 (substs 
-                                   (stx-map get-orig (lookup-Xs/keep-unsolved #'Xs* #'cs))
-                                   #'Xs*
-                                   old-orig
-                                   (lambda (x y) 
-                                    (equal? (syntax->datum x) (syntax->datum y))))))
-                          (set-stx-prop/preserved tyin 'orig (list new-orig)))
-                       #'(τ_in ...)))
-       #:with τ_out* (if (stx-null? #'(unsolved-X ...))
-                         #'τ_out
-                         (syntax-parse #'τ_out
-                           [(~?∀ (Y ...) τ_out)
-                            (unless (→? #'τ_out)
-                              (raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))
-                            (for ([X (in-list (syntax->list #'(unsolved-X ...)))])
-                              (unless (covariant-X? X #'τ_out)
-                                (raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)))
-                            #'(∀ (unsolved-X ... Y ...) τ_out)]))
-       (⊢ (#%app- e_fn- e_arg- ...) : τ_out*)])])]
-  [(_ e_fn . e_args) ; err case; e_fn is not a function
-   #:with [e_fn- τ_fn] (infer+erase #'e_fn)
-   (type-error #:src stx 
-               #:msg (format "Expected expression ~a to have → type, got: ~a"
-                             (syntax->datum #'e_fn) (type->str #'τ_fn)))])
+   ;; solve for type variables Xs
+   #:with [(e_arg- ...) Xs* cs] (solve #'Xs #'tyX_args stx)
+   ;; instantiate polymorphic function type
+   #:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args)
+   #:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)
+   ;; arity check
+   #:fail-unless (stx-length=? #'(τ_in ...) #'e_args)
+   (num-args-fail-msg #'e_fn #'(τ_in ...) #'e_args)
+   ;; compute argument types
+   #:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))
+   ;; typecheck args
+   #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
+   (typecheck-fail-msg/multi #'(τ_in ...) #'(τ_arg ...) #'e_args)
+   #:with τ_out* (if (stx-null? #'(unsolved-X ...))
+                     #'τ_out
+                     (syntax-parse #'τ_out
+                       [(~?∀ (Y ...) τ_out)
+                        (unless (→? #'τ_out)
+                          (raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))
+                        (for ([X (in-list (syntax->list #'(unsolved-X ...)))])
+                          (unless (covariant-X? X #'τ_out)
+                            (raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)))
+                        #'(∀ (unsolved-X ... Y ...) τ_out)]))
+   (⊢ (#%app- e_fn- e_arg- ...) : τ_out*)])
 
 
 ;; cond and other conditionals
@@ -1107,10 +1076,7 @@
    #:with [(acc- x- ...) body- ty_body] 
           (infer/ctx+erase #'([acc : ty_init][x : ty] ...) #'body)
    #:fail-unless (typecheck? #'ty_body #'ty_init)
-                 (type-error #:src stx
-                  #:msg 
-                  "for/fold: Type of body and initial accumulator must be the same, given ~a and ~a"
-                  #'ty_init #'ty_body)
+   (typecheck-fail-msg/1 #'ty_init #'ty_body #'body)
    (⊢ (for/fold- ([acc- init-]) ([x- e-] ...) body-) : ty_body)])
 
 (define-typed-syntax for/hash
diff --git a/macrotypes/examples/stlc+box.rkt b/macrotypes/examples/stlc+box.rkt
index 79f155c..06a347d 100644
--- a/macrotypes/examples/stlc+box.rkt
+++ b/macrotypes/examples/stlc+box.rkt
@@ -13,15 +13,16 @@
 
 (define-typed-syntax ref
   [(ref e)
-   #:with (e- τ) (infer+erase #'e)
+   #:with [e- τ] (infer+erase #'e)
    (⊢ (box- e-) : (Ref τ))])
 (define-typed-syntax deref
   [(deref e)
-   #:with (e- (τ)) (⇑ e as Ref)
+   #:with [e- (~Ref τ)] (infer+erase #'e)
    (⊢ (unbox- e-) : τ)])
 (define-typed-syntax := #:literals (:=)
   [(:= e_ref e)
-   #:with (e_ref- (τ1)) (⇑ e_ref as Ref)
-   #:with (e- τ2) (infer+erase #'e)
-   #:when (typecheck? #'τ1 #'τ2)
+   #:with [e_ref- (~Ref τ1)] (infer+erase #'e_ref)
+   #:with [e- τ2] (infer+erase #'e)
+   #:fail-unless (typecheck? #'τ1 #'τ2)
+   (typecheck-fail-msg/1 #'τ1 #'τ2 #'e)
    (⊢ (set-box!- e_ref- e-) : Unit)])
diff --git a/macrotypes/examples/stlc+cons.rkt b/macrotypes/examples/stlc+cons.rkt
index 214d717..9f6b030 100644
--- a/macrotypes/examples/stlc+cons.rkt
+++ b/macrotypes/examples/stlc+cons.rkt
@@ -17,48 +17,43 @@
    (⊢ null- : (List τi.norm))]
   ; minimal type inference
   [nil:id #:with expected-τ (get-expected-type #'nil)
-          #:when (syntax-e #'expected-τ) ; 'expected-type property exists (ie, not false)
-          #:with ty_lst (local-expand #'expected-τ 'expression null) ; canonicalize
-          #:fail-unless (List? #'ty_lst)
+          #:fail-unless (syntax-e #'expected-τ) ; 'expected-type property exists (ie, not false)
+          (raise (exn:fail:type:infer
+                  (format "~a (~a:~a): nil: ~a"
+                          (syntax-source stx) (syntax-line stx) (syntax-column stx)
+                          (no-expected-type-fail-msg))
+                  (current-continuation-marks)))
+          #:fail-unless (List? #'expected-τ)
           (raise (exn:fail:type:infer
                   (format "~a (~a:~a): Inferred ~a type for nil, which is not a List."
                           (syntax-source stx) (syntax-line stx) (syntax-column stx)
                           (type->str #'ty_lst))
                   (current-continuation-marks)))
-          #:with (~List τ) #'ty_lst
-          (⊢ null- : (List τ))]
-  [_:id #:fail-when #t
-        (raise (exn:fail:type:infer
-                (format "~a (~a:~a): nil requires type annotation"
-                        (syntax-source stx) (syntax-line stx) (syntax-column stx))
-                (current-continuation-marks)))
-        #'(void-)])
+          (⊢ null- : expected-τ)])
 (define-typed-syntax cons
   [(cons e1 e2)
-   #:with [e1- τ1] (infer+erase #'e1)
-;   #:with e2ann (add-expected-type #'e2 #'(List τ1))
-   #:with (e2- (τ2)) (⇑ (add-expected e2 (List τ1)) as List)
-   #:fail-unless (typecheck? #'τ1 #'τ2)
-                 (format "trying to cons expression ~a with type ~a to list ~a with type ~a\n"
-                         (syntax->datum #'e1) (type->str #'τ1)
-                         (syntax->datum #'e2) (type->str #'(List τ2)))
+   #:with [e1- τ_e1] (infer+erase #'e1)
+   #:with τ_list ((current-type-eval) #'(List τ_e1))
+   #:with [e2- τ_e2] (infer+erase (add-expected-ty #'e2 #'τ_list))
+   #:fail-unless (typecheck? #'τ_e2 #'τ_list)
+   (typecheck-fail-msg/1 #'τ_list #'τ_e2 #'e2)
    ;; propagate up inferred types of variables
    #:with env (stx-flatten (filter (λ (x) x) (stx-map get-env #'(e1- e2-))))
    #:with result-cons (add-env #'(cons- e1- e2-) #'env)
-   (⊢ result-cons : (List τ1))])
+   (⊢ result-cons : τ_list)])
 (define-typed-syntax isnil
   [(isnil e)
-   #:with (e- _) (⇑ e as List)
+   #:with [e- (~List _)] (infer+erase #'e)
    (⊢ (null?- e-) : Bool)])
 (define-typed-syntax head
   [(head e)
-   #:with (e- (τ)) (⇑ e as List)
+   #:with [e- (~List τ)] (infer+erase #'e)
    (⊢ (car- e-) : τ)])
 (define-typed-syntax tail
   [(tail e)
-   #:with (e- τ-lst) (infer+erase #'e)
-   #:when (List? #'τ-lst)
-   (⊢ (cdr- e-) : τ-lst)])
+   #:with [e- τ_lst] (infer+erase #'e)
+   #:when (List? #'τ_lst)
+   (⊢ (cdr- e-) : τ_lst)])
 (define-typed-syntax list
   [(list) #'nil]
   [(_ x . rst) ; has expected type
diff --git a/macrotypes/examples/stlc+effect.rkt b/macrotypes/examples/stlc+effect.rkt
index 68ec8e8..4d78077 100644
--- a/macrotypes/examples/stlc+effect.rkt
+++ b/macrotypes/examples/stlc+effect.rkt
@@ -53,14 +53,10 @@
    #:with tyds (get-deref-effects #'ty_fn)
    #:with (~→ τ_in ... τ_out) #'ty_fn
    #:with ([e_arg- τ_arg ns as ds] ...) (infers+erase/eff #'(e ...))
-;   #:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn as →)
    #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ_in ...))
-                 (mk-app-err-msg stx #:expected #'(τ_in ...) 
-                                     #:given #'(τ_arg ...)
-                  #:note "Wrong number of arguments.")
+   (num-args-fail-msg #'efn #'(τ_in ...) #'(e ...))
    #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
-                 (mk-app-err-msg stx #:expected #'(τ_in ...) 
-                                     #:given #'(τ_arg ...))
+   (typecheck-fail-msg/multi #'(τ_in ...) #'(τ_arg ...) #'(e ...))
   (assign-type/eff #'(#%app- e_fn- e_arg- ...) #'τ_out
                    (stx-flatten #'(fns tyns . (ns ...)))
                    (stx-flatten #'(fas tyas . (as ...)))
@@ -108,20 +104,20 @@
 
 (define-typed-syntax ref
   [(ref e)
-   #:with (e- τ ns as ds) (infer+erase/eff #'e)
+   #:with [e- τ ns as ds] (infer+erase/eff #'e)
    (assign-type/eff #'(box- e-) #'(Ref τ)
                     (cons (syntax-position stx) #'ns) #'as #'ds)])
 (define-typed-syntax deref
   [(deref e)
-   #:with (e- (~Ref ty) ns as ds) (infer+erase/eff #'e)
+   #:with [e- (~Ref ty) ns as ds] (infer+erase/eff #'e)
    (assign-type/eff #'(unbox- e-) #'ty
                     #'ns #'as (cons (syntax-position stx) #'ds))])
 (define-typed-syntax := #:literals (:=)
   [(:= e_ref e)
-   ;#:with (e_ref- (τ1)) (⇑ e_ref as Ref)
    #:with [e_ref- (~Ref ty1) ns1 as1 ds1] (infer+erase/eff #'e_ref)
    #:with [e- ty2 ns2 as2 ds2] (infer+erase/eff #'e)
-   #:when (typecheck? #'ty1 #'ty2)
+   #:fail-unless (typecheck? #'ty1 #'ty2)
+   (typecheck-fail-msg/1 #'ty1 #'ty2 #'e)
    (assign-type/eff #'(set-box!- e_ref- e-) #'Unit
                     (stx-append #'ns1 #'ns2)
                     (cons (syntax-position stx) (stx-append #'as1 #'as2))
diff --git a/macrotypes/examples/stlc+reco+var.rkt b/macrotypes/examples/stlc+reco+var.rkt
index de9895a..d69ace5 100644
--- a/macrotypes/examples/stlc+reco+var.rkt
+++ b/macrotypes/examples/stlc+reco+var.rkt
@@ -61,6 +61,20 @@
                                #:src #'any
                                #:msg "Expected × type, got: ~a" #'any))))]))))
 
+(begin-for-syntax
+  (define (stx-assoc-ref stx-lst lookup-k #:else [fail (λ () #f)])
+    (define match_res (stx-assoc lookup-k stx-lst))
+    (cond [match_res
+           (stx-cadr match_res)]
+          [else
+           (fail)]))
+  (define (×-ref ×-type l)
+    (syntax-parse ×-type
+      [(~× [l_τ : τ] ...)
+       (define res
+         (stx-assoc-ref #'([l_τ τ] ...) l #:else (λ () (error 'X-ref "bad!"))))
+       (add-orig res (get-orig res))])))
+
 ;; records
 (define-typed-syntax tup #:datum-literals (=)
   [(tup [l:id = e] ...)
@@ -68,9 +82,12 @@
    (⊢ (list- (list- 'l e-) ...) : (× [l : τ] ...))])
 (define-typed-syntax proj #:literals (quote)
   [(proj e_rec l:id)
-   #:with (e_rec- ([l_τ τ] ...)) (⇑ e_rec as ×)
-   #:with (_ τ_match) (stx-assoc #'l #'([l_τ τ] ...))
-   (⊢ (cadr- (assoc- 'l e_rec-)) : τ_match)])
+   #:with [e_rec- τ_e] (infer+erase #'e_rec)
+   #:fail-unless (×? #'τ_e)
+   (format "Expected expression ~s to have × type, got: ~a"
+           (syntax->datum #'e_rec) (type->str #'τ_e))
+   #:with τ_l (×-ref #'τ_e #'l)
+   (⊢ (cadr- (assoc- 'l e_rec-)) : τ_l)])
 
 (define-type-constructor ∨/internal #:arity >= 0)
 
@@ -107,26 +124,36 @@
                                     #:msg "Expected ∨ type, got: ~a" #'any))))
                ~!)])))) ; dont backtrack here
 
+(begin-for-syntax
+  (define (∨-ref ∨-type l #:else [fail (λ () #f)])
+    (syntax-parse ∨-type
+      [(~∨ [l_τ : τ] ...)
+       (define res
+         (stx-assoc-ref #'([l_τ τ] ...) l #:else fail))
+       (add-orig res (get-orig res))])))
+
 (define-typed-syntax var #:datum-literals (as =)
   [(var l:id = e as τ:type)
-   #:with (~∨* [l_τ : τ_l] ...) #'τ.norm
-   #:with match_res (stx-assoc #'l #'((l_τ τ_l) ...))
-   #:fail-unless (syntax-e #'match_res)
-                 (format "~a field does not exist" (syntax->datum #'l))
-   #:with (_ τ_match) #'match_res
-   #:with (e- τ_e) (infer+erase #'e)
-   #:when (typecheck? #'τ_e #'τ_match)
-   (⊢ (list- 'l e) : τ)])
+   #:fail-unless (∨? #'τ.norm)
+   (format "Expected the expected type to be a ∨ type, got: ~a" (type->str #'τ.norm))
+   #:with τ_match
+   (∨-ref #'τ.norm #'l #:else
+          (λ () (raise-syntax-error #f
+                   (format "~a field does not exist" (syntax->datum #'l))
+                   stx)))
+   #:with [e- τ_e] (infer+erase #'e)
+   #:fail-unless (typecheck? #'τ_e #'τ_match)
+   (typecheck-fail-msg/1 #'τ_match #'τ_e #'e)
+   (⊢ (list- 'l e) : τ.norm)])
 (define-typed-syntax case
   #:datum-literals (of =>)
   [(case e [l:id x:id => e_l] ...)
    #:fail-when (null? (syntax->list #'(l ...))) "no clauses"
-   #:with (e- ([l_x τ_x] ...)) (⇑ e as ∨)
+   #:with [e- (~∨* [l_x : τ_x] ...)] (infer+erase #'e)
    #:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
    #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"
    #:with (((x-) e_l- τ_el) ...)
           (stx-map (λ (bs e) (infer/ctx+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...))
-   #:fail-unless (same-types? #'(τ_el ...)) "branches have different types"
    (⊢ (let- ([l_e (car- e-)])
         (cond- [(symbol=?- l_e 'l) (let- ([x- (cadr- e-)]) e_l-)] ...))
-      : #,(stx-car #'(τ_el ...)))])
+      : (⊔ τ_el ...))])
diff --git a/macrotypes/examples/stlc+tup.rkt b/macrotypes/examples/stlc+tup.rkt
index c742c21..988a2e1 100644
--- a/macrotypes/examples/stlc+tup.rkt
+++ b/macrotypes/examples/stlc+tup.rkt
@@ -27,7 +27,7 @@
    (⊢ (list- e- ...) : (× τ ...))])
 (define-typed-syntax proj
   [(proj e_tup n:nat)
-   #:with [e_tup- τs_tup] (⇑ e_tup as ×)
+   #:with [e_tup- (~× . τs_tup)] (infer+erase #'e_tup)
    #:fail-unless (< (syntax-e #'n) (stx-length #'τs_tup)) "index too large"
    (⊢ (list-ref- e_tup- n) : #,(stx-list-ref #'τs_tup (syntax-e #'n)))])
    
diff --git a/macrotypes/examples/stlc.rkt b/macrotypes/examples/stlc.rkt
index 29c6e02..d2659cb 100644
--- a/macrotypes/examples/stlc.rkt
+++ b/macrotypes/examples/stlc.rkt
@@ -1,6 +1,5 @@
 #lang s-exp macrotypes/typecheck
 (provide (for-syntax current-type=? types=?))
-(provide (for-syntax mk-app-err-msg))
  
 (require (for-syntax racket/list))
 
@@ -81,50 +80,12 @@
    #:with (xs- e- τ_res) (infer/ctx+erase #'bvs #'e)
    (⊢ (λ- xs- e-) : (→ bvs.type ... τ_res))])
 
-(define-for-syntax (mk-app-err-msg stx #:expected [expected-τs #'()]
-                                       #:given [given-τs #'()]
-                                       #:note [note ""]
-                                       #:name [name #f])
-  (syntax-parse stx
-    #;[(app . rst)
-     #:when (not (equal? '#%app (syntax->datum #'app)))
-     (mk-app-err-msg (syntax/loc stx (#%app app . rst))
-       #:expected expected-τs
-       #:given given-τs
-       #:note note
-       #:name name)]
-    [(app e_fn e_arg ...)
-     (define fn-name
-       (if name name
-           (format "function ~a"
-                   (syntax->datum (or (get-orig #'e_fn) #'e_fn)))))
-     (string-append
-      (format "~a (~a:~a):\nType error applying "
-              (syntax-source stx) (syntax-line stx) (syntax-column stx))
-      fn-name ". " note "\n"
-      (format "  Expected: ~a argument(s) with type(s): " (stx-length expected-τs))
-      (string-join (stx-map type->str expected-τs) ", " #:after-last "\n")
-      "  Given:\n"
-      (string-join
-       (map (λ (e t) (format "    ~a : ~a" e t)) ; indent each line
-            (syntax->datum #'(e_arg ...))
-            (if (stx-length=? #'(e_arg ...) given-τs)
-                (stx-map type->str given-τs)
-                (stx-map (lambda (e) "?") #'(e_arg ...))))
-       "\n")
-      "\n")]))
-
 (define-typed-syntax #%app #:literals (#%app)
   [(#%app e_fn e_arg ...)
-   #:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn as →)
+   #:with [e_fn- (~→ τ_in ... τ_out)] (infer+erase #'e_fn)
    #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
    #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ_in ...))
-                 (type-error #:src stx
-                  #:msg (mk-app-err-msg stx #:expected #'(τ_in ...) 
-                                            #:given #'(τ_arg ...)
-                                            #:note "Wrong number of arguments."))
+   (num-args-fail-msg #'e_fn #'(τ_in ...) #'(e_arg ...))
    #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
-                 (type-error #:src stx
-                  #:msg (mk-app-err-msg stx #:expected #'(τ_in ...) 
-                                            #:given #'(τ_arg ...)))
-  (⊢ (#%app- e_fn- e_arg- ...) : τ_out)])
+   (typecheck-fail-msg/multi #'(τ_in ...) #'(τ_arg ...) #'(e_arg ...))
+   (⊢ (#%app- e_fn- e_arg- ...) : τ_out)])
diff --git a/macrotypes/examples/tests/ext-stlc-tests.rkt b/macrotypes/examples/tests/ext-stlc-tests.rkt
new file mode 100644
index 0000000..4c40524
--- /dev/null
+++ b/macrotypes/examples/tests/ext-stlc-tests.rkt
@@ -0,0 +1,171 @@
+#lang s-exp "../ext-stlc.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; tests for stlc extensions
+;; 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)
+ #:with-msg "expected: +Unit\n *given: +Int\n *expressions: 2")
+(typecheck-fail
+ ((λ ([x : Unit]) x) void)
+  #:with-msg "expected: +Unit\n *given: +\\(→ Unit\\)\n *expressions: void")
+
+(check-type ((λ ([x : Unit]) x) (void)) : Unit)
+
+;; begin
+(check-type (begin 1) : Int)
+
+(typecheck-fail (begin) #:with-msg "expected more terms")
+;; 2016-03-06: begin terms dont need to be Unit
+(check-type (begin 1 2 3) : Int)
+#;(typecheck-fail
+ (begin 1 2 3)
+ #:with-msg "Expected expression 1 to have Unit type, got: Int")
+
+(check-type (begin (void) 1) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int)
+(check-type ((λ ([x : Int]) (begin x)) 1) : Int)
+(check-type ((λ ([x : Int]) (begin (begin x))) 1) : Int)
+(check-type ((λ ([x : Int]) (begin (void) (begin (void) x))) 1) : Int)
+(check-type ((λ ([x : Int]) (begin (begin (void) x))) 1) : Int)
+
+;;ascription
+(check-type (ann 1 : Int) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
+(typecheck-fail (ann 1 : Bool)
+                #:with-msg "ann: type mismatch: expected Bool, given Int\n *expression: 1")
+;ann errs
+(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
+(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
+(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
+(typecheck-fail (ann Int : Int)
+                #:with-msg "ann: type mismatch: expected Int, given #%type\n *expression: Int")
+
+; let
+(check-type (let () (+ 1 1)) : Int ⇒ 2)
+(check-type (let ([x 10]) (+ 1 2)) : Int)
+(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
+(typecheck-fail
+ (let ([x #f]) (+ x 1))
+ #:with-msg "expected: +Int, Int\n *given: +Bool, Int\n *expressions: x, 1")
+(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))
+                #:with-msg "x: unbound identifier")
+
+(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
+(typecheck-fail
+ (let* ([x #t] [y (+ x 1)]) 1)
+  #:with-msg "expected: +Int, Int\n *given: +Bool, Int\n *expressions: x, 1")
+
+; letrec
+(typecheck-fail
+ (letrec ([(x : Int) #f] [(y : Int) 1]) y)
+ #:with-msg
+ "letrec: type mismatch\n *expected: +Int, Int\n *given: +Bool, Int\n *expressions: #f, 1")
+(typecheck-fail
+ (letrec ([(y : Int) 1] [(x : Int) #f]) x)
+ #:with-msg
+ "letrec: type mismatch\n *expected: +Int, Int\n *given: +Int, Bool\n *expressions: 1, #f")
+(typecheck-fail
+ (ann (letrec ([(x : Int) #f] [(y : Int) 1]) y) : Int)
+ #:with-msg
+ "letrec: type mismatch\n *expected: +Int, Int\n *given: +Bool, Int\n *expressions: #f, 1")
+(typecheck-fail
+ (ann (letrec ([(y : Int) 1] [(x : Int) #f]) x) : Int)
+ #:with-msg
+ "letrec: type mismatch\n *expected: +Int, Int\n *given: +Int, Bool\n *expressions: 1, #f")
+
+(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)
+
+;; check some more err msgs
+(typecheck-fail
+ (and "1" #f)
+ #:with-msg
+ "and: type mismatch: expected Bool, given String\n *expression: \"1\"")
+(typecheck-fail
+ (and #t "2")
+ #:with-msg
+ "and: type mismatch: expected Bool, given String\n *expression: \"2\"")
+(typecheck-fail
+ (or "1" #f)
+ #:with-msg
+ "or: type mismatch\n *expected: +Bool, Bool\n *given: +String, Bool\n *expressions: \"1\", #f")
+(typecheck-fail
+ (or #t "2")
+ #:with-msg
+ "or: type mismatch\n *expected: +Bool, Bool\n *given: +Bool, String\n *expressions: #t, \"2\"")
+;; 2016-03-10: change if to work with non-false vals
+(check-type (if "true" 1 2) : Int -> 1)
+(typecheck-fail
+ (if #t 1 "2")
+ #:with-msg 
+ "branches have incompatible types: Int and String")
+
+;; 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)
+ #:with-msg "expected: +Bool\n *given: +Int\n *expressions: 1")
+;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
+(typecheck-fail
+ (λ ([f : Int]) (f 1 2))
+ #:with-msg
+ "Expected → type, got: Int")
+
+(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))
+ #:with-msg (string-append "expected: +Int, Int\n *given: +Int, \\(→ Int Int\\)\n"
+                           " *expressions: 1, \\(λ \\(\\(x : Int\\)\\) x\\)"))
+(typecheck-fail
+ (λ ([x : (→ Int Int)]) (+ x x))
+  #:with-msg "expected: +Int, Int\n *given: +\\(→ Int Int\\), \\(→ Int Int\\)\n *expressions: x, x")
+(typecheck-fail
+ ((λ ([x : Int] [y : Int]) y) 1)
+ #:with-msg "wrong number of arguments: expected 2, given 1")
+
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+
diff --git a/macrotypes/examples/tests/infer-tests.rkt b/macrotypes/examples/tests/infer-tests.rkt
index 5a27a6f..e91c1d7 100644
--- a/macrotypes/examples/tests/infer-tests.rkt
+++ b/macrotypes/examples/tests/infer-tests.rkt
@@ -69,7 +69,7 @@
 ; list abbrv
 (check-type (list 1 2 3) : (List Int))
 (typecheck-fail (list 1 "3")
- #:with-msg "cons expression.+with type Int to list.+with type \\(List String\\)")
+ #:with-msg "expected \\(List Int\\), given \\(List String\\)\n *expression: \\(list \"3\"\\)")
 
 
 (define {X Y} (map [f : (→ X Y)] [lst : (List X)] → (List Y))
@@ -241,12 +241,12 @@
 ;;ascription
 (check-type (ann 1 : Int) : Int ⇒ 1)
 (check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
-(typecheck-fail (ann 1 : Bool) #:with-msg "ann: 1 does not have type Bool")
+(typecheck-fail (ann 1 : Bool) #:with-msg "expected Bool, given Int\n *expression: 1")
 ;ann errs
 (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
 (typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
 (typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
-(typecheck-fail (ann Int : Int) #:with-msg "does not have type Int")
+(typecheck-fail (ann Int : Int) #:with-msg "expected Int, given #%type\n *expression: Int")
 
 ; let
 (check-type (let () (+ 1 1)) : Int ⇒ 2)
@@ -269,11 +269,11 @@
 (typecheck-fail
  (letrec ([(x : Int) #f] [(y : Int) 1]) y)
  #:with-msg
- "letrec: type check fail, args have wrong type:\n#f has type Bool, expected Int")
+ "letrec: type mismatch\n *expected: +Int, Int\n *given: +Bool, Int\n *expressions: #f, 1")
 (typecheck-fail
  (letrec ([(y : Int) 1] [(x : Int) #f]) x)
  #:with-msg
- "letrec: type check fail, args have wrong type:.+#f has type Bool, expected Int")
+ "letrec: type mismatch\n *expected: +Int, Int\n *given: +Int, Bool\n *expressions: 1, #f")
 
 (check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
 
@@ -301,19 +301,19 @@
 ;; check some more err msgs
 (typecheck-fail
  (and "1" #f)
- #:with-msg "Expected expression \"1\" to have Bool type, got: String")
+ #:with-msg "and: type mismatch: expected Bool, given String\n *expression: \"1\"")
 (typecheck-fail
  (and #t "2")
  #:with-msg
- "Expected expression \"2\" to have Bool type, got: String")
+ "and: type mismatch: expected Bool, given String\n *expression: \"2\"")
 (typecheck-fail
  (or "1" #f)
  #:with-msg
- "Expected expression \"1\" to have Bool type, got: String")
+ "or: type mismatch\n  expected: +Bool, Bool\n *given: +String, Bool\n *expressions: \"1\", #f")
 (typecheck-fail
  (or #t "2")
  #:with-msg
- "Expected expression \"2\" to have Bool type, got: String")
+ "or: type mismatch\n  expected: +Bool, Bool\n *given: +Bool, String\n *expressions: #t, \"2\"")
 ;; 2016-03-10: change if to work with non-false vals
 (check-type (if "true" 1 2) : Int -> 1)
 (typecheck-fail
diff --git a/macrotypes/examples/tests/mlish-tests.rkt b/macrotypes/examples/tests/mlish-tests.rkt
new file mode 100644
index 0000000..50f39f7
--- /dev/null
+++ b/macrotypes/examples/tests/mlish-tests.rkt
@@ -0,0 +1,788 @@
+#lang s-exp "../mlish.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; match on tups
+(check-type
+    (match (tup 1 2) with
+      [x y -> (+ x y)])
+  : Int -> 3)
+
+;; tests more or less copied from infer-tests.rkt ------------------------------
+(typecheck-fail (λ (x) x) #:with-msg "λ: no expected type, add annotations")
+
+;; top-level defines
+(define (f [x : Int] → Int) x)
+(typecheck-fail (f 1 2) #:with-msg "f: wrong number of arguments: expected 1, given 2")
+(check-type f : (→ Int Int))
+(check-type (f 1) : Int ⇒ 1)
+(typecheck-fail (f (λ ([x : Int]) x)))
+
+(define (g [x : X] → X) x)
+(check-type g : (→/test X X))
+
+;; (inferred) polymorpic instantiation
+(check-type (g 1) : Int ⇒ 1)
+(check-type (g #f) : Bool ⇒ #f) ; different instantiation
+(check-type (g add1) : (→ Int Int))
+(check-type (g +) : (→ Int Int Int))
+
+;; function polymorphic in list element
+(define-type (List X)
+  Nil
+  (Cons X (List X)))
+
+;; arity err
+(typecheck-fail (Cons 1) #:with-msg "Cons: wrong number of arguments: expected 2, given 1")
+
+;; type err
+(typecheck-fail (Cons 1 1)
+  #:with-msg "expected: \\(List Int\\)\n *given: Int")
+
+(typecheck-fail 
+  (match (Cons 1 Nil) with
+   [Nil -> 1])
+  #:with-msg "match: clauses not exhaustive; missing: Cons")
+(typecheck-fail 
+  (match (Cons 1 Nil) with
+   [Cons x xs -> 1])
+  #:with-msg "match: clauses not exhaustive; missing: Nil")
+  
+(define (g2 [lst : (List Y)] → (List Y)) lst)
+(check-type g2 : (→/test (List Y) (List Y)))
+(typecheck-fail (g2 1) 
+  #:with-msg 
+  "expected: \\(List Y\\)\n *given: Int")
+
+;; todo? allow polymorphic nil?
+(check-type (g2 (Nil {Int})) : (List Int) ⇒ (Nil {Int}))
+(check-type (g2 (Nil {Bool})) : (List Bool) ⇒ (Nil {Bool}))
+(check-type (g2 (Nil {(List Int)})) : (List (List Int)) ⇒ (Nil {(List Int)}))
+(check-type (g2 (Nil {(→ Int Int)})) : (List (→ Int Int)) ⇒ (Nil {(List (→ Int Int))}))
+;; annotations unneeded: same as tests above, but without annotations
+(check-type (g2 Nil) : (List Int) ⇒ Nil)
+(check-type (g2 Nil) : (List Bool) ⇒ Nil)
+(check-type (g2 Nil) : (List (List Int)) ⇒ Nil)
+(check-type (g2 Nil) : (List (→ Int Int)) ⇒ Nil)
+
+(check-type (g2 (Cons 1 Nil)) : (List Int) ⇒ (Cons 1 Nil))
+(check-type (g2 (Cons "1" Nil)) : (List String) ⇒ (Cons "1" Nil))
+
+;; mlish cant type this fn (ie, incomplete cases on variant --- what to put for Nil case?)
+;(define (g3 [lst : (List X)] → X) (hd lst)) 
+;(check-type g3 : (→ {X} (List X) X))
+;(check-type g3 : (→ {A} (List A) A))
+;(check-not-type g3 : (→ {A B} (List A) B))
+;(typecheck-fail (g3) #:with-msg "Expected.+arguments with type.+List") ; TODO: more precise err msg
+;(check-type (g3 (nil {Int})) : Int) ; runtime fail
+;(check-type (g3 (nil {Bool})) : Bool) ; runtime fail
+;(check-type (g3 (cons 1 nil)) : Int ⇒ 1)
+;(check-type (g3 (cons "1" nil)) : String ⇒ "1")
+
+;; recursive fn
+(define (recf [x : Int] → Int) (recf x))
+(check-type recf : (→ Int Int))
+
+(define (countdown [x : Int] → Int)
+  (if (zero? x)
+      0
+      (countdown (sub1 x))))
+(check-type (countdown 0) : Int ⇒ 0)
+(check-type (countdown 10) : Int ⇒ 0)
+(typecheck-fail (countdown "10") #:with-msg "expected: Int\n *given: String")
+
+;; list fns ----------
+
+; map: tests whether match and define properly propagate 'expected-type
+(define (map [f : (→ X Y)] [lst : (List X)] → (List Y))
+  (match lst with
+    [Nil -> Nil]
+    [Cons x xs -> (Cons (f x) (map f xs))]))
+(check-type map : (→/test (→ X Y) (List X) (List Y)))
+(check-type map : (→/test {Y X} (→ Y X) (List Y) (List X)))
+(check-type map : (→/test (→ A B) (List A) (List B)))
+(check-not-type map : (→/test (→ A B) (List B) (List A)))
+(check-not-type map : (→/test (→ X X) (List X) (List X))) ; only 1 bound tyvar
+
+; nil without annotation; tests fn-first, left-to-right arg inference
+; does work yet, need to add left-to-right inference in #%app
+(check-type (map add1 Nil) : (List Int) ⇒ Nil)
+(check-type (map add1 (Cons 1 (Cons 2 (Cons 3 Nil)))) 
+  : (List Int) ⇒ (Cons 2 (Cons 3 (Cons 4 Nil))))
+(typecheck-fail (map add1 (Cons "1" Nil))
+  #:with-msg "expected: Int\n *given: String")
+(check-type (map (λ ([x : Int]) (+ x 2)) (Cons 1 (Cons 2 (Cons 3 Nil)))) 
+  : (List Int) ⇒ (Cons 3 (Cons 4 (Cons 5 Nil))))
+;; ; doesnt work yet: all lambdas need annotations
+;; (check-type (map (λ (x) (+ x 2)) (list 1 2 3)) : (List Int) ⇒ (list 3 4 5))
+
+(define (filter [p? : (→ X Bool)] [lst : (List X)] → (List X))
+  (match lst with
+   [Nil -> Nil]
+   [Cons x xs -> (if (p? x) 
+                     (Cons x (filter p? xs)) 
+                     (filter p? xs))]))
+(define (filter/guard [p? : (→ X Bool)] [lst : (List X)] → (List X))
+  (match lst with
+   [Nil -> Nil]
+   [Cons x xs #:when (p? x) -> (Cons x (filter p? xs))]
+   [Cons x xs -> (filter p? xs)]))
+(check-type (filter zero? Nil) : (List Int) ⇒ Nil)
+(check-type (filter zero? (Cons 1 (Cons 2 (Cons 3 Nil)))) 
+  : (List Int) ⇒ Nil)
+(check-type (filter zero? (Cons 0 (Cons 1 (Cons 2 Nil)))) 
+  : (List Int) ⇒ (Cons 0 Nil))
+(check-type (filter (λ (x) (not (zero? x))) (Cons 0 (Cons 1 (Cons 2 Nil)))) 
+  : (List Int) ⇒ (Cons 1 (Cons 2 Nil)))
+(check-type (filter/guard zero? Nil) : (List Int) ⇒ Nil)
+(check-type (filter/guard zero? (Cons 1 (Cons 2 (Cons 3 Nil)))) 
+  : (List Int) ⇒ Nil)
+(check-type (filter/guard zero? (Cons 0 (Cons 1 (Cons 2 Nil)))) 
+  : (List Int) ⇒ (Cons 0 Nil))
+(check-type 
+  (filter/guard (λ (x) (not (zero? x))) (Cons 0 (Cons 1 (Cons 2 Nil)))) 
+  : (List Int) ⇒ (Cons 1 (Cons 2 Nil)))
+; doesnt work yet: all lambdas need annotations
+;(check-type (filter (λ (x) (not (zero? x))) (list 0 1 2)) : (List Int) ⇒ (list 1 2))
+
+(define (foldr [f : (→ X Y Y)] [base : Y] [lst : (List X)] → Y)
+  (match lst with
+   [Nil -> base]
+   [Cons x xs -> (f x (foldr f base xs))]))
+(define (foldl [f : (→ X Y Y)] [acc : Y] [lst : (List X)] → Y)
+  (match lst with
+   [Nil -> acc]
+   [Cons x xs -> (foldr f (f x acc) xs)]))
+
+(define (all? [p? : (→ X Bool)] [lst : (List X)] → Bool)
+  (match lst with
+   [Nil -> #t]
+   [Cons x xs #:when (p? x) -> (all? p? xs)]
+   [Cons x xs -> #f]))
+
+(define (tails [lst : (List X)] → (List (List X)))
+  (match lst with
+   [Nil -> (Cons Nil Nil)]
+   [Cons x xs -> (Cons lst (tails xs))]))
+
+(define (build-list [n : Int] [f : (→ Int X)] → (List X))
+  (if (zero? (sub1 n))
+      (Cons (f 0) Nil)
+      (Cons (f (sub1 n)) (build-list (sub1 n) f))))
+(check-type (build-list 1 add1) : (List Int) ⇒ (Cons 1 Nil))
+(check-type (build-list 3 add1) : (List Int) ⇒ (Cons 3 (Cons 2 (Cons 1 Nil))))
+(check-type (build-list 5 sub1) 
+  : (List Int) ⇒ (Cons 3 (Cons 2 (Cons 1 (Cons 0 (Cons -1 Nil))))))
+(check-type (build-list 5 (λ (x) (add1 (add1 x))))
+  : (List Int) ⇒ (Cons 6 (Cons 5 (Cons 4 (Cons 3 (Cons 2 Nil))))))
+
+(define (build-list/comp [i : Int] [n : Int] [nf : (→ Int Int)] [f : (→ Int X)] → (List X))
+  (if (= i n)
+      Nil
+      (Cons (f (nf i)) (build-list/comp (add1 i) n nf f))))
+
+(define built-list-1 (build-list/comp 0 3 (λ (x) (* 2 x)) add1))
+(define built-list-2 (build-list/comp 0 3 (λ (x) (* 2 x)) number->string))
+(check-type built-list-1 : (List Int) -> (Cons 1 (Cons 3 (Cons 5 Nil))))
+(check-type built-list-2 : (List String) -> (Cons "0" (Cons "2" (Cons "4" Nil))))
+
+(define (~>2 [a : A] [f : (→ A A)] [g : (→ A B)] → B)
+  (g (f a)))
+
+(define ~>2-result-1 (~>2 1 (λ (x) (* 2 x)) add1))
+(define ~>2-result-2 (~>2 1 (λ (x) (* 2 x)) number->string))
+(check-type ~>2-result-1 : Int -> 3)
+(check-type ~>2-result-2 : String -> "2")
+
+(define (append [lst1 : (List X)] [lst2 : (List X)] → (List X))
+  (match lst1 with
+   [Nil -> lst2]
+   [Cons x xs -> (Cons x (append xs lst2))]))
+
+(check-type (λ (a f g) (g (f a) (+ (f 1) (f 2))))
+            : (→/test Int (→ Int Int) (→ Int Int C) C))
+
+(check-type ((λ ([a : A] [f : (→ Int A)]) a) 4 (λ (x) x))
+            : Int)
+
+;; end infer.rkt tests --------------------------------------------------
+
+;; algebraic data types
+(define-type IntList
+  INil
+  (ConsI Int IntList))
+
+;; HO, monomorphic
+(check-type ConsI : (→ Int IntList IntList))
+(define (new-cons [c : (→ Int IntList IntList)] [x : Int] [xs : IntList] 
+                  -> IntList)
+  (c x xs))
+(check-type (new-cons ConsI 1 INil) : IntList -> (ConsI 1 INil))
+
+;; check that ConsI and INil are available as tyvars
+(define (f10 [x : INil] [y : ConsI] -> ConsI) y)
+(check-type f10 : (→/test X Y Y))
+
+(check-type INil : IntList)
+(check-type (ConsI 1 INil) : IntList)
+(check-type
+ (match INil with
+   [INil -> 1]
+   [ConsI x xs -> 2]) : Int ⇒ 1)
+(check-type
+ (match (ConsI 1 INil) with
+   [INil -> 1]
+   [ConsI x xs -> 2]) : Int ⇒ 2)
+(typecheck-fail (match 1 with [INil -> 1]))
+
+(typecheck-fail (ConsI #f INil)
+ #:with-msg 
+ "expected: Int\n *given: Bool")
+
+;; annotated
+(check-type (Nil {Int}) : (List Int))
+(check-type (Cons {Int} 1 (Nil {Int})) : (List Int))
+(check-type (Cons {Int} 1 (Cons 2 (Nil {Int}))) : (List Int))
+;; partial annotations
+(check-type (Cons 1 (Nil {Int})) : (List Int))
+(check-type (Cons 1 (Cons 2 (Nil {Int}))) : (List Int))
+(check-type (Cons {Int} 1 Nil) : (List Int))
+(check-type (Cons {Int} 1 (Cons 2 Nil)) : (List Int))
+(check-type (Cons 1 (Cons {Int} 2 Nil)) : (List Int))
+; no annotations
+(check-type (Cons 1 Nil) : (List Int))
+(check-type (Cons 1 (Cons 2 Nil)) : (List Int))
+
+(define-type (Tree X)
+  (Leaf X)
+  (Node (Tree X) (Tree X)))
+(check-type (Leaf 10) : (Tree Int))
+(check-type (Node (Leaf 10) (Leaf 11)) : (Tree Int))
+
+(typecheck-fail Nil #:with-msg "Nil: no expected type, add annotations")
+(typecheck-fail (Cons 1 (Nil {Bool}))
+ #:with-msg 
+ "expected: \\(List Int\\)\n *given: \\(List Bool\\)")
+(typecheck-fail (Cons {Bool} 1 (Nil {Int}))
+ #:with-msg
+ (string-append
+  "Cons: type mismatch\n *expected: +Bool, \\(List Bool\\)\n *given: +Int, \\(List Int\\)\n"
+  " *expressions: 1, \\(Nil \\(Int\\)\\)"))
+(typecheck-fail (Cons {Bool} 1 Nil)
+ #:with-msg
+ (string-append
+  "Cons: type mismatch\n *expected: +Bool, \\(List Bool\\)\n *given: +Int, \\(List Bool\\)\n"
+  " *expressions: 1, Nil"))
+
+(typecheck-fail (match Nil with [Cons x xs -> 2] [Nil -> 1])
+                #:with-msg "Nil: no expected type, add annotations")
+(check-type
+ (match (Nil {Int}) with
+   [Cons x xs -> 2]
+   [Nil -> 1])
+ : Int ⇒ 1)
+
+(check-type
+ (match (Nil {Int}) with
+   [Nil -> 1]
+   [Cons x xs -> 2])
+ : Int ⇒ 1)
+
+(check-type
+ (match (Cons 1 Nil) with
+   [Nil -> 3]
+   [Cons y ys -> (+ y 4)])
+ : Int ⇒ 5)
+            
+(check-type
+ (match (Cons 1 Nil) with
+   [Cons y ys -> (+ y 5)]
+   [Nil -> 3])
+ : Int ⇒ 6)
+            
+;; check expected-type propagation for other match paterns
+
+(define-type (Option A)
+  (None)
+  (Some A))
+
+(define (None* → (Option A)) None)
+
+(check-type (match (tup 1 2) with [a b -> None]) : (Option Int) -> None)
+(check-type 
+  (match (list 1 2) with 
+   [[] -> None]
+   [[x y] -> None]) 
+  : (Option Int) -> None)
+
+(check-type 
+  (match (list 1 2) with 
+   [[] -> None]
+   [x :: xs -> None]) 
+  : (Option Int) -> None)
+
+(define-type (Pairof A B) (C A B))
+(check-type (match (C 1 2) with [C a b -> None]) : (Option Int) -> None)
+
+;; type variable inference
+
+; F should remain valid tyvar, even though it's bound
+(define (F [x : X] -> X) x) 
+(define (tvf1 [x : F] -> F) x)
+(check-type tvf1 : (→/test X X))
+
+; G should remain valid tyvar
+(define-type (Type1 X) (G X)) 
+(define (tvf5 [x : G] -> G) x)
+(check-type tvf5 : (→/test X X))
+
+; TY should not be tyvar, bc it's a valid type
+(define-type-alias TY (Pairof Int Int))
+(define (tvf2 [x : TY] -> TY) x)
+(check-not-type tvf2 : (→/test X X))
+
+; same with Bool
+(define (tvf3 [x : Bool] -> Bool) x)
+(check-not-type tvf3 : (→/test X X))
+
+;; X in lam should not be a new tyvar
+(define (tvf4 [x : X] -> (→ X X))
+  (λ (y) x))
+(check-type tvf4 : (→/test X (→ X X)))
+(check-not-type tvf4 : (→/test X (→ Y X)))
+
+(define (tvf6 [x : X] -> (→ Y X))
+  (λ (y) x))
+(check-type tvf6 : (→/test X (→ Y X)))
+
+;; nested lambdas
+
+(check-type (λ ([x : X]) (λ ([y : X]) y)) : (→/test X (→ X X)))
+(check-not-type (λ ([x : X]) (λ ([y : X]) y)) : (→/test {X} X (→/test {Y} Y Y)))
+(check-type (λ ([x : X]) (λ ([y : Y]) y)) : (→/test {X} X (→/test {Y} Y Y)))
+(check-not-type (λ ([x : X]) (λ ([y : Y]) x)) : (→/test X (→ X X)))
+
+(check-type 
+  ((λ ([x : X]) (λ ([y : Y]) y)) 1)
+  : (→/test Y Y))
+
+;; TODO?
+;; - this fails if polymorphic functions are allowed as HO args
+;;   - do we want to allow this?
+;; - must explicitly instantiate before passing fn
+(check-type 
+  ((λ ([x : (→ X (→ Y Y))]) x) 
+   (inst (λ ([x : X]) (inst (λ ([y : Y]) y) Int)) Int))
+   : (→ Int (→ Int Int)))  
+
+(check-type 
+  ((λ ([x : X]) (λ ([y : Y]) (λ ([z : Z]) z))) 1)
+  : (→/test {Y} Y (→/test {Z} Z Z)))
+
+(check-type (inst Cons (→/test X X))
+  : (→ (→/test X X) (List (→/test X X)) (List (→/test X X))))
+(check-type map : (→/test (→ X Y) (List X) (List Y)))
+
+(check-type (Cons (λ ([x : X]) x) Nil)
+  : (List (→/test {X} X X)))
+
+(define (nn [x : X] -> (→ (× X (→ Y Y))))
+  (λ () (tup x (λ ([x : Y]) x))))
+(typecheck-fail (nn 1) #:with-msg "Could not infer instantiation of polymorphic function nn.")
+(check-type (nn 1) : (→ (× Int (→ String String))))
+(check-type (nn 1) : (→ (× Int (→ (List Int) (List Int)))))
+
+(define (nn2 [x : X] -> (→ (× X (→ Y Y) (List Z))))
+  (λ () (tup x (λ ([x : Y]) x) Nil)))
+(typecheck-fail (nn2 1) #:with-msg "Could not infer instantiation of polymorphic function nn2.")
+(check-type (nn2 1) : (→ (× Int (→ String String) (List (List Int)))))
+(check-type (nn2 1) : (→ (× Int (→ (List Int) (List Int)) (List String))))
+;; test inst order
+(check-type ((inst nn2 Int String (List Int)) 1)
+            : (→ (× Int (→ String String) (List (List Int)))))
+(check-type ((inst nn2 Int (List Int) String) 1)
+            : (→ (× Int (→ (List Int) (List Int)) (List String))))
+
+(define (nn3 [x : X] -> (→ (× X (Option Y) (Option Z))))
+  (λ () (tup x None None)))
+(check-type (nn3 1) : (→/test (× Int (Option Y) (Option Z))))
+(check-type (nn3 1) : (→ (× Int (Option String) (Option (List Int)))))
+(check-type ((nn3 1)) : (× Int (Option String) (Option (List Int))))
+(check-type ((nn3 1)) : (× Int (Option (List Int)) (Option String)))
+;; test inst order
+(check-type ((inst (nn3 1) String (List Int))) : (× Int (Option String) (Option (List Int))))
+(check-type ((inst (nn3 1) (List Int) String)) : (× Int (Option (List Int)) (Option String)))
+
+(define (nn4 -> (→ (Option X)))
+  (λ () (None*)))
+(check-type (let ([x (nn4)])
+              x)
+            : (→/test (Option X)))
+
+(define (nn5 -> (→ (Ref (Option X))))
+  (λ () (ref (None {X}))))
+(typecheck-fail (let ([x (nn5)])
+                  x)
+                #:with-msg "Could not infer instantiation of polymorphic function nn5.")
+
+(define (nn6 -> (→ (Option X)))
+  (let ([r (((inst nn5 X)))])
+    (λ () (deref r))))
+(check-type (nn6) : (→/test (Option X)))
+
+;; A is covariant, B is invariant.
+(define-type (Cps A B)
+  (cps (→ (→ A B) B)))
+(define (cps* [f : (→ (→ A B) B)] → (Cps A B))
+  (cps f))
+
+(define (nn7 -> (→ (Cps (Option A) B)))
+  (let ([r (((inst nn5 A)))])
+    (λ () (cps* (λ (k) (k (deref r)))))))
+(typecheck-fail (let ([x (nn7)])
+                  x)
+                #:with-msg "Could not infer instantiation of polymorphic function nn7.")
+
+(define (nn8 -> (→ (Cps (Option A) Int)))
+  (nn7))
+(check-type (let ([x (nn8)])
+              x)
+            : (→/test (Cps (Option A) Int)))
+
+(define-type (Result A B)
+  (Ok A)
+  (Error B))
+
+(define (ok [a : A] → (Result A B))
+  (Ok a))
+(define (error [b : B] → (Result A B))
+  (Error b))
+
+(define (ok-fn [a : A] -> (→ (Result A B)))
+  (λ () (ok a)))
+(define (error-fn [b : B] -> (→ (Result A B)))
+  (λ () (error b)))
+
+(check-type (let ([x (ok-fn 1)])
+              x)
+            : (→/test (Result Int B)))
+(check-type (let ([x (error-fn "bad")])
+              x)
+            : (→/test (Result A String)))
+
+(define (nn9 [a : A] -> (→ (Result A (Ref B))))
+  (ok-fn a))
+(define (nn10 [a : A] -> (→ (Result A (Ref String))))
+  (nn9 a))
+(define (nn11 -> (→ (Result (Option A) (Ref String))))
+  (nn10 (None*)))
+
+(typecheck-fail (let ([x (nn9 1)])
+                  x)
+                #:with-msg "Could not infer instantiation of polymorphic function nn9.")
+(check-type (let ([x (nn10 1)])
+              x)
+            : (→ (Result Int (Ref String))))
+(check-type (let ([x (nn11)])
+              x)
+            : (→/test (Result (Option A) (Ref String))))
+
+(check-type (if (zero? (random 2))
+                (ok 0)
+                (error "didn't get a zero"))
+            : (Result Int String))
+
+(define result-if-0
+  (λ ([b : (Result A1 B1)] [succeed : (→ A1 (Result A2 B2))] [fail : (→ B1 (Result A2 B2))])
+    (match b with
+      [Ok a -> (succeed a)]
+      [Error b -> (fail b)])))
+(check-type result-if-0
+            : (→/test (Result A1 B1) (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2))
+                      (Result A2 B2)))
+
+(define (result-if-1 [b : (Result A1 B1)]
+                     → (→ (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2))
+                          (Result A2 B2)))
+  (λ ([succeed : (→ A1 (Result A2 B2))] [fail : (→ B1 (Result A2 B2))])
+    (result-if-0 b succeed fail)))
+(check-type result-if-1
+            : (→/test (Result A1 B1) (→ (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2))
+                                        (Result A2 B2))))
+(check-type ((inst result-if-1 Int String (List Int) (List String)) (Ok 1))
+            : (→ (→ Int (Result (List Int) (List String)))
+                 (→ String (Result (List Int) (List String)))
+                 (Result (List Int) (List String))))
+(check-type ((inst result-if-1 Int String (List Int) (List String)) (Error "bad"))
+            : (→ (→ Int (Result (List Int) (List String)))
+                 (→ String (Result (List Int) (List String)))
+                 (Result (List Int) (List String))))
+(check-type (((inst result-if-1 Int String (List Int) (List String)) (Ok 1))
+             (λ ([a : Int])    (ok (Cons a Nil)))
+             (λ ([b : String]) (error (Cons b Nil))))
+            : (Result (List Int) (List String)))
+;; same thing, but without the lambda annotations:
+(check-type (((inst result-if-1 Int String (List Int) (List String)) (Ok 1))
+             (λ (a) (ok (Cons a Nil)))
+             (λ (b) (error (Cons b Nil))))
+            : (Result (List Int) (List String)))
+
+(define (result-if-2 [b : (Result A1 B1)]
+                     → (→ (→ A1 (Result A2 B2))
+                          (→ (→ B1 (Result A2 B2))
+                             (Result A2 B2))))
+  (λ ([succeed : (→ A1 (Result A2 B2))])
+    (λ ([fail : (→ B1 (Result A2 B2))])
+      (result-if-0 b succeed fail))))
+(check-type result-if-2
+            : (→/test (Result A1 B1) (→ (→ A1 (Result A2 B2))
+                                        (→ (→ B1 (Result A2 B2))
+                                           (Result A2 B2)))))
+(check-type ((inst result-if-2 Int String (List Int) (List String)) (Ok 1))
+            : (→/test (→ Int (Result (List Int) (List String)))
+                      (→ (→ String (Result (List Int) (List String)))
+                         (Result (List Int) (List String)))))
+(check-type (((inst result-if-2 Int String (List Int) (List String)) (Ok 1))
+             (λ (a) (Ok (Cons a Nil))))
+            : (→/test (→ String (Result (List Int) (List String)))
+                      (Result (List Int) (List String))))
+(check-type ((((inst result-if-2 Int String (List Int) (List String)) (Ok 1))
+              (λ (a) (Ok (Cons a Nil))))
+             (λ (b) (Error (Cons b Nil))))
+            : (Result (List Int) (List String)))
+
+(define (tup* [a : A] [b : B] -> (× A B))
+  (tup a b))
+
+(define (nn12 -> (→ (× (Option A) (Option B))))
+  (λ () (tup* (None*) (None*))))
+(check-type (let ([x (nn12)])
+              x)
+            : (→/test (× (Option A) (Option B))))
+
+(define (nn13 -> (→ (× (Option A) (Option (Ref B)))))
+  (nn12))
+(typecheck-fail (let ([x (nn13)])
+                  x)
+                #:with-msg "Could not infer instantiation of polymorphic function nn13.")
+
+;; records and automatically-defined accessors and predicates
+(define-type (RecoTest X Y)
+  (RT1 [x : X] [y : Y] [z : String])
+  (RT2 [a : Y] [b : X] [c : (List X)])
+  (RT3 X Y)) ; mixing records and non-records allowed
+
+(check-type RT1-x : (→/test (RecoTest X Y) X))
+(check-type RT1-y : (→/test (RecoTest X Y) Y))
+(check-type RT1-z : (→/test (RecoTest X Y) String))
+(check-type RT2-a : (→/test (RecoTest X Y) Y))
+(check-type RT2-b : (→/test (RecoTest X Y) X))
+
+(check-type RT1? : (→/test (RecoTest X Y) Bool))
+(check-type RT2? : (→/test (RecoTest X Y) Bool))
+(check-type RT3? : (→/test (RecoTest X Y) Bool))
+
+(check-type (RT1-x (RT1 1 #t "2")) : Int -> 1)
+(check-type (RT1-y (RT1 1 #t "2")) : Bool -> #t)
+(check-type (RT1-z (RT1 1 #t "2")) : String -> "2")
+
+(check-type (RT2-a (RT2 1 #f Nil)) : Int -> 1)
+(check-type (RT2-b (RT2 1 #f Nil)) : Bool -> #f)
+(check-type (RT2-c (RT2 1 #f Nil)) : (List Bool) -> Nil)
+
+(check-type (RT1? (RT1 1 2 "3")) : Bool -> #t)
+(check-type (RT1? (RT2 1 2 Nil)) : Bool -> #f)
+(check-type (RT1? (RT3 1 "2")) : Bool -> #f)
+(check-type (RT3? (RT3 1 2)) : Bool -> #t)
+(check-type (RT3? (RT1 1 2 "3")) : Bool -> #f)
+
+(typecheck-fail RT3-x #:with-msg "unbound identifier")
+  
+;; accessors produce runtime exception if given wrong variant
+(check-runtime-exn (RT1-x (RT2 1 #f (Cons #t Nil))))
+(check-runtime-exn (RT1-y (RT2 1 #f (Cons #t Nil))))
+(check-runtime-exn (RT1-z (RT2 1 #f (Cons #t Nil))))
+(check-runtime-exn (RT1-x (RT3 1 2)))
+(check-runtime-exn (RT2-a (RT1 1 #f "2")))
+(check-runtime-exn (RT2-c (RT1 1 #f "2")))
+(check-runtime-exn (RT2-c (RT1 1 #f "2")))
+(check-runtime-exn (RT2-a (RT3 #f #t)))
+
+;; non-match version
+(define (rt-fn [rt : (RecoTest X Y)] -> X)
+  (if (RT1? rt)
+      (RT1-x rt)
+      (if (RT2? rt)
+          (RT2-b rt)
+          (match rt with [RT3 x y -> x][RT1 x y z -> x][RT2 a b c -> b]))))
+(check-type (rt-fn (RT1 1 #f "3")) : Int -> 1)
+(check-type (rt-fn (RT2 #f 2 Nil)) : Int -> 2)
+(check-type (rt-fn (RT3 10 20)) : Int -> 10)
+
+;; HO constructors
+(check-type RT1 : (→/test X Y String (RecoTest X Y)))
+(check-type RT2 : (→/test {X Y} Y X (List X) (RecoTest X Y)))
+(check-type RT3 : (→/test X Y (RecoTest X Y)))
+
+(typecheck-fail (for/fold ([x 1]) () "hello") 
+ #:with-msg "for/fold: type mismatch: expected Int, given String\n *expression: \"hello\"")
+
+; ext-stlc tests --------------------------------------------------
+
+; tests for stlc extensions
+; 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)
+ #:with-msg
+ "expected: Unit\n *given: Int")
+(typecheck-fail
+ ((λ ([x : Unit]) x) void)
+ #:with-msg
+ "expected: Unit\n *given: \\(→ Unit\\)")
+
+(check-type ((λ ([x : Unit]) x) (void)) : Unit)
+
+;; begin
+(check-type (begin 1) : Int)
+
+(typecheck-fail (begin) #:with-msg "expected more terms")
+;; 2016-03-06: begin terms dont need to be Unit
+(check-type (begin 1 2 3) : Int)
+#;(typecheck-fail
+ (begin 1 2 3)
+ #:with-msg "Expected expression 1 to have Unit type, got: Int")
+
+(check-type (begin (void) 1) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int)
+(check-type ((λ ([x : Int]) (begin x)) 1) : Int)
+(check-type ((λ ([x : Int]) (begin (begin x))) 1) : Int)
+(check-type ((λ ([x : Int]) (begin (void) (begin (void) x))) 1) : Int)
+(check-type ((λ ([x : Int]) (begin (begin (void) x))) 1) : Int)
+
+;;ascription
+(check-type (ann 1 : Int) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
+(typecheck-fail (ann 1 : Bool) #:with-msg "expected Bool, given Int\n *expression: 1")
+;ann errs
+(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
+(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
+(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
+(typecheck-fail (ann Int : Int) #:with-msg "expected Int, given #%type\n *expression: Int")
+
+; let
+(check-type (let () (+ 1 1)) : Int ⇒ 2)
+(check-type (let ([x 10]) (+ 1 2)) : Int)
+(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
+(typecheck-fail
+ (let ([x #f]) (+ x 1))
+ #:with-msg "expected: Int\n *given: Bool")
+(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))
+                #:with-msg "x: unbound identifier")
+
+(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
+(typecheck-fail
+ (let* ([x #t] [y (+ x 1)]) 1)
+  #:with-msg "expected: Int\n *given: Bool")
+
+; letrec
+(typecheck-fail
+ (letrec ([(x : Int) #f] [(y : Int) 1]) y)
+ #:with-msg
+ "letrec: type mismatch\n *expected: +Int, Int\n *given: +Bool, Int\n *expressions: #f, 1")
+(typecheck-fail
+ (letrec ([(y : Int) 1] [(x : Int) #f]) x)
+ #:with-msg
+ "letrec: type mismatch\n *expected: +Int, Int\n *given: +Int, Bool\n *expressions: 1, #f")
+
+(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
+
+;; recursive
+(check-type
+ (letrec ([(countdown : (→ Int String))
+           (λ (i)
+             (if (= i 0)
+                 "liftoff"
+                 (countdown (- i 1))))])
+   (countdown 10)) : String ⇒ "liftoff")
+
+;; mutually recursive
+(check-type
+ (letrec ([(is-even? : (→ Int Bool))
+           (λ (n)
+             (or (zero? n)
+                 (is-odd? (sub1 n))))]
+          [(is-odd? : (→ Int Bool))
+           (λ (n)
+             (and (not (zero? n))
+                  (is-even? (sub1 n))))])
+   (is-odd? 11)) : Bool ⇒ #t)
+
+;; check some more err msgs
+(typecheck-fail
+ (and "1" #f)
+ #:with-msg "and: type mismatch: expected Bool, given String\n *expression: \"1\"")
+(typecheck-fail
+ (and #t "2")
+ #:with-msg
+ "and: type mismatch: expected Bool, given String\n *expression: \"2\"")
+(typecheck-fail
+ (or "1" #f)
+ #:with-msg
+ "or: type mismatch\n *expected: +Bool, Bool\n *given: +String, Bool\n *expressions: \"1\", #f")
+(typecheck-fail
+ (or #t "2")
+ #:with-msg
+ "or: type mismatch\n *expected: +Bool, Bool\n *given: +Bool, String\n *expressions: #t, \"2\"")
+;; 2016-03-09: now ok
+(check-type (if "true" 1 2) : Int -> 1)
+(typecheck-fail
+ (if #t 1 "2")
+ #:with-msg 
+ "branches have incompatible types: Int and String")
+
+;; 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 y) x) : (→ Int Int Int))
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ (x) x) : (→ Int Int))
+(check-type (λ (f) 1) : (→ (→ Int Int) Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+
+(typecheck-fail
+ ((λ ([x : Bool]) x) 1)
+ #:with-msg "expected: Bool\n *given: Int")
+;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
+(typecheck-fail
+ (λ ([f : Int]) (f 1 2))
+ #:with-msg
+ "Expected → type, got: Int")
+
+(check-type (λ (f x y) (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))
+ #:with-msg "expected: Int\n *given: \\(→ Int Int\\)")
+(typecheck-fail
+ (λ ([x : (→ Int Int)]) (+ x x))
+  #:with-msg "expected: Int\n *given: \\(→ Int Int\\)")
+(typecheck-fail
+ ((λ ([x : Int] [y : Int]) y) 1)
+ #:with-msg "wrong number of arguments: expected 2, given 1\n *expected: +Int, Int\n *arguments: 1")
+
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+
diff --git a/macrotypes/examples/tests/rackunit-typechecking.rkt b/macrotypes/examples/tests/rackunit-typechecking.rkt
new file mode 100644
index 0000000..ff712e9
--- /dev/null
+++ b/macrotypes/examples/tests/rackunit-typechecking.rkt
@@ -0,0 +1,3 @@
+#lang racket/base
+(provide (all-from-out turnstile/examples/tests/rackunit-typechecking))
+(require turnstile/examples/tests/rackunit-typechecking)
diff --git a/macrotypes/examples/tests/stlc+box-tests.rkt b/macrotypes/examples/tests/stlc+box-tests.rkt
new file mode 100644
index 0000000..84f3c61
--- /dev/null
+++ b/macrotypes/examples/tests/stlc+box-tests.rkt
@@ -0,0 +1,243 @@
+#lang s-exp "../stlc+box.rkt"
+(require "rackunit-typechecking.rkt")
+
+(define x (ref 10))
+(check-type x : (Ref Int))
+(check-type (deref x) : Int ⇒ 10)
+(check-type (:= x 20) : Unit) ; x still 10 because check-type does not evaluate
+(check-type (begin (:= x 20) (deref x)) : Int ⇒ 20)
+(check-type x : (Ref Int))
+(check-type (deref (ref 20)) : Int ⇒ 20)
+(check-type (deref x) : Int ⇒ 20)
+
+(check-type ((λ ([b : (Ref Int)]) (deref b)) (ref 10)) : Int ⇒ 10)
+(check-type ((λ ([b : (Ref Int)]) (begin (begin (:= b 20) (deref b)))) (ref 10)) : Int ⇒ 20)
+
+;; Ref err msgs
+; wrong arity
+(typecheck-fail
+ (λ ([lst : (Ref Int Int)]) lst)
+ #:with-msg
+ "Improper usage of type constructor Ref: \\(Ref Int Int\\), expected = 1 arguments")
+(typecheck-fail
+ (λ ([lst : (Ref)]) lst)
+ #:with-msg
+ "Improper usage of type constructor Ref: \\(Ref\\), expected = 1 arguments")
+(typecheck-fail
+ (deref 1)
+ #:with-msg
+ "Expected Ref type, got: Int")
+(typecheck-fail
+ (:= 1 1)
+ #:with-msg
+ "Expected Ref type, got: Int")
+(typecheck-fail
+ (:= (ref 1) "hi")
+ #:with-msg
+ ":=: type mismatch: expected Int, given String\n *expression: \"hi\"")
+
+;; previous tests: ------------------------------------------------------------
+(typecheck-fail (cons 1 2))
+;(typecheck-fail (cons 1 nil)) ; works now
+(check-type (cons 1 nil) : (List Int))
+(check-type (cons 1 (nil {Int})) : (List Int))
+(typecheck-fail nil)
+(typecheck-fail (nil Int))
+(typecheck-fail (nil (Int)))
+; passes bc ⇒-rhs is only used for its runtime value
+(check-type (nil {Int}) : (List Int) ⇒ (nil {Bool}))
+(check-not-type (nil {Bool}) : (List Int))
+(check-type (nil {Bool}) : (List Bool))
+(check-type (nil {(→ Int Int)}) : (List (→ Int Int)))
+(define fn-lst (cons (λ ([x : Int]) (+ 10 x)) (nil {(→ Int Int)})))
+(check-type fn-lst : (List (→ Int Int)))
+(check-type (isnil fn-lst) : Bool ⇒ #f)
+(typecheck-fail (isnil (head fn-lst))) ; head lst is not List
+(check-type (isnil (tail fn-lst)) : Bool ⇒ #t)
+(check-type (head fn-lst) : (→ Int Int))
+(check-type ((head fn-lst) 25) : Int ⇒ 35)
+(check-type (tail fn-lst) : (List (→ Int Int)) ⇒ (nil {(→ Int Int)}))
+
+;; previous tests: ------------------------------------------------------------
+;; define-type-alias
+(define-type-alias Integer Int)
+(define-type-alias ArithBinOp (→ Int Int Int))
+
+(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))
+
+(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]))
+
+
+(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 -----------------------------------------------------------
+; fail bc tuple changed syntax
+;(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)
+;; 2016-03-06: begin terms dont need to be Unit
+(check-type (begin 1 2 3) : Int)
+#;(typecheck-fail
+ (begin 1 2 3)
+ #:with-msg "Expected expression 1 to have Unit type, got: Int")
+(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+cons-tests.rkt b/macrotypes/examples/tests/stlc+cons-tests.rkt
new file mode 100644
index 0000000..d15d583
--- /dev/null
+++ b/macrotypes/examples/tests/stlc+cons-tests.rkt
@@ -0,0 +1,229 @@
+#lang s-exp "../stlc+cons.rkt"
+(require "rackunit-typechecking.rkt")
+
+(typecheck-fail (cons 1 2)
+                #:with-msg "expected \\(List Int\\), given Int\n *expression: 2")
+;(typecheck-fail (cons 1 nil)
+;                #:with-msg "nil: requires type annotation")
+(check-type (cons 1 nil) : (List Int))
+(check-type (cons 1 (nil {Int})) : (List Int))
+(typecheck-fail nil #:with-msg "nil: no expected type, add annotations")
+(typecheck-fail
+ (nil Int)
+ #:with-msg
+ "Improperly formatted type annotation: Int; should have shape {τ}, where τ is a valid type.")
+(typecheck-fail
+ (nil (Int))
+ #:with-msg
+ "Improperly formatted type annotation: \\(Int\\); should have shape {τ}, where τ is a valid type.")
+(typecheck-fail
+ (λ ([lst : (List Int Int)]) lst)
+ #:with-msg
+ "Improper usage of type constructor List: \\(List Int Int\\), expected = 1 arguments")
+(typecheck-fail
+ (λ ([lst : (List)]) lst)
+ #:with-msg
+ "Improper usage of type constructor List: \\(List\\), expected = 1 arguments")
+;; passes bc ⇒-rhs is only used for its runtime value
+(check-type (nil {Int}) : (List Int) ⇒ (nil {Bool}))
+(check-not-type (nil {Bool}) : (List Int))
+(check-type (nil {Bool}) : (List Bool))
+(check-type (nil {(→ Int Int)}) : (List (→ Int Int)))
+(define fn-lst (cons (λ ([x : Int]) (+ 10 x)) (nil {(→ Int Int)})))
+(check-type fn-lst : (List (→ Int Int)))
+(check-type (isnil fn-lst) : Bool ⇒ #f)
+(typecheck-fail
+ (isnil (head fn-lst))
+ #:with-msg
+ "Expected List type, got: \\(→ Int Int\\)")
+(check-type (isnil (tail fn-lst)) : Bool ⇒ #t)
+(check-type (head fn-lst) : (→ Int Int))
+(check-type ((head fn-lst) 25) : Int ⇒ 35)
+(check-type (tail fn-lst) : (List (→ Int Int)) ⇒ (nil {(→ Int Int)}))
+
+; more list errors
+(typecheck-fail
+ (cons 1 1)
+ #:with-msg
+ "expected \\(List Int\\), given Int\n *expression: 1")
+
+;; previous tests: ------------------------------------------------------------
+;; define-type-alias
+(define-type-alias Integer Int)
+(define-type-alias ArithBinOp (→ Int Int Int))
+
+(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]))
+
+
+(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 -----------------------------------------------------------
+; fail because changed tuple syntax
+;(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/stlc+effect-tests.rkt b/macrotypes/examples/tests/stlc+effect-tests.rkt
new file mode 100644
index 0000000..cff3907
--- /dev/null
+++ b/macrotypes/examples/tests/stlc+effect-tests.rkt
@@ -0,0 +1,245 @@
+#lang s-exp "../stlc+effect.rkt"
+(require "rackunit-typechecking.rkt")
+
+(check-props ν (ref 11) :  (88))
+(check-props ! (deref (ref 11)) :  (121))
+(check-props ν (deref (ref 11)) :  (170))
+(check-props ν ((λ ([x : Int]) (ref x)) 21) :  (221))
+             
+(define x (ref 10))
+(check-type x : (Ref Int))
+(check-type (deref x) : Int ⇒ 10)
+(check-type (:= x 20) : Unit) ; x still 10 because check-type does not evaluate
+(check-type (begin (:= x 20) (deref x)) : Int ⇒ 20)
+(check-type x : (Ref Int))
+(check-type (deref (ref 20)) : Int ⇒ 20)
+(check-type (deref x) : Int ⇒ 20)
+
+(check-type ((λ ([b : (Ref Int)]) (deref b)) (ref 10)) : Int ⇒ 10)
+(check-type ((λ ([x : Int]) x) ((λ ([b : (Ref Int)]) (deref b)) (ref 10))) : Int ⇒ 10)
+(check-type ((λ ([b : (Ref Int)]) (begin (begin (:= b 20) (deref b)))) (ref 10)) : Int ⇒ 20)
+
+;; Ref err msgs
+; wrong arity
+(typecheck-fail
+ (λ ([lst : (Ref Int Int)]) lst)
+ #:with-msg
+ "Improper usage of type constructor Ref: \\(Ref Int Int\\), expected = 1 arguments")
+(typecheck-fail
+ (λ ([lst : (Ref)]) lst)
+ #:with-msg
+ "Improper usage of type constructor Ref: \\(Ref\\), expected = 1 arguments")
+(typecheck-fail
+ (deref 1)
+ #:with-msg
+ "Expected Ref type, got: Int")
+(typecheck-fail
+ (:= 1 1)
+ #:with-msg
+ "Expected Ref type, got: Int")
+(typecheck-fail
+ (:= (ref 1) "hi")
+ #:with-msg
+ ":=: type mismatch: expected Int, given String\n *expression: \"hi\"")
+
+;; previous tests: ------------------------------------------------------------
+(typecheck-fail (cons 1 2))
+;(typecheck-fail (cons 1 nil)) ; works now
+(check-type (cons 1 nil) : (List Int))
+(check-type (cons 1 (nil {Int})) : (List Int))
+(typecheck-fail nil)
+(typecheck-fail (nil Int))
+(typecheck-fail (nil (Int)))
+; passes bc ⇒-rhs is only used for its runtime value
+(check-type (nil {Int}) : (List Int) ⇒ (nil {Bool}))
+(check-not-type (nil {Bool}) : (List Int))
+(check-type (nil {Bool}) : (List Bool))
+(check-type (nil {(→ Int Int)}) : (List (→ Int Int)))
+(define fn-lst (cons (λ ([x : Int]) (+ 10 x)) (nil {(→ Int Int)})))
+(check-type fn-lst : (List (→ Int Int)))
+(check-type (isnil fn-lst) : Bool ⇒ #f)
+(typecheck-fail (isnil (head fn-lst))) ; head lst is not List
+(check-type (isnil (tail fn-lst)) : Bool ⇒ #t)
+(check-type (head fn-lst) : (→ Int Int))
+(check-type ((head fn-lst) 25) : Int ⇒ 35)
+(check-type (tail fn-lst) : (List (→ Int Int)) ⇒ (nil {(→ Int Int)}))
+
+;; previous tests: ------------------------------------------------------------
+;; define-type-alias
+(define-type-alias Integer Int)
+(define-type-alias ArithBinOp (→ Int Int Int))
+
+(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))
+
+(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]))
+
+
+(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 -----------------------------------------------------------
+; fail bc tuple changed syntax
+;(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/stlc+lit-tests.rkt b/macrotypes/examples/tests/stlc+lit-tests.rkt
new file mode 100644
index 0000000..8eefb5c
--- /dev/null
+++ b/macrotypes/examples/tests/stlc+lit-tests.rkt
@@ -0,0 +1,62 @@
+#lang s-exp "../stlc+lit.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; thunk
+(check-type (λ () 1) : (→ Int))
+
+(check-type 1 : Int)
+(check-not-type 1 : (→ Int Int))
+
+(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)
+ #:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments")
+(typecheck-fail
+ (λ ([x : (→ →)]) x)
+ #:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments")
+(typecheck-fail
+ (λ ([x : (→)]) x)
+ #:with-msg "Improper usage of type constructor →: \\(→\\), expected >= 1 arguments")
+
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+
+(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
+ "Expected → type, got: Int")
+
+(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))
+ #:with-msg (string-append "expected: +Int, Int\n *given: +Int, \\(→ Int Int\\)\n"
+                           " *expressions: 1, \\(λ \\(\\(x : Int\\)\\) x\\)"))
+(typecheck-fail
+ (λ ([x : (→ Int Int)]) (+ x x))
+  #:with-msg "expected: +Int, Int\n *given: +\\(→ Int Int\\), \\(→ Int Int\\)\n *expressions: x, x")
+(typecheck-fail
+ ((λ ([x : Int] [y : Int]) y) 1)
+ #:with-msg "wrong number of arguments: expected 2, given 1")
+
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+
+(typecheck-fail (λ ([x : (→ 1 2)]) x) #:with-msg "not a valid type")
+(typecheck-fail (λ ([x : 1]) x) #:with-msg "not a valid type")
+(typecheck-fail (λ ([x : (+ 1 2)]) x) #:with-msg "not a valid type")
+(typecheck-fail (λ ([x : (λ ([y : Int]) y)]) x) #:with-msg "not a valid type")
+
diff --git a/macrotypes/examples/tests/stlc+overloading-tests.rkt b/macrotypes/examples/tests/stlc+overloading-tests.rkt
index f6b54dd..0400c9e 100644
--- a/macrotypes/examples/tests/stlc+overloading-tests.rkt
+++ b/macrotypes/examples/tests/stlc+overloading-tests.rkt
@@ -75,7 +75,7 @@
 
 (typecheck-fail
  ((resolve to-string Num) "hello")
- #:with-msg (expected "Num" #:given "Str"))
+ #:with-msg "expected: +Num\n *given: +Str\n *expressions: \"hello\"")
 
 ;; -- instances are type-checked. They must match
 (typecheck-fail
diff --git a/macrotypes/examples/tests/stlc+reco+var-tests.rkt b/macrotypes/examples/tests/stlc+reco+var-tests.rkt
new file mode 100644
index 0000000..8786199
--- /dev/null
+++ b/macrotypes/examples/tests/stlc+reco+var-tests.rkt
@@ -0,0 +1,232 @@
+#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) : (×))
+(check-type (tup [name = "Stephen"]) : (× [name : String]))
+(check-type (proj (tup [name = "Stephen"]) name) : String ⇒ "Stephen")
+(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]))
+
+;; record errors
+(typecheck-fail
+ (proj 1 "a")
+ #:with-msg
+ "expected identifier")
+(typecheck-fail
+ (proj 1 a)
+ #:with-msg
+ "Expected expression 1 to have × type, got: Int")
+
+;; 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])))
+ #:with-msg
+ "expected: +\\(∨ \\(coffee : Unit\\) \\(tea : Unit\\)\\)\n *given: +\\(∨ \\(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])
+ #:with-msg "wrong number of case clauses")
+(typecheck-fail
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+   [coffee x => 1]
+   [teaaaaaa x => 2])
+ #:with-msg "case clauses not exhaustive")
+(typecheck-fail
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+   [coffee x => 1]
+   [tea x => 2]
+   [coke x => 3])
+ #:with-msg "wrong number of case clauses")
+(typecheck-fail
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+   [coffee x => "1"]
+   [tea x => 2])
+ #:with-msg "branches have incompatible types: String and Int")
+(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)
+
+;; variant errors
+(typecheck-fail
+ (var name = "Steve" as Int)
+ #:with-msg
+ "Expected the expected type to be a ∨ type, got: Int")
+(typecheck-fail
+ (case 1 [racket x => 1])
+ #:with-msg
+ "Expected ∨ type, got: Int")
+(typecheck-fail
+ (λ ([x : (∨)]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
+(typecheck-fail
+ (λ ([x : (∨ 1)]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ 1\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
+(typecheck-fail
+ (λ ([x : (∨ [1 2])]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ \\(1 2\\)\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
+(typecheck-fail
+ (λ ([x : (∨ [a 2])]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ \\(a 2\\)\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
+(typecheck-fail
+ (λ ([x : (∨ [a Int])]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ \\(a Int\\)\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
+(typecheck-fail
+ (λ ([x : (∨ [1 : Int])]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ \\(1 : Int\\)\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
+(typecheck-fail
+ (λ ([x : (∨ [a : 1])]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ \\(a : 1\\)\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
+
+;; previous tuple tests: ------------------------------------------------------------
+;; wont work anymore
+;;(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/stlc+tup-tests.rkt b/macrotypes/examples/tests/stlc+tup-tests.rkt
new file mode 100644
index 0000000..2b3f90f
--- /dev/null
+++ b/macrotypes/examples/tests/stlc+tup-tests.rkt
@@ -0,0 +1,107 @@
+#lang s-exp "../stlc+tup.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; 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) -1) #:with-msg "expected exact-nonnegative-integer")
+(typecheck-fail (proj (tup 1 "2" #f) 3) #:with-msg "index too large")
+(typecheck-fail
+ (proj 1 2)
+ #:with-msg
+ "proj: 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-tests.rkt b/macrotypes/examples/tests/stlc-tests.rkt
new file mode 100644
index 0000000..2502b9e
--- /dev/null
+++ b/macrotypes/examples/tests/stlc-tests.rkt
@@ -0,0 +1,12 @@
+#lang s-exp "../stlc.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; cannot write any terms without base types, but can check some errors
+
+(typecheck-fail (λ ([x : Undef]) x) #:with-msg "Undef: unbound identifier")
+(typecheck-fail (λ ([x : →]) x)
+ #:with-msg "Improper usage of type constructor →.+expected >= 1 arguments")
+(typecheck-fail (λ ([x : (→)]) x)
+ #:with-msg "Improper usage of type constructor →.+expected >= 1 arguments")
+(typecheck-fail (λ ([x : (→ →)]) x)
+ #:with-msg "Improper usage of type constructor →.+expected >= 1 arguments")
\ No newline at end of file
diff --git a/macrotypes/type-constraints.rkt b/macrotypes/type-constraints.rkt
index 8c509b7..01b5c52 100644
--- a/macrotypes/type-constraints.rkt
+++ b/macrotypes/type-constraints.rkt
@@ -50,6 +50,9 @@
          (cons (list (lookup #'a substs) #'b)
                #'rst)
          orig-cs)]
+       [(and (identifier? #'b) (var? #'b) (free-identifier=? #'a #'b))
+        ;; #'a and #'b are equal, drop this constraint
+        (add-constraints/var? Xs var? substs #'rst orig-cs)]
        [else
         (define entry (occurs-check (list #'a #'b) orig-cs))
         (add-constraints/var?
diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt
index b36092a..1a46f53 100644
--- a/turnstile/examples/mlish.rkt
+++ b/turnstile/examples/mlish.rkt
@@ -118,7 +118,7 @@
     (format (string-append
              "Could not infer instantiation of polymorphic function ~s.\n"
              "  expected: ~a\n"
-             "  given: ~a")
+             "  given:    ~a")
             (syntax->datum (get-orig e_fn))
             (string-join (stx-map type->str expected-tys) ", ")
             (string-join (stx-map type->str given-tys) ", ")))
diff --git a/turnstile/examples/tests/stlc+box-tests.rkt b/turnstile/examples/tests/stlc+box-tests.rkt
index d7eda17..84f3c61 100644
--- a/turnstile/examples/tests/stlc+box-tests.rkt
+++ b/turnstile/examples/tests/stlc+box-tests.rkt
@@ -31,6 +31,10 @@
  (:= 1 1)
  #:with-msg
  "Expected Ref type, got: Int")
+(typecheck-fail
+ (:= (ref 1) "hi")
+ #:with-msg
+ ":=: type mismatch: expected Int, given String\n *expression: \"hi\"")
 
 ;; previous tests: ------------------------------------------------------------
 (typecheck-fail (cons 1 2))
diff --git a/turnstile/examples/tests/stlc+effect-tests.rkt b/turnstile/examples/tests/stlc+effect-tests.rkt
index a912e6b..1632bd9 100644
--- a/turnstile/examples/tests/stlc+effect-tests.rkt
+++ b/turnstile/examples/tests/stlc+effect-tests.rkt
@@ -37,6 +37,10 @@
  (:= 1 1)
  #:with-msg
  "Expected Ref type, got: Int")
+(typecheck-fail
+ (:= (ref 1) "hi")
+ #:with-msg
+ ":=: type mismatch: expected Int, given String\n *expression: \"hi\"")
 
 ;; previous tests: ------------------------------------------------------------
 (typecheck-fail (cons 1 2))