diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
index 2b5675f..58862ba 100644
--- a/tapl/ext-stlc.rkt
+++ b/tapl/ext-stlc.rkt
@@ -39,18 +39,23 @@
    (⊢ (and e1- e2-) : Bool)])
   
 (define-typed-syntax or
-  [(_ e1 e2)
-   #:with e1- (⇑ e1 as Bool)
-   #:with e2- (⇑ e2 as Bool)
-   (⊢ (or e1- e2-) : Bool)])
+  [(_ e ...)
+   #:with (e- ...) (⇑s (e ...) as Bool)
+;   #:with e1- (⇑ e1 as Bool)
+;   #:with e2- (⇑ e2 as Bool)
+;   (⊢ (or e1- e2-) : Bool)])
+   (⊢ (or e- ...) : Bool)])
 
 (begin-for-syntax 
   (define current-join (make-parameter (λ (x y) x))))
 (define-typed-syntax if
-  [(_ e_tst e1 e2)
+  [(~and ifstx (_ e_tst e1 e2))
+   #:with τ-expected (get-expected-type #'ifstx)
    #:with e_tst- (⇑ e_tst as Bool)
-   #:with (e1- τ1) (infer+erase #'e1)
-   #:with (e2- τ2) (infer+erase #'e2)
+   #: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)
    #:fail-unless (and (typecheck? #'τ1 #'τ-out)
                       (typecheck? #'τ2 #'τ-out))
diff --git a/tapl/infer.rkt b/tapl/infer.rkt
index 543b312..14343ef 100644
--- a/tapl/infer.rkt
+++ b/tapl/infer.rkt
@@ -2,7 +2,10 @@
 (extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not
          #:rename [~→ ~ext-stlc:→])
 (reuse ∀ ~∀ ∀? Λ #:from "sysf.rkt")
-(reuse cons head tail nil isnil List #:from "stlc+cons.rkt")
+(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 →)
 
 ;; a language with partial (local) type inference using bidirectional type checking
@@ -22,7 +25,36 @@
 (define-primop sub1 : (→ Int Int))
 (define-primop add1 : (→ Int Int))
 (define-primop not : (→ Bool Bool))
-                  
+(define-primop abs : (→ Int Int))
+
+(begin-for-syntax 
+  (define (compute-constraint τ1-τ2)
+    (syntax-parse τ1-τ2
+      [(X:id τ) #'((X τ))]
+      [((~List τ1) (~List τ2)) (compute-constraint #'(τ1 τ2))]
+      ; should only be monomorphic?
+      [((~∀ () (~ext-stlc:→ τ1 ...)) (~∀ () (~ext-stlc:→ τ2 ...)))
+       (compute-constraints #'((τ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-typed-syntax define
   [(_ x:id e)
    #:with (e- τ) (infer+erase #'e)
@@ -33,14 +65,16 @@
   [(_ (~and Xs {X:id ...}) (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
    #:when (brace? #'Xs)
    #:with g (generate-temporary)
+   #:with e_ann #'(add-expected e τ_out)
    #'(begin
        (define-syntax f (make-rename-transformer (⊢ g : (∀ (X ...) (ext-stlc:→ τ ... τ_out)))))
-       (define g (Λ (X ...) (ext-stlc:λ ([x : τ] ...) e))))]
+       (define g (Λ (X ...) (ext-stlc:λ ([x : τ] ...) e_ann))))]
   [(_ (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
    #:with g (generate-temporary)
+   #:with e_ann #'(add-expected e τ_out)
    #'(begin
        (define-syntax f (make-rename-transformer (⊢ g : (→ τ ... τ_out))))
-       (define g (ext-stlc:λ ([x : τ] ...) e)))])
+       (define g (ext-stlc:λ ([x : τ] ...) e_ann)))])
 
 ; all λs have type (∀ (X ...) (→ τ_in ... τ_out))
 (define-typed-syntax λ #:datum-literals (:)
@@ -57,18 +91,86 @@
    (⊢ λ- : (∀ () τ_λ))])
 
 (define-typed-syntax #%app
-  [(_ e_fn e_arg ...)
-   #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
+  [(_ e_fn e_arg ...) ; infer args first
+   #:with maybe-inferred-τs (with-handlers ([exn:fail:type:infer? (λ _ #f)])
+                                 (infers+erase #'(e_arg ...)))
+   #:when (syntax-e #'maybe-inferred-τs)
+   #:with ([e_arg- τ_arg] ...) #'maybe-inferred-τs
    #:with e_fn_anno (syntax-property #'e_fn 'given-τ-args #'(τ_arg ...))
 ;   #:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn_anno as →)
-   #:with [e_fn- ((X ...) ((~ext-stlc:→ τ_in ... τ_out)))] (⇑ e_fn_anno as ∀)
+   #:with [e_fn- ((X ...) ((~ext-stlc:→ τ_inX ... τ_outX)))] (⇑ e_fn_anno as ∀)
+   #:fail-unless (stx-length=? #'(τ_inX ...) #'(e_arg ...)) ; check arity
+                 (string-append
+                  (format "~a (~a:~a) Wrong number of arguments given to function ~a.\n"
+                          (syntax-source stx) (syntax-line stx) (syntax-column stx)
+                          (syntax->datum #'e_fn))
+                  (format "Expected: ~a arguments with types: "
+                          (stx-length #'(τ_inX ...)))
+                  (string-join (stx-map type->str #'(τ_inX ...)) ", " #:after-last "\n")
+                  "Given:\n"
+                  (string-join
+                   (map (λ (e t) (format "  ~a : ~a" e t)) ; indent each line
+                        (syntax->datum #'(e_arg ...))
+                        (stx-map type->str #'(τ_arg ...)))
+                   "\n"))
+   #:with cs (compute-constraints #'((τ_inX τ_arg) ...))
+   #:with (τ_solved ...) (stx-map (λ (y) (lookup y #'cs)) #'(X ...))
+   #:with (τ_in ... τ_out) (stx-map (λ (t) (substs #'(τ_solved ...) #'(X ...) t)) #'(τ_inX ... τ_outX))
    ; some code duplication
    #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
                  (string-append
-                  (format "~a (~a:~a) Arguments to function ~a have wrong type(s), "
+                  (format "~a (~a:~a) Arguments to function ~a have wrong type(s).\n"
                           (syntax-source stx) (syntax-line stx) (syntax-column stx)
                           (syntax->datum #'e_fn))
-                  "or wrong number of arguments:\nGiven:\n"
+                  "Given:\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 ...)) ", "))
+  (⊢ (#%app e_fn- e_arg- ...) : τ_out)]
+  [(_ e_fn e_arg ...) ; infer fn first ------------------------- ; TODO: remove code dup
+   #:with [e_fn- ((X ...) ((~ext-stlc:→ τ_inX ... τ_outX)))] (⇑ e_fn as ∀)
+   #:fail-unless (stx-length=? #'(τ_inX ...) #'(e_arg ...)) ; check arity
+                 (string-append
+                  (format "~a (~a:~a) Wrong number of arguments given to function ~a.\n"
+                          (syntax-source stx) (syntax-line stx) (syntax-column stx)
+                          (syntax->datum #'e_fn))
+                  (format "Expected: ~a arguments with types: "
+                          (stx-length #'(τ_inX ...)))
+                  (string-join (stx-map type->str #'(τ_inX ...)) ", " #:after-last "\n")
+                  "Given args: "
+                  (string-join (map ~a (syntax->datum #'(e_arg ...))) ", "))
+;   #:with ([e_arg- τ_arg] ...) #'(infers+erase #'(e_arg ...))
+   #:with (cs ([e_arg- τ_arg] ...))
+          (let-values ([(cs e+τs)
+          (for/fold ([cs #'()] [e+τs #'()])
+                    ([e_arg (syntax->list #'(e_arg ...))]
+                     [τ_inX (syntax->list #'(τ_inX ...))])
+            (define/with-syntax τs_solved (stx-map (λ (y) (lookup y cs)) #'(X ...)))
+            (cond
+              [(andmap syntax-e (syntax->list #'τs_solved)) ; all tyvars X have mapping
+               (define e+τ (infer+erase #`(add-expected #,e_arg #,(substs #'τs_solved #'(X ...) τ_inX))))
+               (values cs (cons e+τ e+τs))]
+              [else
+               (define/with-syntax [e τ] (infer+erase e_arg))
+               (define/with-syntax (c ...) cs)
+               (define/with-syntax (new-c ...) (compute-constraint #`(#,τ_inX τ)))
+               (values #'(new-c ... c ...) (cons #'[e τ] e+τs))]))])
+            (define/with-syntax e+τs/stx e+τs)
+            (list cs (reverse (syntax->list #'e+τs/stx))))
+   #:with (τ_solved ...) (stx-map (λ (y) (lookup y #'cs)) #'(X ...))
+   #:with (τ_in ... τ_out) (stx-map (λ (t) (substs #'(τ_solved ...) #'(X ...) t)) #'(τ_inX ... τ_outX))
+   ; some code duplication
+   #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
+                 (string-append
+                  (format "~a (~a:~a) Arguments to function ~a have wrong type(s).\n"
+                          (syntax-source stx) (syntax-line stx) (syntax-column stx)
+                          (syntax->datum #'e_fn))
+                  "Given:\n"
                   (string-join
                    (map (λ (e t) (format "  ~a : ~a" e t)) ; indent each line
                         (syntax->datum #'(e_arg ...))
diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt
index 73f3e80..0fcf5d7 100644
--- a/tapl/stlc+cons.rkt
+++ b/tapl/stlc+cons.rkt
@@ -12,17 +12,29 @@
 
 (define-type-constructor List)
 
-(define-typed-syntax nil
-  [(_ ~! τi:type-ann) (⊢ null : (List τi.norm))]
+(define-typed-syntax nil/tc #:export-as nil
+  [(~and ni (_ ~! τi:type-ann))
+   (⊢ null : (List τi.norm))]
   ; minimal type inference
-  [ni:id #:with τ (syntax-property #'ni 'type) #:when (syntax-e #'τ) (⊢ null : (List τ))] 
-  [_:id #:fail-when #t (error 'nil "requires type annotation") #'(void)])
-(define-typed-syntax cons
+  [ni:id #:with expected-τ (get-expected-type #'ni)
+         #:when (syntax-e #'expected-τ) ; 'expected-type property exists (ie, not false)
+         #:with (~List τ) (local-expand #'expected-τ 'expression null) ; canonicalize
+         (⊢ 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)])
+(define-typed-syntax cons/tc #:export-as cons
   [(_ e1 e2)
    #:with [e1- τ1] (infer+erase #'e1)
-   #:with e2+ (syntax-property #'e2 'type #'τ1)
-   #:with (e2- (τ2)) (⇑ e2+ as List)
-   #:when (typecheck? #'τ1 #'τ2)
+;   #: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)))
    (⊢ (cons e1- e2-) : (List τ1))])
 (define-typed-syntax isnil
   [(_ e)
@@ -36,4 +48,7 @@
   [(_ e)
    #:with (e- τ-lst) (infer+erase #'e)
    #:when (List? #'τ-lst)
-   (⊢ (cdr e-) : τ-lst)])
\ No newline at end of file
+   (⊢ (cdr e-) : τ-lst)])
+(define-typed-syntax list/tc #:export-as list
+  [(_) #'nil/tc]
+  [(_ x . rst) #'(cons/tc x (list/tc . rst))])
\ No newline at end of file
diff --git a/tapl/stlc+occurrence.rkt b/tapl/stlc+occurrence.rkt
index 85dec4f..66365e4 100644
--- a/tapl/stlc+occurrence.rkt
+++ b/tapl/stlc+occurrence.rkt
@@ -1,6 +1,6 @@
 #lang s-exp "typecheck.rkt"
 (extends "stlc+sub.rkt" #:except #%datum)
-(extends "stlc+cons.rkt" #:except + #%datum and tup × proj ~×)
+(extends "stlc+cons.rkt" #:except + #%datum and tup × proj ~× list)
 (reuse tup × proj ~× #:from "stlc+tup.rkt")
 
 ;; Calculus for occurrence typing.
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
index d3061c3..6238219 100644
--- a/tapl/stx-utils.rkt
+++ b/tapl/stx-utils.rkt
@@ -11,7 +11,7 @@
   (apply ormap f (map syntax->list stx-lsts)))
 
 (define (stx-flatten stxs)
-  (apply append (stx-map syntax->list stxs)))
+  (apply append (stx-map (λ (stx) (if (syntax? stx) (syntax->list stx) stx)) stxs)))
 
 (define (curly-parens? stx)
   (define paren-prop (syntax-property stx 'paren-shape))
@@ -48,6 +48,8 @@
 (define (stx-append stx1 stx2)
   (append (if (syntax? stx1) (syntax->list stx1) stx1)
           (if (syntax? stx2) (syntax->list stx2) stx2)))
+(define (stx-appendmap f stx)
+  (stx-flatten (stx-map f stx)))
 
 ;; based on make-variable-like-transformer from syntax/transformer,
 ;; but using (#%app id ...) instead of ((#%expression id) ...)
diff --git a/tapl/tests/ext-stlc-tests.rkt b/tapl/tests/ext-stlc-tests.rkt
index 3757ab5..d96543f 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 10cb43b..8082e3f 100644
--- a/tapl/tests/infer-tests.rkt
+++ b/tapl/tests/infer-tests.rkt
@@ -25,6 +25,110 @@
 (define {X} (g [x : X] → X) x)
 (check-type g : (→ {X} 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 {X} (g2 [lst : (List X)] → (List X)) lst)
+(check-type g2 : (→ {X} (List X) (List X)))
+(typecheck-fail (g2 1) #:with-msg "Expected.+arguments with type.+List") ; TODO: more precise err msg
+(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))}))
+(check-type (g2 (cons 1 nil)) : (List Int) ⇒ (cons 1 nil))
+(check-type (g2 (cons "1" nil)) : (List String) ⇒ (cons "1" nil))
+
+(define {X} (g3 [lst : (List X)] → X) (hd lst))
+(check-type g3 : (→ {X} (List X) X))
+(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 "Arguments.+have wrong type")
+
+; 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\\)")
+
+
+(define {X Y} (map [f : (→ X Y)] [lst : (List X)] → (List Y))
+  (if (nil? lst)
+      nil ; test expected-type propagation of if and define
+      ; recursive call should instantiate to "concrete" X and Y types
+      (cons (f (hd lst)) (map f (tl lst)))))
+
+; nil without annotation tests fn-first, left-to-right arg inference (2nd #%app case)
+(check-type (map add1 nil) : (List Int) ⇒ (nil {Int}))
+(check-type (map add1 (list)) : (List Int) ⇒ (nil {Int}))
+(check-type (map add1 (list 1 2 3)) : (List Int) ⇒ (list 2 3 4))
+(typecheck-fail (map add1 (list "1")) #:with-msg "Arguments.+have wrong type")
+(check-type (map (λ ([x : Int]) (+ x 2)) (list 1 2 3)) : (List Int) ⇒ (list 3 4 5))
+; doesnt work yet
+;(map (λ (x) (+ x 2)) (list 1 2 3))
+
+(define {X} (filter [p? : (→ X Bool)] [lst : (List X)] → (List X))
+  (if (nil? lst)
+      nil
+      (if (p? (hd lst))
+          (cons (hd lst) (filter p? (tl lst)))
+          (filter p? (tl lst)))))
+(define {X} (filter/let [p? : (→ X Bool)] [lst : (List X)] → (List X))
+  (if (nil? lst)
+      nil
+      (let ([x (hd lst)] [filtered-rst (filter p? (tl lst))])
+        (if (p? x) (cons x filtered-rst) filtered-rst))))
+
+(check-type (filter zero? nil) : (List Int) ⇒ (nil {Int}))
+(check-type (filter zero? (list 1 2 3)) : (List Int) ⇒ (nil {Int}))
+(check-type (filter zero? (list 0 1 2)) : (List Int) ⇒ (list 0))
+(check-type (filter (λ ([x : Int]) (not (zero? x))) (list 0 1 2)) : (List Int) ⇒ (list 1 2))
+
+(define {X Y} (foldr [f : (→ X Y Y)] [base : Y] [lst : (List X)] → Y)
+  (if (nil? lst)
+      base
+      (f (hd lst) (foldr f base (tl lst)))))
+(define {X Y} (foldl [f : (→ X Y Y)] [acc : Y] [lst : (List X)] → Y)
+  (if (nil? lst)
+      acc
+      (foldr f (f (hd lst) acc) (tl lst))))
+
+(define {X} (all? [p? : (→ X Bool)] [lst : (List X)] → Bool)
+  (if (nil? lst)
+      #t
+      (and (p? (hd lst)) (all? p? (tl lst)))))
+  
+; nqueens
+(define-type-alias Queen (× Int Int))
+(define (q-x [q : Queen] → Int) (proj q 0))
+(define (q-y [q : Queen] → Int) (proj q 1))
+
+(define (safe? [q1 : Queen] [q2 : Queen] → Bool)
+  (let ([x1 (q-x q1)][y1 (q-y q1)]
+        [x2 (q-x q2)][y2 (q-y q2)])
+    (not (or (= x1 x2) (= y1 y2) (= (abs (- x1 x2)) (abs (- y1 y2)))))))
+(define (safe/list? [qs : (List Queen)] → Bool)
+  (if (nil? qs)
+      #t
+      (let ([q1 (hd qs)])
+        (all? (λ ([q2 : Queen]) (safe? q1 q2)) (tl qs)))))
+
 ; --------------------------------------------------
 ; all ext-stlc tests should still pass (copied below):
 ;; tests for stlc extensions
@@ -55,7 +159,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)
@@ -186,7 +290,7 @@
  "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")
+ #:with-msg "Wrong number of arguments")
 
 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
 
diff --git a/tapl/tests/stlc+cons-tests.rkt b/tapl/tests/stlc+cons-tests.rkt
index 14f5316..18746b7 100644
--- a/tapl/tests/stlc+cons-tests.rkt
+++ b/tapl/tests/stlc+cons-tests.rkt
@@ -7,7 +7,7 @@
 ;                #: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: requires type annotation")
+(typecheck-fail nil #:with-msg "nil requires type annotation")
 (typecheck-fail
  (nil Int)
  #:with-msg
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index bddf242..94ee5eb 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -52,7 +52,7 @@
          (provide (rename-out [name out-name]))
          (define-syntax (name syntx)
            (syntax-parameterize ([stx (syntax-id-rules () [_ syntx])])
-             (syntax-parse syntx stx-parse-clause ...))))]
+             (syntax-parse syntx #:context #'out-name stx-parse-clause ...))))]
     [(_ name:id stx-parse-clause ...)
      #`(define-typed-syntax #,(generate-temporary) #:export-as name
          stx-parse-clause ...)]))
@@ -117,6 +117,9 @@
                      (λ (n) (and (not (member n excluded)) n)))
                    (all-from-out base-lang))))]))
 
+(define-syntax add-expected
+  (syntax-parser [(_ e τ) (syntax-property #'e 'expected-type #'τ)]))
+
 ;; type assignment
 (begin-for-syntax
   ;; Type assignment macro for nicer syntax
@@ -133,6 +136,11 @@
   ;;   which didnt get marked bc they were syntax properties
   (define (assign-type e τ #:tag [tag 'type])
     (syntax-property e tag (syntax-local-introduce ((current-type-eval) τ))))
+
+  (define (add-expected-type e τ)
+    (syntax-property e 'expected-type τ)) ; dont type-eval?, ie expand?
+  (define (get-expected-type e)
+    (syntax-property e 'expected-type))
   
   ;; typeof : Syntax -> Type or #f
   ;; Retrieves type of given stx, or #f if input has not been assigned a type.
@@ -179,7 +187,7 @@
                     (λ (e t)
                       (or (τ? t)
                           (type-error #:src e
-                                      #:msg "Expected expression ~a to have ~a type, got: ~a"
+                                      #:msg "Expected expression ~s to have ~a type, got: ~a"
                                       e (quote-syntax tycon) t)))
                     #'es
                     #'(τ_e (... ...)))
@@ -300,6 +308,7 @@
     (local-expand e 'expression null))
 
   (struct exn:fail:type:check exn:fail:user ())
+  (struct exn:fail:type:infer exn:fail:user ())
 
   ;; type-error #:src Syntax #:msg String Syntax ...
   ;; usage: