add an arrow when typechecking case->

For a function that has optional parameter types [t1, t2, t_i ... t_n], if each
of [t_i ... t_n] is a supertype of the first rest parameter type, add to the
resulting the function type one arrow with [t_i ... t_n] being absorbed into
the rest.

Author: capfredf

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

@@ -11,7 +11,7 @@
                     [->* t:->*]
                     [one-of/c t:one-of/c])
          (private type-annotation syntax-properties)
-         (types resolve type-table)
+         (types resolve type-table subtype)
          (typecheck signatures tc-metafunctions tc-subst)
          (env lexical-env tvar-env index-env scoped-tvar-env)
          (utils tc-utils)
@@ -639,12 +639,28 @@
   (match expected
     [(tc-result1:(? DepFun? dep-fun-ty))
      (tc/dep-lambda formalss bodies dep-fun-ty)]
-    [_ (make-Fun
-        (tc/mono-lambda
-         (for/list ([f (in-syntax formalss)]
-                    [b (in-syntax bodies)])
-           (cons (make-formals f not-in-poly) b))
-         expected))]))
+    [_
+     (define arrs (tc/mono-lambda
+                   (for/list ([f (in-syntax formalss)]
+                              [b (in-syntax bodies)])
+                     (cons (make-formals f not-in-poly) b))
+                   expected))
+     
+     (define (maybe-new-arrow arrs)
+       (append arrs (match arrs
+                      [(or (? empty?) (list _)) null]
+                      [(app last (Arrow: dom (and (Rest: (list ty tys ...)) rst) kws rng))
+                       (define new-doms (dropf-right dom (lambda (x) (subtype ty x))))
+                       (if (equal? (length new-doms) dom)
+                           null
+                           (list (make-Arrow new-doms
+                                             rst
+                                             kws
+                                             rng)))]
+                      [_ null])))
+     (define arrs^ (maybe-new-arrow arrs))
+     (make-Fun arrs^)]))
+
 
 (define (plambda-prop stx)
   (define d (plambda-property stx))

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

@@ -7,6 +7,7 @@
 (require "../utils/utils.rkt"
          (utils prefab identifier)
          racket/list
+         racket/lazy-require
          syntax/id-set
          racket/match
          (prefix-in c: (contract-req))
@@ -24,6 +25,7 @@
 
          (for-syntax racket/base syntax/parse))
 
+(lazy-require ("subtype.rkt" (subtype)))
 (provide (all-defined-out)
          (all-from-out "base-abbrev.rkt" "match-expanders.rkt"))
 
@@ -188,11 +190,21 @@
 (define/decl -false-propset (-PS -ff -tt))
 
 (define (opt-fn args opt-args result #:rest [rest #f] #:kws [kws null])
-  (apply cl->* (for/list ([i (in-range (add1 (length opt-args)))])
+  (define ret (for/list ([i (in-range (add1 (length opt-args)))])
                  (make-Fun (list (-Arrow (append args (take opt-args i))
                                          result ;; only the LAST arrow gets the rest arg
                                          #:rest (and (= i (length opt-args)) rest)
-                                         #:kws kws))))))
+                                         #:kws kws)))))
+  (define ret^ (append ret (cond
+                             [rest
+                              (match-define (Rest: (list ty tys ...)) rest)
+                              (list (make-Fun (list (-Arrow
+                                                     (dropf-right opt-args (lambda (x) (subtype ty x)))
+                                                     result
+                                                     #:rest rest
+                                                     #:kws kws))))]
+                             [else null])))
+  (apply cl->* ret^))
 
 (define-syntax-rule (->opt args ... [opt ...] res)
   (opt-fn (list args ...) (list opt ...) res))

typed-racket-test/succeed/gh-issue-873.rkt

@@ -0,0 +1,18 @@
+#lang typed/racket
+
+(: bar (-> (-> Natural * Any) Any))
+(define (bar f)
+  'any)
+
+(: foo (-> (->* () (Integer Integer) #:rest Natural Any)
+           Any))
+(define (foo f)
+  (bar f))
+
+(: foo^ (-> Any * Any))
+(define foo^
+  (case-lambda
+    [() 'one]
+    [(a) 'two]
+    [(a b . cs) 'three]))
+