diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
new file mode 100644
index 0000000..a3769a0
--- /dev/null
+++ b/tapl/mlish.rkt
@@ -0,0 +1,164 @@
+#lang s-exp "typecheck.rkt"
+(require (for-syntax syntax/id-set))
+
+(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let
+          #:rename [~→ ~ext-stlc:→])
+(require (only-in "sysf.rkt" inst ~∀ ∀ Λ))
+(require (only-in "stlc+rec-iso.rkt" case fld unfld μ × ∨ var tup define-type-alias)
+         (prefix-in stlc+rec-iso: (only-in "stlc+rec-iso.rkt" define)))
+;(reuse cons [head hd] [tail tl] nil [isnil nil?] List ~List list #:from "stlc+cons.rkt")
+;(reuse tup × proj #:from "stlc+tup.rkt")
+;(reuse define-type-alias #:from "stlc+reco+var.rkt")
+;(provide hd tl nil?)
+(provide (rename-out [lifted→ →]))
+(provide define-type match)
+(provide (rename-out [ext-stlc:let let]))
+
+;; ML-like language with no type inference
+
+;; type inference constraint solving
+(begin-for-syntax 
+  (define (compute-constraint τ1-τ2)
+    (syntax-parse τ1-τ2
+      [(X:id τ) #'((X τ))]
+      [((~Any τ1 ...) (~Any τ2 ...))
+       (compute-constraints #'((τ1 τ2) ...))]
+      ; should only be monomorphic?
+      [((~∀ () (~ext-stlc:→ τ1 ...)) (~∀ () (~ext-stlc:→ τ2 ...)))
+       (compute-constraints #'((τ1 τ2) ...))]
+      [_ #:when (displayln τ1-τ2) #'()]))
+  (define (compute-constraints τs)
+    ;(printf "constraints: ~a\n" (syntax->datum τs))
+    (stx-appendmap compute-constraint τs))
+
+  (define (solve-constraint x-τ)
+    (syntax-parse x-τ
+      [(X:id τ) #'((X τ))]
+      [_ #'()]))
+  (define (solve-constraints cs)
+    (stx-appendmap compute-constraint cs))
+  
+  (define (lookup x substs)
+    (syntax-parse substs
+      [((y:id τ) . rst)
+       #:when (free-identifier=? #'y x)
+       #'τ]
+      [(_ . rst) (lookup x #'rst)]
+      [() false])))
+
+(define-type-constructor Tmp #:arity >= 0 #:bvs >= 0) ; need a >= 0 arity
+
+(define-syntax (define-type stx)
+  (syntax-parse stx
+    [(_ (Name:id X:id ...)
+        ;; constructors must have the form (Cons τ ...)
+        ;; but the first ~or clause accepts 0-arg constructors as ids
+        ;; the ~and is required to bind the duplicate Cons ids (see Ryan's email)
+        (~and (~or (~and IdCons:id (~parse (Cons τ ...) #'(IdCons)))
+                   (Cons τ ...))) ...)
+     #:with (StructName ...) (generate-temporaries #'(Cons ...))
+     #:with ((e_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
+     #:with ((e_arg- ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
+     #:with ((τ_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
+     #:with ((fld ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
+     #:with ((acc ...) ...) (stx-map (λ (S fs) (stx-map (λ (f) (format-id S "~a-~a" S f)) fs))
+                                     #'(StructName ...) #'((fld ...) ...))
+     #`(begin
+         (define-type-constructor Name
+           #:arity = #,(stx-length #'(X ...))
+           #:other-prop variants #'(X ...) #'((Cons τ ...) ...))
+         (struct StructName (fld ...) #:reflection-name 'Cons #:transparent) ...
+         (define-syntax (Cons stx)
+           (syntax-parse stx
+             [C:id #:when (and (stx-null? #'(X ...)) (stx-null? #'(τ ...))) #'(C)]
+             [_:id
+              #:when (and (not (stx-null? #'(X ...)))
+                          (not (stx-null? #'(τ ...))))
+              (type-error
+               #:src stx
+               #:msg
+               (string-append
+                (format "constructor ~a must instantiate ~a type argument(s): "
+                        'Cons (stx-length #'(X ...)))
+                (string-join (stx-map type->str #'(X ...)) ", ")
+                "\n"
+                (format "and be applied to ~a arguments with type(s): "(stx-length #'(τ ...)))
+                (string-join (stx-map type->str #'(τ ...)) ", ")))]
+             [(_ τs e_arg ...)
+              #:when (brace? #'τs) ; commit
+              #:with {~! τ_X:type (... ...)} #'τs
+              #:with ([e_arg- τ_arg] ...) (stx-map infer+erase #'(e_arg ...))
+              #:with (τ_in:type (... ...))
+                     (stx-map (λ (t) (substs #'(τ_X.norm (... ...)) #'(X ...) t)) #'(τ ...))
+              #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in.norm (... ...)))
+                            ;; need to duplicate #%app err msg here, to attach additional props
+                            (string-append
+                             (format "~a (~a:~a) Arguments to constructor ~a have wrong type(s), "
+                                     (syntax-source stx) (syntax-line stx) (syntax-column stx)
+                                     'Cons)
+                             "or wrong number of arguments:\nGiven:\n"
+                             (string-join
+                              (map (λ (e t) (format "  ~a : ~a" e t)) ; indent each line
+                                   (syntax->datum #'(e_arg ...))
+                                   (stx-map type->str #'(τ_arg ...)))
+                              "\n" #:after-last "\n")
+                             (format "Expected: ~a arguments with type(s): "
+                                     (stx-length #'(τ_in (... ...))))
+                             (string-join (stx-map type->str #'(τ_in (... ...))) ", "))
+              #:with τ_out (syntax-property
+                            (syntax-property #'(Name τ_X (... ...)) 'constructor #'Cons)
+                            'accessors
+                            #'(acc ...))
+              (⊢ (StructName e_arg- ...) : τ_out)]
+             [(C . args) #:when (stx-null? #'(X ...)) #'(C {} . args)] ; no tyvars, no annotations
+             [(C . args) ; no type annotations, must infer instantiation
+              #:with ([arg- τarg] (... ...)) (infers+erase #'args)
+              #:with (~Tmp Ys τ+ (... ...)) ((current-type-eval) #'(Tmp (X ...) τ ...))
+              #:with cs (compute-constraints #'((τ+ τarg) (... ...)))
+              #:with (τ_solved (... ...)) (stx-map (λ (y) (lookup y #'cs)) #'Ys)
+              #'(C {τ_solved (... ...)} . args)]))
+         ...)]))
+
+(define-syntax (match stx)
+  (syntax-parse stx #:datum-literals (with ->)
+    [(_ e with . clauses)
+     #:fail-when (null? (syntax->list #'clauses)) "no clauses"
+     #:with ([Clause:id x ... -> e_c] ...) (stx-sort #'clauses symbol<?)
+     #:with [e- τ_e] (infer+erase #'e)
+     #:with ((Cons τ ...) ...) (stx-sort (syntax-property #'τ_e 'variants) symbol<?)
+     #:fail-unless (= (stx-length #'(Clause ...)) (stx-length #'(Cons ...))) "wrong number of case clauses"
+     #:fail-unless (typechecks? #'(Clause ...) #'(Cons ...)) "case clauses not exhaustive"
+     #:with (((x- ...) e_c- τ_ec) ...)
+            (stx-map (λ (bs e) (infer/ctx+erase bs e)) #'(([x : τ] ...) ...) #'(e_c ...))
+     #:fail-unless (same-types? #'(τ_ec ...)) "branches have different types"
+     #:with C (syntax-property #'τ_e 'constructor)
+     #:with (_ (x_out ...) e_out τ_out) (stx-assoc #'C #'((Clause (x- ...) e_c- τ_ec) ...))
+     #:with (acc ...) (syntax-property #'τ_e 'accessors)
+     (⊢ (let ([x_out (acc e-)] ...) e_out) : τ_out)]))
+
+(define-syntax lifted→ ; wrap → with ∀
+  (syntax-parser
+    [(_ . rst) #'(∀ () (ext-stlc:→ . rst))]))
+
+(define-primop + : (lifted→ Int Int Int))
+(define-primop - : (lifted→ Int Int Int))
+(define-primop void : (lifted→ Unit))
+(define-primop = : (lifted→ Int Int Bool))
+(define-primop zero? : (lifted→ Int Bool))
+(define-primop sub1 : (lifted→ Int Int))
+(define-primop add1 : (lifted→ Int Int))
+(define-primop not : (lifted→ Bool Bool))
+(define-primop abs : (lifted→ Int Int))
+
+
+; all λs have type (∀ (X ...) (→ τ_in ... τ_out))
+(define-typed-syntax liftedλ #:export-as λ #:datum-literals (:)
+  [(_ . rst)
+   #'(Λ () (ext-stlc:λ . rst))])
+
+(define-typed-syntax new-app #:export-as #%app
+  [(_ τs f . args)
+   #:when (brace? #'τs)
+   #'(ext-stlc:#%app (inst f . τs) . args)]
+  [(_ f . args)
+   #'(ext-stlc:#%app (inst f) . args)])
diff --git a/tapl/notes.txt b/tapl/notes.txt
index d69fd0f..47247b2 100644
--- a/tapl/notes.txt
+++ b/tapl/notes.txt
@@ -1,3 +1,13 @@
+2016-02-19
+Implementing algebraic data types
+- macro cannot define type-alias and constructor functions that produce
+  variant values
+  - not only because adts should be an abstraction (ie not type alias)
+  - constructor output will have variant type and not the type defined
+- macro should basically expand to list implementation in stlc+cons.rkt
+ - where to store the names of the variants (as stx prop?)
+
+
 2015-10-09
 TODO: variant case should call current-join?
 
diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt
index d2851f4..b4a16fb 100644
--- a/tapl/stlc+lit.rkt
+++ b/tapl/stlc+lit.rkt
@@ -21,6 +21,9 @@
      #:with op/tc (generate-temporary #'op)
      #'(begin
          (provide (rename-out [op/tc op]))
+         (define-primop op/tc op : τ))]
+    [(_ op/tc op : τ)
+     #'(begin
          #;(define-syntax op/tc (make-rename-transformer (assign-type #'op #'τ)))
          ; rename transformer doesnt seem to expand at the right time
          ; - op still has no type in #%app
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
index 4788a60..b0b7a31 100644
--- a/tapl/stlc.rkt
+++ b/tapl/stlc.rkt
@@ -80,7 +80,7 @@
                  (string-append
                   (format "~a (~a:~a) Arguments to function ~a have wrong type(s), "
                           (syntax-source stx) (syntax-line stx) (syntax-column stx)
-                          (syntax->datum #'e_fn))
+                          (syntax->datum #'e_fn-))
                   "or wrong number of arguments:\nGiven:\n"
                   (string-join
                    (map (λ (e t) (format "  ~a : ~a" e t)) ; indent each line
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
index 6238219..15ec98d 100644
--- a/tapl/stx-utils.rkt
+++ b/tapl/stx-utils.rkt
@@ -39,8 +39,12 @@
 (define (stx-str=? s1 s2)
   (string=? (syntax-e s1) (syntax-e s2)))
 
-(define (stx-sort stx cmp)
-  (sort (syntax->list stx) (λ (stx1 stx2) (cmp (syntax-e (stx-car stx1)) (syntax-e (stx-car stx2))))))
+(define (stx-sort stx cmp #:key [key-fn (λ (x) x)])
+  (sort
+   (syntax->list stx)
+   (λ (stx1 stx2)
+     (cmp (syntax-e (stx-car stx1)) (syntax-e (stx-car stx2))))
+   #:key key-fn))
 
 (define (stx-fold f base . lsts)
   (apply foldl f base (map syntax->list lsts)))
diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt
index 33d1332..21c2f96 100644
--- a/tapl/sysf.rkt
+++ b/tapl/sysf.rkt
@@ -21,4 +21,9 @@
 (define-typed-syntax inst
   [(_ e τ:type ...)
    #:with (e- (tvs (τ_body))) (⇑ e as ∀)
-   (⊢ e- : #,(substs #'(τ.norm ...) #'tvs #'τ_body))])
\ No newline at end of file
+   ;#:with [e- (~and t (~∀ tvs τ_body))] (infer+erase #'e)
+   ;#:with (_ Xs τ_orig) (get-orig #'t) ; doesnt work with implicit lifted→
+   ;#:with new-orig (substs #'(τ ...) #'Xs #'τ_orig)
+   ;(⊢ e- : #,(add-orig (substs #'(τ.norm ...) #'tvs #'τ_body) #'new-orig))]
+   (⊢ e- : #,(substs #'(τ.norm ...) #'tvs #'τ_body))]
+  [(_ e) #'e])
\ No newline at end of file
diff --git a/tapl/tests/ext-stlc-tests.rkt b/tapl/tests/ext-stlc-tests.rkt
index d96543f..3757ab5 100644
--- a/tapl/tests/ext-stlc-tests.rkt
+++ b/tapl/tests/ext-stlc-tests.rkt
@@ -29,7 +29,7 @@
 (typecheck-fail (begin) #:with-msg "expected more terms")
 (typecheck-fail
  (begin 1 2 3)
- #:with-msg "Expected expression \"1\" to have Unit type, got: Int")
+ #: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)
diff --git a/tapl/tests/infer-tests.rkt b/tapl/tests/infer-tests.rkt
index 1bcf632..3a87a1a 100644
--- a/tapl/tests/infer-tests.rkt
+++ b/tapl/tests/infer-tests.rkt
@@ -223,7 +223,7 @@
 (typecheck-fail (begin) #:with-msg "expected more terms")
 (typecheck-fail
  (begin 1 2 3)
- #:with-msg "Expected expression \"1\" to have Unit type, got: Int")
+ #: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)
diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt
new file mode 100644
index 0000000..ccfa93d
--- /dev/null
+++ b/tapl/tests/mlish-tests.rkt
@@ -0,0 +1,224 @@
+#lang s-exp "../mlish.rkt"
+(require "rackunit-typechecking.rkt")
+
+(define-type (IntList)
+  INil
+  (ConsI Int (IntList)))
+
+(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]))
+
+(define-type (List X)
+  (Nil)
+  (Cons X (List X)))
+(check-type (Nil {Int}) : (List Int))
+(check-type (Cons 1 (Nil {Int})) : (List Int))
+(check-type (Cons 1 (Cons 2 (Nil {Int}))) : (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 (Cons 1 (Nil {Bool}))
+                #:with-msg "wrong type\\(s\\)")
+(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 {Int})) with
+   [Nil -> 3]
+   [Cons y ys -> (+ y 4)])
+ : Int ⇒ 5)
+            
+(check-type
+ (match (Cons 1 (Nil {Int})) with
+   [Cons y ys -> (+ y 5)]
+   [Nil -> 3])
+ : Int ⇒ 6)
+            
+
+; 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
+ "Arguments to function.+have wrong type.+Given:.+Int.+Expected:.+Unit")
+(typecheck-fail
+ ((λ ([x : Unit]) x) void)
+  #:with-msg
+ "Arguments to function.+have wrong type.+Given:.+(→ Unit).+Expected:.+Unit")
+
+(check-type ((λ ([x : Unit]) x) (void)) : Unit)
+
+;; begin
+(check-type (begin 1) : Int)
+
+(typecheck-fail (begin) #:with-msg "expected more terms")
+(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: 1 does not have type Bool")
+;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")
+
+; 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
+ "Arguments to function \\+.+have wrong type.+Given:.+Bool.+Int.+Expected:.+Int.+Int")
+(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
+ "Arguments to function \\+.+have wrong type.+Given:.+Bool.+Int.+Expected:.+Int.+Int")
+
+; letrec
+(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")
+(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")
+
+(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 "Expected expression \"1\" to have Bool type, got: String")
+(typecheck-fail
+ (and #t "2")
+ #:with-msg
+ "Expected expression \"2\" to have Bool type, got: String")
+(typecheck-fail
+ (or "1" #f)
+ #:with-msg
+ "Expected expression \"1\" to have Bool type, got: String")
+(typecheck-fail
+ (or #t "2")
+ #:with-msg
+ "Expected expression \"2\" to have Bool type, got: String")
+(typecheck-fail
+ (if "true" 1 2)
+ #:with-msg
+ "Expected expression \"true\" to have Bool type, got: String")
+(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
+ "Arguments to function.+have wrong type.+Given:.+Int.+Expected:.+Bool")
+;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
+(typecheck-fail
+ (λ ([f : Int]) (f 1 2))
+ #:with-msg
+ "Expected expression f to have → 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
+ "Arguments to function \\+ have wrong type.+Given:\n  1 : Int.+(→ Int Int).+Expected: 2 arguments with type.+Int\\, Int")
+(typecheck-fail
+ (λ ([x : (→ Int Int)]) (+ x x))
+  #:with-msg
+ "Arguments to function \\+ have wrong type.+Given:.+(→ Int Int).+Expected: 2 arguments with type.+Int\\, Int")
+(typecheck-fail
+ ((λ ([x : Int] [y : Int]) y) 1)
+ #:with-msg "Arguments to function.+have.+wrong number of arguments")
+
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index 075e4c5..7263cf6 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -2,8 +2,8 @@
 (require
   (for-syntax (except-in racket extends)
               syntax/parse racket/syntax syntax/stx racket/stxparam
-              "stx-utils.rkt"
-              syntax/parse/debug)
+              syntax/parse/debug
+              "stx-utils.rkt")
   (for-meta 2 racket/base syntax/parse racket/syntax syntax/stx "stx-utils.rkt")
   (for-meta 3 racket/base syntax/parse racket/syntax)
   racket/bool racket/provide racket/require)
@@ -12,7 +12,8 @@
  (except-out (all-from-out racket/base) #%module-begin)
  (for-syntax (all-defined-out)) (all-defined-out)
  (for-syntax
-  (all-from-out racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt"))
+  (all-from-out racket syntax/parse racket/syntax syntax/stx
+                "stx-utils.rkt"))
  (for-meta 2 (all-from-out racket/base syntax/parse racket/syntax)))
 
 ;; type checking functions/forms
@@ -154,6 +155,8 @@
     (define ty (syntax-property stx tag))
     (if (cons? ty) (car ty) ty))
 
+  (define type-pat "[A-Za-z]+")
+  
   ;; - infers type of e
   ;; - checks that type of e matches the specified type
   ;; - erases types in e
@@ -165,14 +168,34 @@
        #:with τ? (mk-? #'tycon)
        #:with τ-get (format-id #'tycon "~a-get" #'tycon)
        #:with τ-expander (format-id #'tycon "~~~a" #'tycon)
-       #'(syntax-parse (infer+erase #'e) #:context #'e
+       #'(syntax-parse
+             ;; when type error, prefer outer err msg
+             (with-handlers ([exn:fail?
+                              (λ (ex)
+                                (define matched-ty
+                                  (regexp-match
+                                   (pregexp
+                                    (string-append "got\\:\\s(" type-pat ")"))
+                                   (exn-message ex)))
+                                (unless matched-ty
+                                  (raise ex (current-continuation-marks)))
+                                (define t-in-msg
+                                  (datum->syntax #'here
+                                    (string->symbol
+                                     (cadr matched-ty))))
+                                  (list #'e t-in-msg))])
+               (infer+erase #'e))
+           #:context #'e
            [(e- τ_e_)
             #:with τ_e ((current-promote) #'τ_e_)
             #:fail-unless (τ? #'τ_e)
             (format
              "~a (~a:~a): Expected expression ~s to have ~a type, got: ~a"
              (syntax-source #'e) (syntax-line #'e) (syntax-column #'e)
-             (syntax->datum #'e) 'tycon (type->str #'τ_e))
+             (syntax-parse #'e-
+               ['x (syntax-e #'x)]
+               [_ (syntax->datum #'e-)])
+             'tycon (type->str #'τ_e))
             #;(if (stx-pair? #'τ_e)
                 (syntax-parse #'τ_e
                  [(τ-expander . args) #'(e- args)])
@@ -193,8 +216,11 @@
                     (λ (e t)
                       (or (τ? t)
                           (type-error #:src e
-                                      #:msg "Expected expression ~s to have ~a type, got: ~a"
-                                      e (quote-syntax tycon) t)))
+                                      #:msg
+                                      (string-append
+                                       (format "Expected expression ~s" (syntax->datum e))
+                                       " to have ~a type, got: ~a")
+                                      (quote-syntax tycon) t)))
                     #'es
                     #'(τ_e (... ...)))
             ;#:with args (τ-get #'τ_e)
@@ -430,7 +456,10 @@
          (~seq #:bvs (~and (~parse has-bvs? #'#t) bvs-op) bvs-n:exact-nonnegative-integer)
          #:defaults ([bvs-op #'=][bvs-n #'0]))
         (~optional (~seq #:arr (~and (~parse has-annotations? #'#t) tycon))
-         #:defaults ([tycon #'void])))
+         #:defaults ([tycon #'void]))
+        (~optional (~seq #:other-prop other-key other-bvs other-val)
+                   #:defaults ([other-key #'#f]))
+        )
      #:with #%kind (format-id #'kind "#%~a" #'kind)
      #:with τ-internal (generate-temporary #'τ)
      #:with τ? (mk-? #'τ)
@@ -509,7 +538,11 @@
                #:with k_result (if #,(attribute has-annotations?)
                                    #'(tycon k_arg (... ...))
                                    #'#%kind)
-               (assign-type #'(τ-internal (λ bvs- void . τs-)) #'k_result)]
+               #:with result
+                (assign-type (syntax/loc stx (τ-internal (λ bvs- void . τs-))) #'k_result)
+                #,(if (syntax-e #'other-key)
+                    #`(syntax-property #'result 'other-key (substs #'args #,#'other-bvs #,#'other-val))
+                    #'#'result)]
              ;; else fail with err msg
              [_
               (type-error #:src stx
@@ -612,6 +645,12 @@
 
 ; substitution
 (begin-for-syntax
+  (define-syntax ~Any ; matches any tycon
+    (pattern-expander
+     (syntax-parser
+       [(_ x ...)
+        #'((~literal #%plain-app) _
+            ((~literal #%plain-lambda) bvs (~literal void) x ...))])))
   (define (merge-type-tags stx)
     (define t (syntax-property stx 'type))
     (or (and (pair? t)