fix optional and rest arg reasoning (#618)

typed-racket-lib/typed-racket/env/init-envs.rkt

@@ -194,15 +194,15 @@
              ,(type->sexp t)
              (list ,@(map path-elem->sexp pth)))]
     [(Fun: (? has-optional-args? arrs))
-     (match-define (Arrow: fdoms rest *kws rng) (first arrs))
-     (match-define (Arrow: ldoms _ _ _) (last arrs))
+     (match-define (Arrow: fdoms _ kws rng) (first arrs))
+     (match-define (Arrow: ldoms rst _ _) (last arrs))
      (define opts (drop ldoms (length fdoms)))
-     (define kws (map type->sexp *kws))
-     `(opt-fn (list ,@(map type->sexp fdoms))
-              (list ,@(map type->sexp opts))
-              ,(type->sexp rng)
-              ,@(if rest `(#:rest ,rest) '())
-              ,@(if (null? kws) '() `(#:kws (list ,@kws))))]
+     `(opt-fn
+       (list ,@(map type->sexp fdoms))
+       (list ,@(map type->sexp opts))
+       ,(type->sexp rng)
+       ,@(if rst `(#:rest ,(type->sexp rst)) '())
+       ,@(if (null? kws) '() `(#:kws (list ,@(map type->sexp kws)))))]
     [(Fun: arrs) `(make-Fun (list ,@(map type->sexp arrs)))]
     [(DepFun: dom pre rng)
      `(make-DepFun (list ,@(map type->sexp dom))

typed-racket-lib/typed-racket/private/type-contract.rkt

@@ -782,21 +782,24 @@
      (define (partition-kws kws) (partition (match-lambda [(Keyword: _ _ mand?) mand?]) kws))
      (define (process-dom dom*)  (if method? (cons any/sc dom*) dom*))
      (cond
-      ;; To generate a single `->*', everything must be the same for all arrs, except for positional
-      ;; arguments which can increase by at most one each time.
-      ;; Note: optional arguments can only increase by 1 each time, to avoid problems with
-      ;;  functions that take, e.g., either 2 or 6 arguments. These functions shouldn't match,
-      ;;  since this code would generate contracts that accept any number of arguments between
-      ;;  2 and 6, which is wrong.
-      ;; TODO sufficient condition, but may not be necessary
-      [(has-optional-args? arrows)
-       (define first-arrow (first arrows))
+       ;; To generate a single `->*':
+       ;; - keywords and range must be the same for all arrows
+       ;; - only the last arrow may have a rest argument
+       ;; - positional argument count increases by one at each step
+       ;; Note: optional arguments can only increase by 1 each time, to avoid problems with
+       ;;  functions that take, e.g., either 2 or 6 arguments. These functions shouldn't match,
+       ;;  since this code would generate contracts that accept any number of arguments between
+       ;;  2 and 6, which is wrong.
+       ;; TODO sufficient condition, but may not be necessary
+       [(has-optional-args? arrows)
+        (define first-arrow (first arrows))
        (define last-arrow (last arrows))
        (define (convert-arrow)
-         (match-define (Arrow: first-dom rst kws
+         (match-define (Arrow: first-dom _ kws
                                (Values: (list (Result: rngs _ _) ...)))
            first-arrow)
-         ;; all but dom is the same for all arrs
+         (define rst (Arrow-rst last-arrow))
+         ;; kws and rng same for all arrs
          (define last-dom (Arrow-dom last-arrow))
          (define mand-args (map t->sc/neg first-dom))
          (define opt-args (map t->sc/neg (drop last-dom (length first-dom))))

typed-racket-lib/typed-racket/rep/type-rep.rkt

@@ -549,6 +549,14 @@
    (for-each f kws)
    (f rng)])
 
+(define/provide (Arrow-min-arity a)
+  (length (Arrow-dom a)))
+
+(define/provide (Arrow-max-arity a)
+  (if (Type? (Arrow-rst a))
+      +inf.0
+      (length (Arrow-dom a))))
+
 ;; a standard function
 ;; + all functions are case-> under the hood (i.e. see 'arrows')
 ;; + each Arrow in 'arrows' may have a dependent range

typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt

@@ -2,7 +2,7 @@
 
 (require "../utils/utils.rkt"
          racket/list syntax/parse syntax/stx
-         racket/match syntax/id-table racket/set
+         racket/match syntax/private/id-table racket/set
          racket/sequence
          (contract-req)
          (rep type-rep object-rep rep-utils)
@@ -55,39 +55,41 @@
 ;; tc-lambda-body: Typechecks the body with the given args and names and returns the resulting arr?.
 ;; arg-names: The identifiers of the positional args
 ;; arg-types: The types of the positional args
-;; raw-rest: Either #f for no rest argument or (list rest-id rest-type) where rest-id is the
-;;           identifier of the rest arg, and rest-type is the type.
+;; rest-arg+type: Either #f for no rest argument or (cons rest-id rest-type)
+;;                where rest-id is the identifier of the rest arg,
+;;                and (ListOf rest-type) is the type that identifier would
+;;                have in the function body
 ;; expected: The expected type of the body forms.
 ;; body: The body of the lambda to typecheck.
 (define/cond-contract
-  (tc-lambda-body arg-names arg-types #:rest [raw-rest #f] #:expected [expected #f] body)
+  (tc-lambda-body arg-names arg-types #:rest-arg+type [rest-arg+type #f] #:expected [expected #f] body)
   (->* ((listof identifier?) (listof Type?) syntax?)
-       (#:rest (or/c #f (list/c identifier? (or/c Type? RestDots?)))
+       (#:rest-arg+type (or/c #f (cons/c identifier? (or/c Type? RestDots?)))
         #:expected (or/c #f tc-results/c))
        Arrow?)
-  (define-values (rest-id rst)
-    (if raw-rest
-        (values (first raw-rest) (second raw-rest))
-        (values #f #f)))
 
-  (define rest-types
-    (match rst
-      [(? Type?) (list (-lst rst))]
-      [(RestDots: dty dbound)
-       (list (make-ListDots dty dbound))]
-      [#f (list)]))
-  (define rest-names
-    (if rest-id (list rest-id) null))
+  (define-values (rst-id rst-type names types)
+    (match rest-arg+type
+      [(cons id rst)
+       (values id rst
+               (cons id arg-names)
+               (cons (match rst
+                       [(? Bottom?) -Null]
+                       [(? Type?) (-lst rst)]
+                       [(RestDots: dty dbound)
+                        (make-ListDots dty dbound)])
+                     arg-types))]
+      [_ (values #f #f arg-names arg-types)]))
 
   (-Arrow
    arg-types
    (abstract-results
     (with-extended-lexical-env
-        [#:identifiers (append rest-names arg-names)
-         #:types (append rest-types arg-types)]
+        [#:identifiers names
+         #:types types]
       (tc-body/check body expected))
-    arg-names #:rest-id rest-id)
-   #:rest rst))
+    arg-names #:rest-id rst-id)
+   #:rest rst-type))
 
 ;; check-clause: Checks that a lambda clause has arguments and body matching the expected type
 ;; arg-list: The identifiers of the positional args in the lambda form
@@ -138,15 +140,15 @@
            (cond
              [(type-annotation rest-id) (get-type rest-id #:default Univ)]
              [(Type? rst) rst]
+             [(not rst) -Bottom]
              [else Univ]))
          (define extra-types
            (if (<= arg-len tys-len)
                (drop arg-tys arg-len)
                null))
          (apply Un base-rest-type extra-types)]))
-
     (tc-lambda-body arg-list arg-types
-                    #:rest (and rest-type (list rest-id rest-type))
+                    #:rest-arg+type (and rest-type (cons rest-id rest-type))
                     #:expected ret-ty
                     body)))
 
@@ -265,7 +267,7 @@
       [else
        (list
         (tc-lambda-body arg-list (map (lambda (v) (or v Univ)) arg-types)
-                        #:rest (and rest-type (list rest-id rest-type))
+                        #:rest-arg+type (and rest-type (cons rest-id rest-type))
                         body))])]))
 
 
@@ -364,11 +366,12 @@
       [_ #f]))
 
 
-  ;; For each clause we figure out which arrs it needs to typecheck as, and also which clauses are
-  ;; dead code.
+  ;; For each clause we figure out which arrs it needs to typecheck as,
+  ;; and also which clauses are dead code.
   (define-values (used-formals+bodies+arrs arities-seen)
-    (for/fold ((formals+bodies+arrs* empty) (arities-seen initial-arities-seen))
-              ((formal+body formals+bodies))
+    (for/fold ([formals+bodies+arrs* empty]
+               [arities-seen initial-arities-seen])
+              ([formal+body (in-list formals+bodies)])
       (match formal+body
         [(list formal body)
          (define arity (formals->arity formal))
@@ -385,27 +388,29 @@
              formals+bodies+arrs*)
            (arities-seen-add arities-seen arity))])))
 
-  (if (and
-        (andmap (λ (f-b-arr) (empty? (third f-b-arr))) used-formals+bodies+arrs)
-        ;; If the empty function is expected, then don't error out
-        (match expected-type
-          [(Fun: (list)) #f]
-          [_ #t]))
-      ;; TODO improve error message.
-      (tc-error/expr #:return (list (-Arrow null -Bottom #:rest Univ))
-                     "Expected a function of type ~a, but got a function with the wrong arity"
-                     expected-type)
-      (apply append
-             (for/list ([fb* (in-list used-formals+bodies+arrs)])
-               (match-define (list f* b* t*) fb*)
-               (cond
-                 [(not t*) (tc/lambda-clause f* b*)]
-                 [else
-                  (for/list ([arrow (in-list t*)])
-                    (match arrow
-                      [(Arrow: dom rst '() rng)
-                       (tc/lambda-clause/check
-                        f* b* dom (values->tc-results rng (formals->objects f*)) rst)]))])))))
+  (cond
+    [(and (andmap (λ (f-b-arr) (empty? (third f-b-arr)))
+                  used-formals+bodies+arrs)
+          ;; If the empty function is expected, then don't error out
+          (match expected-type
+            [(Fun: (list)) #f]
+            [_ #t]))
+     ;; TODO improve error message.
+     (tc-error/expr #:return (list (-Arrow null -Bottom #:rest Univ))
+                    "Expected a function of type ~a, but got a function with the wrong arity"
+                    expected-type)]
+    [else
+     (apply append
+            (for/list ([fb* (in-list used-formals+bodies+arrs)])
+              (match-define (list f* b* t*) fb*)
+              (cond
+                [(not t*) (tc/lambda-clause f* b*)]
+                [else
+                 (for/list ([arrow (in-list t*)])
+                   (match arrow
+                     [(Arrow: dom rst '() rng)
+                      (tc/lambda-clause/check
+                       f* b* dom (values->tc-results rng (formals->objects f*)) rst)]))])))]))
 
 (define (tc/dep-lambda formalss-stx bodies-stx dep-fun-ty)
   (parameterize ([with-refinements? #t])

typed-racket-lib/typed-racket/types/abbrev.rkt

@@ -168,8 +168,9 @@
 (define (opt-fn args opt-args result #:rest [rest #f] #:kws [kws null])
   (apply cl->* (for/list ([i (in-range (add1 (length opt-args)))])
                  (make-Fun (list (-Arrow (append args (take opt-args i))
-                                         result
-                                         #:rest rest #:kws kws))))))
+                                         result ;; only the LAST arrow gets the rest arg
+                                         #:rest (and (= i (length opt-args)) rest)
+                                         #:kws kws))))))
 
 (define-syntax-rule (->opt args ... [opt ...] res)
   (opt-fn (list args ...) (list opt ...) res))

typed-racket-lib/typed-racket/types/base-abbrev.rkt

@@ -235,7 +235,9 @@
        (with-syntax ([((extra ...) ...)
                       (for/list ([i (in-range (add1 (length l)))])
                         (take l i))]
-                     [(rst ...) (for/list ([i (in-range (add1 (length l)))]) #'rst)])
+                     ;; only the LAST arrow gets a #:rest arg
+                     [(rst ...) (for/list ([i (in-range (add1 (length l)))])
+                                  (if (< i (length l)) #'#f #'rst))])
          (syntax/loc stx
            (make-Fun
             (list

typed-racket-lib/typed-racket/types/kw-types.rkt

@@ -9,54 +9,58 @@
          racket/format racket/string
          syntax/parse)
 
-;; convert : [Listof Keyword] [Listof Type] [Listof Type] [Option Type]
-;;           [Option Type] [Option (Pair Type symbol)] boolean -> Type
-(define (convert kw-ts plain-ts opt-ts rng rst split?)
-  (when (RestDots? rst) (int-err "RestDots passed to kw-convert"))
+
+(define (convert keywords ; (listof Keyword?)
+                 mandatory-arg-types ; (listof Type?)
+                 optional-arg-types ; (listof Type?)
+                 rng ; SomeValues?
+                 maybe-rst ; (or/c #f Type? RestDots?)
+                 split?) ; boolean?
+  (when (RestDots? maybe-rst) (int-err "RestDots passed to kw-convert"))
   ;; the kw function protocol passes rest args as an explicit list
-  (define rst-type (if rst (list (-lst rst)) empty))
+  (define rst-type (if maybe-rst (list (-lst maybe-rst)) empty))
 
   ;; the kw protocol puts the arguments in keyword-sorted order in the
   ;; function header, so we need to sort the types to match
   (define sorted-kws
-    (sort kw-ts (λ (kw1 kw2) (keyword<? (Keyword-kw kw1)
-                                       (Keyword-kw kw2)))))
+    (sort keywords (λ (kw1 kw2) (keyword<? (Keyword-kw kw1)
+                                           (Keyword-kw kw2)))))
 
   (make-Fun
-    (cond
-      [(not split?)
-       (define ts 
-         (flatten
-          (list
-           (for/list ([k (in-list sorted-kws)])
-             (match k
-               [(Keyword: _ t #t) t]
-               [(Keyword: _ t #f) (list (-opt t) -Boolean)]))
-           plain-ts
-           (for/list ([t (in-list opt-ts)]) (-opt t))
-           (for/list ([t (in-list opt-ts)]) -Boolean)
-           rst-type)))
-       (list (-Arrow ts rng #:rest rst))]
-      [else
-       ;; The keyword argument types including boolean flags for
-       ;; optional keyword arguments
-       (define kw-args
-         (for/fold ([pos '()])
-                   ([k (in-list (reverse sorted-kws))])
-           (match k
-             ;; mandatory keyword arguments have no extra args
-             [(Keyword: _ t #t) (cons t pos)]
-             ;; we can safely assume 't' and not (-opt t) here
-             ;; because if the keyword is not provided, the value
-             ;; will only appear in dead code (i.e. where the kw-flag arg is #f)
-             ;; within the body of the function
-             [(Keyword: _ t #f) (list* t -Boolean pos)])))
+   (cond
+     [(not split?)
+      (define ts
+        (flatten
+         (list
+          (for/list ([k (in-list sorted-kws)])
+            (match k
+              [(Keyword: _ t #t) t]
+              [(Keyword: _ t #f) (list (-opt t) -Boolean)]))
+          mandatory-arg-types
+          (for/list ([t (in-list optional-arg-types)]) (-opt t))
+          (for/list ([t (in-list optional-arg-types)]) -Boolean)
+          rst-type)))
+      (list (-Arrow ts rng))]
+     [else
+      ;; The keyword argument types including boolean flags for
+      ;; optional keyword arguments
+      (define kw-args
+        (for/fold ([pos '()])
+                  ([k (in-list (reverse sorted-kws))])
+          (match k
+            ;; mandatory keyword arguments have no extra args
+            [(Keyword: _ t #t) (cons t pos)]
+            ;; we can safely assume 't' and not (-opt t) here
+            ;; because if the keyword is not provided, the value
+            ;; will only appear in dead code (i.e. where the kw-flag arg is #f)
+            ;; within the body of the function
+            [(Keyword: _ t #f) (list* t -Boolean pos)])))
 
-       ;; Add boolean arguments for the optional type flaggs.
-       (define opt-flags (make-list (length opt-ts) -Boolean))
+      ;; Add boolean arguments for the optional type flaggs.
+      (define opt-flags (make-list (length optional-arg-types) -Boolean))
 
-       (list (-Arrow (append kw-args plain-ts opt-ts opt-flags rst-type)
-                     rng))])))
+      (list (-Arrow (append kw-args mandatory-arg-types optional-arg-types opt-flags rst-type)
+                    rng))])))
 
 ;; This is used to fix the props of keyword types.
 ;; TODO: This should also explore deeper into the actual types and remove props in there as well.
@@ -78,31 +82,6 @@
                       dty
                       dbound)]))
 
-
-(define (prefix-of a b)
-  (match* (a b)
-    [((Arrow: args1 rst kws rng)
-      (Arrow: args2 rst kws rng))
-     (and (< (length args1) (length args2))
-          (for/and ([t1 (in-list args1)]
-                    [t2 (in-list args2)])
-            (equal? t1 t2)))]
-    [(_ _) #f]))
-
-(define (arg-diff a1 a2)
-  (drop (Arrow-dom a2)
-        (length (Arrow-dom a1))))
-
-(define (find-prefixes l)
-  (define l* (sort l (λ (a1 a2) (< (length (Arrow-dom a1))
-                                   (length (Arrow-dom a2))))))
-  (for/fold ([d '()]) ([e (in-list l*)])
-    (define prefix (for/or ([(p _) (in-assoc d)])
-                     (and (prefix-of p e) p)))
-    (if prefix
-        (assoc-set d prefix (arg-diff prefix e))
-        (assoc-set d e null))))
-
 ;; handle-extra-or-missing-kws : (Listof Keyword) LambdaKeywords
 ;;                               -> (Listof Keyword)
 ;; Remove keywords in the given list that aren't in the actual lambda
@@ -122,22 +101,67 @@
           (for/list ([kw (in-list (set-subtract actual-opts expected-kws))])
             (make-Keyword kw -Bottom #f))))
 
+;; is arrow's max arity one less than arrow*'s min arity,
+;; and arrow cannot have infinite max arity,
+;; and both arrows have equivalent keyword specs
+(define (domain-is-prefix? arrow arrow* min-arity)
+  (and (not (Arrow-rst arrow))
+       (equal? (Arrow-kws arrow) (Arrow-kws arrow*))
+       (= (Arrow-max-arity arrow) (sub1 min-arity))
+       (for/and ([d (in-list (Arrow-dom arrow))]
+                 [d* (in-list (Arrow-dom arrow*))])
+         (equal? d d*))))
+
+;; calculate-mandatory-args
+;;   : (listof Arrow?) -> (assoc-listof Arrow? exact-nonnegative-integer?)
+;; We don't explicitly record optional vs mandatory args on arrows.
+;; This function looks for Arrows which, in a case->, are equivalent
+;; to having optional arguments and returns a dictionary mapping
+;; arrows to their mandatory arg count (from which we can derive their
+;; optional arg count)
+;; e.g. (calculate-mandatory-args (list (-> String Any) (-> String String Any)))
+;;   ==> (list (cons (-> String String Any) 1))
+;; meaning instead of remembering both arrows, we can just remember
+;; (-> String String Any) and the fact that only the first positional argument
+;; is mandatory (i.e. the second is optional)
+(define (calculate-mandatory-args orig-arrows)
+  ;; sorted order is important, our loops below rely on this order
+  (define arity-sorted-arrows
+    (sort orig-arrows
+          (λ (a1 a2) (>= (Arrow-max-arity a1)
+                         (Arrow-max-arity a2)))))
+  (for/fold ([mand-arg-table '()])
+            ([arrow (in-list arity-sorted-arrows)])
+    (cond
+      [(for/or ([(arrow* min-arity) (in-assoc mand-arg-table)])
+         ;; is arrow like arrow* but arrow's max arity is 1 less
+         ;; than arrow*'s currently known min arity?
+         (and (domain-is-prefix? arrow arrow* min-arity)
+              (assoc-set mand-arg-table arrow* (sub1 min-arity))))]
+      [else
+       (assoc-set mand-arg-table arrow (Arrow-min-arity arrow))])))
+
 ;; inner-kw-convert : (Listof arr) (Option LambdaKeywords) Boolean -> Type
 ;; Helper function that converts each arr to a Function type and then
 ;; merges them into a single Function type.
 (define (inner-kw-convert arrs actual-kws split?)
-  (define table (find-prefixes arrs))
+  (define mand-arg-table (calculate-mandatory-args arrs))
   (define fns
     ;; use for/list and remove duplicates afterwards instead of
     ;; set and set->list to retain determinism
     (remove-duplicates
-     (for/list ([(k v) (in-assoc table)])
-       (match k
-         [(Arrow: mand rst kws rng)
+     (for/list ([(arrow mand-arg-count) (in-assoc mand-arg-table)])
+       (match arrow
+         [(Arrow: dom rst kws rng)
           (define kws* (if actual-kws
                            (handle-extra-or-missing-kws kws actual-kws)
                            kws))
-          (convert kws* mand v rng rst split?)]))))
+          (convert kws*
+                   (take dom mand-arg-count)
+                   (drop dom mand-arg-count)
+                   rng
+                   rst
+                   split?)]))))
   (apply cl->* fns))
 
 ;; kw-convert : Type (Option LambdaKeywords) [Boolean] -> Type
@@ -216,12 +240,13 @@
             (define rest-type
               (and rest? (last opt-and-rest-args)))
             (define opt-types (take opt-and-rest-args opt-non-kw-argc))
+            (define opt-types-count (length opt-types))
             (make-Fun
-             (for/list ([to-take (in-range (add1 (length opt-types)))])
+             (for/list ([to-take (in-range (add1 opt-types-count))])
                (-Arrow (append mand-args (take opt-types to-take))
                        (erase-props/Values rng)
                        #:kws actual-kws
-                       #:rest rest-type)))]
+                       #:rest (if (= to-take opt-types-count) rest-type #f))))]
            [else (int-err "unsupported arrs in keyword function type")])]
     [_ (int-err "unsupported keyword function type")]))
 
@@ -356,11 +381,13 @@
             (define rest-type
               (and rest? (last opt-and-rest-args)))
             (define opt-types (take opt-and-rest-args opt-argc))
+            (define opt-types-len (length opt-types))
             (make-Fun
-             (for/list ([to-take (in-range (add1 (length opt-types)))])
-               (-Arrow (append mand-args (take opt-types to-take))
+             (for/list ([how-many-opt-args (in-range (add1 opt-types-len))])
+               (-Arrow (append mand-args (take opt-types how-many-opt-args))
                        rng
-                       #:rest rest-type)))]
+                       #:rest (and (= how-many-opt-args opt-types-len)
+                                   rest-type))))]
            [else (int-err "unsupported arrs in keyword function type")])]
     [_ (int-err "unsupported keyword function type")]))
 

typed-racket-lib/typed-racket/types/printer.rkt

@@ -370,8 +370,8 @@
   ;; see type-contract.rkt, which does something similar and this code
   ;; was stolen from/inspired by/etc.
   (match* ((first arrs) (last arrs))
-    [((Arrow: first-dom rst kws rng)
-      (Arrow: last-dom _ _ _))
+    [((Arrow: first-dom _ kws rng)
+      (Arrow: last-dom rst _ _))
      (define-values (mand-kws opt-kws) (partition-kws kws))
      (define opt-doms (drop last-dom (length first-dom)))
      `(->*

typed-racket-lib/typed-racket/types/utils.rkt

@@ -75,31 +75,38 @@
 ;; Check if the given arrs meet the necessary conditions to be printed
 ;; with a ->* constructor or for generating a ->* contract
 (define (has-optional-args? arrows)
-  (and (> (length arrows) 1)
-       ;; No polydots
-       (not (ormap (λ (a) (RestDots? (Arrow-rst a))) arrows))
-       ;; Keyword args, range and rest specs all the same.
-       (match-let ([(cons (Arrow: _ rst1 kws1 rng1) as) arrows])
-         (for/and ([a (in-list as)])
-           (match a
-             [(Arrow: _ rst2 kws2 rng2)
-              (and (equal? rst1 rst2)
-                   (equal? kws1 kws2)
-                   (equal? rng1 rng2))])))
-       ;; Positionals are monotonically increasing by at most one.
-       (let-values ([(_ ok?)
-                     (for/fold ([positionals (Arrow-dom (first arrows))]
-                                [ok?  #t])
-                               ([arr (in-list (rest arrows))]
-                                #:break (not ok?))
-                       (define dom (Arrow-dom arr))
-                       (define ldom (length dom))
-                       (define lpositionals (length positionals))
-                       (values dom
-                               (and (or (= ldom lpositionals)
-                                        (= ldom (add1 lpositionals)))
-                                    (equal? positionals (take dom lpositionals)))))])
-         ok?)))
+  (and (pair? arrows)
+       (pair? (cdr arrows)) ;; i.e. (> (length arrows) 1)
+       (match arrows
+         [(cons (Arrow: dom #f kws rng) as)
+          (let loop ([dom dom]
+                     [to-check (cdr arrows)])
+            (match to-check
+              [(cons (Arrow: next-dom next-rst next-kws next-rng)
+                     remaining)
+               (cond
+                 ;; a #:rest must be the LAST clause,
+                 ;; can't be a rest dots
+                 [(and next-rst (or (not (null? remaining))
+                                    (RestDots? next-rst)))
+                  #f]
+                 ;; keywords and range must be the same
+                 [(not (and (equal? kws next-kws)
+                            (equal? rng next-rng)))
+                  #f]
+                 [else
+                  ;; next arrow should have one more domain type
+                  ;; and their domains should be pointwise equal
+                  ;; for all other positional args
+                  (define dom-len (length dom))
+                  (define next-dom-len (length next-dom))
+                  (and (= next-dom-len (add1 dom-len))
+                       (for/and ([d (in-list dom)]
+                                 [next-d (in-list next-dom)])
+                         (equal? d next-d))
+                       (loop next-dom remaining))])]
+              [_ #t]))]
+         [_ #f])))
 
 (provide/cond-contract
  [instantiate-poly ((or/c Poly? PolyDots? PolyRow?) (listof Rep?)

typed-racket-lib/typed-racket/utils/utils.rkt

@@ -384,14 +384,14 @@ at least theoretically.
         [else default]))))
 
 (define (assoc-set d key val)
-  (let loop ([xd d])
+  (let loop ([entries d])
     (cond
-      [(null? xd) (list (cons key val))]
+      [(null? entries) (list (cons key val))]
       [else
-       (let ([a (car xd)])
-         (if (equal? (car a) key)
-             (cons (cons key val) (cdr xd))
-             (cons a (loop (cdr xd)))))])))
+       (let ([entry (car entries)])
+         (if (equal? (car entry) key)
+             (cons (cons key val) (cdr entries))
+             (cons entry (loop (cdr entries)))))])))
 
 (define (assoc-remove d key)
   (let loop ([xd d])

typed-racket-test/unit-tests/parse-type-tests.rkt

@@ -218,7 +218,24 @@
 
 
    ;; ->* types
-   [(->* (String Symbol) Void) (t:-> -String -Symbol -Void)]
+   [(->* (String Symbol) Void)
+    (make-Fun (list (-Arrow (list -String -Symbol) -Void)))]
+   [(->* () (String) #:rest Symbol Void)
+    (make-Fun (list (-Arrow (list) -Void)
+                    (-Arrow (list -String)
+                            #:rest -Symbol
+                            -Void)))]
+   [(->* (Number) (String) #:rest Symbol Void)
+    (make-Fun (list (-Arrow (list -Number) -Void)
+                    (-Arrow (list -Number -String)
+                            #:rest -Symbol
+                            -Void)))]
+   [(->* (Number) (String Void) #:rest Symbol Any)
+    (make-Fun (list (-Arrow (list -Number) Univ)
+                    (-Arrow (list -Number -String) Univ)
+                    (-Arrow (list -Number -String -Void)
+                            #:rest -Symbol
+                            Univ)))]
    [(->* (String Symbol) (String) Void)
     (->opt -String -Symbol [-String] -Void)]
    [(->* (String Symbol) (String Symbol) Void)

typed-racket-test/unit-tests/type-printer-tests.rkt

@@ -132,11 +132,18 @@
     (check-prints-as? (-AnyValues (-is-type '(0 . 0) -String))
                       "(AnyValues : (: (0 0) String))")
 
+    (check-prints-as?
+     (make-Fun (list (-Arrow (list Univ) #:rest Univ -String)
+                     (-Arrow (list Univ -String) #:rest Univ -String)))
+     ;; NOT (->* (Any) (String) #:rest Any String)
+     "(case-> (-> Any Any * String) (-> Any String Any * String))")
     (check-prints-as? (->opt Univ [] -Void) "(-> Any Void)")
     (check-prints-as? (->opt [-String] -Void) "(->* () (String) Void)")
     (check-prints-as? (->opt Univ [-String] -Void) "(->* (Any) (String) Void)")
     (check-prints-as? (->opt Univ -Symbol [-String] -Void)
                       "(->* (Any Symbol) (String) Void)")
+    (check-prints-as? (->optkey Univ [-String] #:rest -Symbol -Void)
+                      "(->* (Any) (String) #:rest Symbol Void)")
     (check-prints-as? (->optkey Univ [-String] #:x -String #f -Void)
                       "(->* (Any) (String #:x String) Void)")
     (check-prints-as? (->optkey Univ [-String] #:x -String #t -Void)

typed-racket-test/unit-tests/typecheck-tests.rkt

@@ -4209,6 +4209,121 @@
        [tc-err (let ()
                  (define (f #:x x y) 1)
                  (map f (list 1 2 3)))]
+       ;; fixing optional args + rest args, see
+       ;; TR github issue #614
+       [tc-err
+        (let ()
+          ((tr:λ ([y : String "default"] . rest)
+             y)
+           42)
+          (void))
+        #:ret (ret -Void #f #f)
+        #:msg #rx"No function domains matched"]
+       [tc-err
+        (let ()
+          ((tr:λ ([x : Number] [y : String "default"] . rest)
+             y)
+           0 1)
+          (void))
+        #:ret (ret -Void #f #f)
+        #:msg #rx"No function domains matched"]
+       [tc-e
+        (let ()
+          (ann
+           (case-lambda [(str num . nums)
+                         (+ num (string-length str))]
+                        [(str . nums)
+                         (string-length str)]
+                        [l (length (ann l Null))])
+           (->* () (String) #:rest Number Number))
+          (void))
+        -Void]
+       [tc-e
+        (let ()
+          (ann
+           (case-lambda [(x str num . nums)
+                         (+ x num (string-length str))]
+                        [(x str . nums)
+                         (+ x (string-length str))]
+                        [l (length (ann l (Listof Number)))])
+           (->* (Number) (String) #:rest Number Number))
+          (void))
+        -Void]
+       [tc-e
+        (let ()
+          (ann
+           (case-lambda [(x str num . nums)
+                         (+ x num (string-length str))]
+                        [l (let ([fst (car l)])
+                             (cond
+                               [(number? fst) fst]
+                               [else (string-length fst)]))])
+           (->* (Number) (String) #:rest Number Number))
+          (void))
+        -Void]
+       [tc-e
+        (let ()
+          (ann
+           (case-lambda [(str)
+                         (string-length str)]
+                        [(str sym)
+                         (+ (string-length (symbol->string sym))
+                            (string-length str))]
+                        [(str sym . nums)
+                         (+ (string-length (symbol->string sym))
+                            (string-length str))]
+
+                        [l (length (ann l (Listof (U String Number))))])
+           (->* () (String Symbol) #:rest Number Number))
+          (void))
+        -Void]
+       [tc-e
+        (let ()
+          (ann
+           (case-lambda [(x str)
+                         (+ x (string-length str))]
+                        [(x str sym)
+                         (+ x
+                            (string-length (symbol->string sym))
+                            (string-length str))]
+                        [(x str sym . nums)
+                         (+ x
+                            (string-length (symbol->string sym))
+                            (string-length str))]
+
+                        [l (length (ann l (Listof (U String Number))))])
+           (->* (Number) (String Symbol) #:rest Number Number))
+          (void))
+        -Void]
+       [tc-e
+        (let ()
+          (ann
+           (case-lambda [(str . nums) 42]
+                        [l (let ([fst (car l)])
+                             (cond
+                               [(number? fst) fst]
+                               ;; this should pass since we know
+                               ;; l is null here -- i.e. it's dead code
+                               [else (ann fst Number)]))])
+           (->* () (String) #:rest Number Number))
+          (void))
+        -Void]
+       [tc-err
+        (let ()
+          (ann
+           (case-lambda [(x str num . nums) 42]
+                        [l (let ([snd (cadr l)])
+                             (cond
+                               [(number? snd) snd]
+                               ;; this else should fail to typecheck
+                               ;; it should not be dead code... since
+                               ;; snd is a String (if it exists... but
+                               ;; the type for cadr lets us try)
+                               [else (ann snd Number)]))])
+           (->* (Number) (String) #:rest Number Number))
+          (void))
+        #:ret (ret -Void #f #f)
+        #:msg #rx"given: String"]
        )
 
   (test-suite