diff --git a/collects/tests/typed-scheme/fail/require-typed-wrong.ss b/collects/tests/typed-scheme/fail/require-typed-wrong.ss
new file mode 100644
index 00000000..d35a4f94
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/require-typed-wrong.ss
@@ -0,0 +1,15 @@
+#;
+(exn-pred ".*contract.*")
+#lang scheme/load
+
+(module m typed-scheme
+  (: x (Number -> Number))
+  (define (x n) (add1 n))
+  (provide x))
+
+(module n typed-scheme
+  (require (only-in 'm))
+  (require/typed 'm [x (String -> Number)])
+  (x "foo"))
+
+(require 'n)
diff --git a/collects/tests/typed-scheme/fail/untyped-srfi1.ss b/collects/tests/typed-scheme/fail/untyped-srfi1.ss
new file mode 100644
index 00000000..3a4ec74c
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/untyped-srfi1.ss
@@ -0,0 +1,7 @@
+#;
+(exn-pred ".*untyped identifier map.*" ".*srfi.*")
+#lang typed-scheme
+
+(require srfi/1)
+
+map
diff --git a/collects/tests/typed-scheme/succeed/cmdline.ss b/collects/tests/typed-scheme/succeed/cmdline.ss
new file mode 100644
index 00000000..61faa7b4
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/cmdline.ss
@@ -0,0 +1,38 @@
+#lang typed-scheme
+
+(require scheme/cmdline)
+
+(: version-str String)
+(define version-str "0.1")
+
+(current-command-line-arguments (vector "counter.mch"))
+
+(: verbose-mode (Parameter Boolean))
+(define verbose-mode (make-parameter #f))
+
+(: optimize-level (Parameter Integer))
+(define optimize-level (make-parameter 0))
+
+(: model-checking-mode (Parameter Any))
+(define model-checking-mode (make-parameter 'sat))
+
+(: file-to-model-check String)
+(define file-to-model-check
+ (command-line
+  #:program "eboc" ;; Should be name of executable
+  #:once-each
+  [("-v" "--verbose") "Compile with verbose messages"
+                      (verbose-mode #t)]
+  [("-m" "--mode") #{mode : String} "Mode to run the model checker on (sat, satbin)"
+                   (model-checking-mode (string-append mode))]
+  #:once-any
+  [("-o" "--optimize-1") "Compile with optimization level 1"
+                         (optimize-level 1)]
+  ["--optimize-2"        (; show help on separate lines
+                          "Compile with optimization level 2,"
+                          "which includes all of level 1")
+                         (optimize-level 2)]
+
+  #:args (#{filename : String}) ; expect one command-line argument: <filename>
+  ; return the argument as a filename to compile
+  filename))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/list-struct-sum.ss b/collects/tests/typed-scheme/succeed/list-struct-sum.ss
new file mode 100644
index 00000000..d448eac8
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/list-struct-sum.ss
@@ -0,0 +1,25 @@
+
+#lang typed-scheme
+(require scheme/list)
+
+(define-type-alias (ListOf X) (U Empty (Cons X)))
+(define-struct: Empty ())
+(define-struct: (X) Cons ((first : X) (rest : (ListOf X))))
+
+(: sum ((ListOf Number) -> Number))
+(define (sum alon)
+ (cond
+   [(Empty? alon) 0]
+   [else (+ (Cons-first alon)
+            (sum (Cons-rest alon)))]))
+
+
+(: sum2 ((ListOf Number) -> Number))
+(define (sum2 alon)
+ (cond
+   [(Empty? alon) 0]
+   [(Cons? alon) (+ (Cons-first alon)
+                    (sum2 (Cons-rest alon)))]))
+
+(sum (make-Cons 5 (make-Cons 3 (make-Cons 1 (make-Empty)))))
+(sum2 (make-Cons 5 (make-Cons 3 (make-Cons 1 (make-Empty)))))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/match-dots.ss b/collects/tests/typed-scheme/succeed/match-dots.ss
new file mode 100644
index 00000000..c8a526c5
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/match-dots.ss
@@ -0,0 +1,8 @@
+#lang typed-scheme
+
+(require scheme/match)
+
+(: parse-sexpr : Any -> Number)
+(define (parse-sexpr sexpr)
+  (match sexpr
+    [(list #{(? symbol? a) : (Listof Symbol)} ...) 1]))
diff --git a/collects/tests/typed-scheme/succeed/refinement-even.ss b/collects/tests/typed-scheme/succeed/refinement-even.ss
new file mode 100644
index 00000000..8d6d9693
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/refinement-even.ss
@@ -0,0 +1,15 @@
+#lang typed-scheme
+
+(declare-refinement even?)
+(define-type-alias Even (Refinement even?))
+
+(: x Integer)
+(define x 4)
+
+(: y Even)
+(define y (if (even? x) x (error 'bad)))
+
+(: f (Even -> String))
+(define (f e) (format "~a" e))
+
+(f y)
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/xfail/apply-map-bug.ss b/collects/tests/typed-scheme/xfail/apply-map-bug.ss
new file mode 100644
index 00000000..d08a5c2f
--- /dev/null
+++ b/collects/tests/typed-scheme/xfail/apply-map-bug.ss
@@ -0,0 +1,8 @@
+
+#lang typed-scheme
+
+(: add-lists ((Listof Number) (Listof Number) * -> (Listof Number)))
+(define (add-lists lst . lsts)
+ (apply map #{+ :: (Number Number * -> Number)} lst lsts))
+
+(add-lists '(1 2 3) '(4 5 6) '(7 8 9))
\ No newline at end of file
diff --git a/collects/typed-scheme/env/lexical-env.ss b/collects/typed-scheme/env/lexical-env.ss
index 07f8134c..b6133239 100644
--- a/collects/typed-scheme/env/lexical-env.ss
+++ b/collects/typed-scheme/env/lexical-env.ss
@@ -23,7 +23,7 @@
 
 ;; find the type of identifier i, looking first in the lexical env, then in the top-level env
 ;; identifer -> Type
-(define (lookup-type/lexical i [env (lexical-env)])
+(define (lookup-type/lexical i [env (lexical-env)] #:fail [fail #f])
   (lookup env i 
           (lambda (i) (lookup-type 
                        i (lambda () 
@@ -31,7 +31,7 @@
                                   =>
                                   (lambda (a)
                                     (-lst (substitute Univ (cdr a) (car a))))]
-                                 [else (lookup-fail i)]))))))
+                                 [else ((or fail lookup-fail) i)]))))))
 
 ;; refine the type of i in the lexical env
 ;; (identifier type -> type) identifier -> environment
@@ -41,7 +41,7 @@
   (define (update f k env)
     (parameterize
         ([current-orig-stx k])
-      (let* ([v (lookup-type/lexical k)]
+      (let* ([v (lookup-type/lexical k env #:fail (lambda _ Univ))]
              [new-v (f k v)]
              [new-env (extend env k new-v)])
         new-env)))
diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 3b6ce080..17e73dbf 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -9,7 +9,7 @@
  (only-in '#%kernel [apply kernel:apply])
  scheme/promise
  (only-in string-constants/private/only-once maybe-print-message)
- (only-in scheme/match/runtime match:error)
+ (only-in scheme/match/runtime match:error matchable? match-equality-test)
  (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym])))
 
 [raise (Univ . -> . (Un))]
@@ -146,6 +146,8 @@
        [(Sym B -Namespace (-> Univ)) Univ])]
 
 [match:error (Univ . -> . (Un))]
+[match-equality-test (-Param (Univ Univ . -> . Univ) (Univ Univ . -> . Univ))]
+[matchable? (make-pred-ty (Un -String -Bytes))]
 [display (cl-> [(Univ) -Void] [(Univ -Port) -Void])]
 [write   (cl-> [(Univ) -Void] [(Univ -Port) -Void])]
 [print   (cl-> [(Univ) -Void] [(Univ -Port) -Void])]
@@ -568,6 +570,9 @@
         (cl->*
          ((-lst a) . -> . (-lst a))
          ((-lst a) (a a . -> . Univ) . -> . (-lst a))))]
+[append-map
+ (-polydots (c a b) ((list ((list a) (b b) . ->... . (-lst c)) (-lst a))
+                     ((-lst b) b) . ->... .(-lst c)))]
 
 ;; scheme/tcp
 [tcp-listener? (make-pred-ty -TCP-Listener)]
diff --git a/collects/typed-scheme/typecheck/tc-app-unit.ss b/collects/typed-scheme/typecheck/tc-app-unit.ss
index 63db7660..e0a64c4c 100644
--- a/collects/typed-scheme/typecheck/tc-app-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-app-unit.ss
@@ -21,7 +21,7 @@
           (only-in scheme/private/class-internal make-object do-make-object)))
 (require (r:infer constraint-structs))
 
-(import tc-expr^ tc-lambda^ tc-dots^)
+(import tc-expr^ tc-lambda^ tc-dots^ tc-let^)
 (export tc-app^)
 
 ;; comparators that inform the type system
@@ -779,6 +779,13 @@
          (match-let* ([ft (tc-expr #'f)]
                       [(tc-result: t) (tc/funapp #'f #'(arg) ft (list (ret ty)) #f)])
            (ret (Un (-val #f) t)))))]
+    ;; infer for ((lambda
+    [(#%plain-app (#%plain-lambda (x ...) . body) args ...)
+     (= (length (syntax->list #'(x ...)))
+        (length (syntax->list #'(args ...))))
+     (tc/let-values/check #'((x) ...) #'(args ...) #'body 
+                          #'(let-values ([(x) args] ...) . body)
+                          expected)]
     ;; default case
     [(#%plain-app f args ...) 
      (tc/funapp #'f #'(args ...) (tc-expr #'f) (map tc-expr (syntax->list #'(args ...))) expected)]))
@@ -804,7 +811,11 @@
        (ret expected))]
     ;; special case when argument needs inference
     [_
-     (let ([ts (map (compose generalize tc-expr/t) (syntax->list actuals))])
+     (let ([ts (for/list ([ac (syntax->list actuals)]
+                          [f (syntax->list args)])
+                 (or 
+                  (type-annotation f #:infer #t)
+                  (generalize (tc-expr/t ac))))])
        (tc/rec-lambda/check form args body lp ts expected)
        (ret expected))]))