diff --git a/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl b/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl
index 47665ba7..e639d37b 100644
--- a/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl
+++ b/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl
@@ -555,14 +555,25 @@ protect higher-order uses of the value.
 Instantiate the type of @racket[e] with types @racket[t ...] or with the
 poly-dotted types @racket[t ... t ooo bound]. @racket[e] must
 have a polymorphic type that can be applied to the supplied number of type
-variables. This is legal only in expression contexts.
+variables. For non-poly-dotted functions, however, fewer arguments can be
+  provided and the omitted types default to @racket[Any].
+  @racket[inst] is legal only in expression contexts.
 @ex[(foldl (inst cons Integer Integer) null (list 1 2 3 4))
 
-    (: fold-list : (All (A) (Listof A) -> (Listof A)))
-    (define (fold-list lst)
-      (foldl (inst cons A A) null lst))
+    (: my-cons (All (A B) (-> A B (Pairof A B))))
+    (define my-cons cons)
 
-    (fold-list (list "1" "2" "3" "4"))
+    (: foldl-list : (All (α) (Listof α) -> (Listof α)))
+    (define (foldl-list lst)
+      (foldl (inst my-cons α (Listof α)) null lst))
+
+    (foldl-list (list "1" "2" "3" "4"))
+
+    (: foldr-list : (All (α) (Listof α) -> Any))
+    (define (foldr-list lst)
+      (foldr (inst my-cons α) null lst))
+
+    (foldr-list (list "1" "2" "3" "4"))
 
     (: my-values : (All (A B ...) (A B ... -> (values A B ... B))))
     (define (my-values arg . args)
@@ -683,7 +694,8 @@ a @racket[require/typed] form. Here is an example of using
 so we need to use @racket[case->].
 
 @history[#:changed "1.4" @elem{Added the @racket[#:type-name] option.}
-         #:changed "1.6" "Added syntax for struct type variables, only works in unsafe requires"]}
+         #:changed "1.6" "Added syntax for struct type variables, only works in unsafe requires."
+         #:changed "1.12" @elem{Added default type @racket[Any] for omitted @racket[inst] args.}]}
 
 @defform[(require/typed/provide m rt-clause ...)]{
 Similar to @racket[require/typed], but also provides the imported identifiers.
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-expression.rkt b/typed-racket-lib/typed-racket/typecheck/tc-expression.rkt
index 830b3050..808201ed 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-expression.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-expression.rkt
@@ -77,11 +77,12 @@
      (tc-error/expr #:return -Bottom "Cannot instantiate non-polymorphic type ~a"
                     (cleanup-type ty))]
     [(and (Poly? ty)
-          (not (= (syntax-length inst) (Poly-n ty))))
+          (> (syntax-length inst) (Poly-n ty)))
      (tc-error/expr #:return -Bottom
-                    "Wrong number of type arguments to polymorphic type ~a:\nexpected: ~a\ngot: ~a"
+                    "Too many type arguments to polymorphic type ~a:\nexpected ~a or fewer\ngot: ~a"
                     (cleanup-type ty) (Poly-n ty) (syntax-length inst))]
-    [(and (PolyDots? ty) (not (>= (syntax-length inst) (sub1 (PolyDots-n ty)))))
+    [(and (PolyDots? ty)
+          (not (>= (syntax-length inst) (sub1 (PolyDots-n ty)))))
      ;; we can provide 0 arguments for the ... var
      (tc-error/expr #:return -Bottom
                     "Wrong number of type arguments to polymorphic type ~a:\nexpected at least: ~a\ngot: ~a"
diff --git a/typed-racket-lib/typed-racket/types/utils.rkt b/typed-racket-lib/typed-racket/types/utils.rkt
index b25f1f07..a648df35 100644
--- a/typed-racket-lib/typed-racket/types/utils.rkt
+++ b/typed-racket-lib/typed-racket/types/utils.rkt
@@ -17,10 +17,12 @@
 (define (instantiate-poly t types)
   (match t
     [(Poly: ns body)
-     (unless (= (length types) (length ns))
+     (unless (<= (length types) (length ns))
        (int-err "instantiate-poly: wrong number of types: expected ~a, got ~a"
                 (length ns) (length types)))
-     (subst-all (make-simple-substitution ns types) body)]
+     ;; use Any as the default type for any omitted types
+     (subst-all (make-simple-substitution ns (list-extend ns types Univ))
+                body)]
     [(PolyDots: (list fixed ... dotted) body)
      (unless (>= (length types) (length fixed))
        (int-err
diff --git a/typed-racket-lib/typed-racket/utils/utils.rkt b/typed-racket-lib/typed-racket/utils/utils.rkt
index 68114034..621268c5 100644
--- a/typed-racket-lib/typed-racket/utils/utils.rkt
+++ b/typed-racket-lib/typed-racket/utils/utils.rkt
@@ -246,7 +246,11 @@ at least theoretically.
 ;; Listof[A] Listof[B] B -> Listof[B]
 ;; pads out t to be as long as s
 (define (list-extend s t extra)
-  (append t (build-list (max 0 (- (length s) (length t))) (lambda _ extra))))
+  (define s-len (length s))
+  (define t-len (length t))
+  (cond
+    [(<= s-len t-len) t]
+    [else (append t (build-list (- s-len t-len) (λ _ extra)))]))
 
 ;; does l1 end with l2?
 ;; e.g. (list 1 2 3) ends with (list 2 3)
diff --git a/typed-racket-test/unit-tests/typecheck-tests.rkt b/typed-racket-test/unit-tests/typecheck-tests.rkt
index 709ae7e8..8170614e 100644
--- a/typed-racket-test/unit-tests/typecheck-tests.rkt
+++ b/typed-racket-test/unit-tests/typecheck-tests.rkt
@@ -1440,10 +1440,10 @@
         [tc-e (remf* symbol? '(a b c)) (-lst (one-of/c 'a 'b 'c))]
         [tc-e (check-duplicates '("a" "a" "b")) (-opt -String)]
         [tc-e (check-duplicates '("a" "a" "b") string=?) (-opt -String)]
-        ;[tc-e ((inst check-duplicates String Number)
-        ;       '("a" "aa" "aaa")
-        ;       #:key string-length)
-        ;      (-opt -String)]
+        [tc-e ((inst check-duplicates String Number)
+               '("a" "aa" "aaa")
+               #:key string-length)
+              (-opt -String)]
         [tc-e ((inst check-duplicates String Any 'nope)
                '("a" "a" "b")
                string=?