From d32218ad15935c9636df38b5851ca40e2e8d90aa Mon Sep 17 00:00:00 2001
From: Andrew Kent <andmkent@iu.edu>
Date: Fri, 10 Nov 2017 17:38:57 -0500
Subject: [PATCH] have `inst` use Any as default type for omitted args

In addition to potentially being convenient, this helps us not
break backwards compatibility when APIs add features that require
additional type variables to properly type.
---
 .../scribblings/reference/special-forms.scrbl | 24 ++++++++++++++-----
 .../typed-racket/typecheck/tc-expression.rkt  |  7 +++---
 typed-racket-lib/typed-racket/types/utils.rkt |  6 +++--
 typed-racket-lib/typed-racket/utils/utils.rkt |  6 ++++-
 .../unit-tests/typecheck-tests.rkt            |  8 +++----
 5 files changed, 35 insertions(+), 16 deletions(-)

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=?