Type inference fails for dotted polymorphic functions when argument is `Mutable-Vector` vs `Mutable-Vectorof`

[NoahStoryM]

What version of Racket are you using?

8.18 [cs]

What program did you run?

#lang typed/racket/base

(: test (→ (∀ (a ...)
              (→ (Mutable-Vectorof (→ (Values a ... a))) (Values a ... a)))
           (→ String String)))

(define ((test f) s)
  (f (vector (λ () s))))

What should have happened?

The program should type-check successfully. The expression (vector (λ () s)) is inferred as (Mutable-Vector (→ String)), which is a subtype of (Mutable-Vectorof (→ String)). The type checker should be able to unify this with (Mutable-Vectorof (→ (Values a ... a))) and instantiate a ... to String.

Evidence that the subtype relationship is recognized: the following two workarounds both type-check without error:

;; Workaround 1: explicit annotation
(define ((test f) s)
  (f (ann (vector (λ () s)) (Mutable-Vectorof (→ String)))))

;; Workaround 2: explicit instantiation
(define ((test f) s)
  ((inst f String) (vector (λ () s))))

If you got an error message, please include it here.

Type Checker: Polymorphic function `f' could not be applied to arguments:
Argument 1:
  Expected: (Mutable-Vectorof (-> (values a ... a)))
  Given:    (Mutable-Vector (-> String))
Result type:     (values a ... a)
Expected result: String
  in: (f (vector (λ () s)))

The same issue also manifests with case→. When Mutable-Vectorof is one case alongside Mutable-Vector (zero-element), the error message reports a mismatch against the first case instead:

#lang typed/racket/base

(: test (→ (∀ (a ...)
              (case→ (→ (Mutable-Vector) Nothing)
                     (→ (Mutable-Vectorof (→ (Values a ... a))) (Values a ... a))))
           (→ String String)))

(define ((test f) s)
  (f (vector (λ () s))))

Or

#lang typed/racket/base

(: test (→ (∀ (a ...)
              (case→ (→ (Mutable-Vector) Nothing)
                     (→ (Mutable-Vectorof (→ (Values a ... a))) (Values a ... a))))
           (→ String String)))

(define ((test f) s)
  ((inst f String) (vector (λ () s))))

Error message:

Type Checker: type mismatch
  expected: (Mutable-Vector)
  given: (Mutable-Vector (-> String))
  in: (vector (λ () s))