Make dotted functions of the same bound correctly be inferred.

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt

@@ -265,17 +265,19 @@
             [new-tys (for/list ([var (in-list vars)])
                        (substitute (make-F var) dbound dty))])
        (% move-vars-to-dmap (cgen/list V (append vars X) Y ss (append ts new-tys)) dbound vars))]
-    ;; this case is just for constrainting other variables, not dbound
+
+    ;; samed dotted bound
     [((seq ss (dotted-end s-dty dbound))
       (seq ts (dotted-end t-dty dbound)))
      #:return-unless (= (length ss) (length ts))
      #f
-     ;; If we want to infer the dotted bound, then why is it in both types?
-     #:return-when (memq dbound Y)
-     #f
      (% cset-meet
         (cgen/list V X Y ss ts)
-        (cgen V X Y s-dty t-dty))]
+        (if (memq dbound Y)
+            (extend-tvars (list dbound)
+              (% move-rest-to-dmap (cgen V (cons dbound X) Y s-dty t-dty) dbound))
+            (cgen V X Y s-dty t-dty)))]
+
     ;; bounds are different
     [((seq ss (dotted-end s-dty (? (λ (db) (memq db Y)) dbound)))
       (seq ts (dotted-end t-dty dbound*)))

pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/infer-tests.rkt

@@ -136,6 +136,11 @@
     [infer-t (->... null ((-v a) a) (-v b)) (-> -Symbol -String) #:vars '(b) #:indices '(a)]
     [infer-t (->... null ((-v a) a) (make-ListDots (-v a) 'a)) (-> -String -Symbol  (-lst* -String -Symbol)) #:indices '(a)]
     [infer-t (->... (list (-v b)) ((-v a) a) (-v b)) (-> -String -Symbol -String) #:vars '(b) #:indices '(a)]
+    [infer-t (->... (list (-v b)) ((-v a) a) (-v b))
+             (->... (list -Symbol) (-String a) (-v b))
+             #:vars '(b) #:indices '(a)
+             #:result [(-lst* (make-ListDots (-v a) 'a) (-v b))
+                       (-lst* (-lst -String) -Symbol)]]
 
     [infer-l (list (->... null ((-v b) b) (-v a))  (-> (-v a) -Boolean))
              (list (-> -String            -Symbol) (-> -Symbol   -Boolean))