Values handling in non-function contexts causes errors

[NoahStoryM]

What version of Racket are you using?
8.14 [cs]

What program did you run?

1. Using Values in the return type of let:

Welcome to Racket v8.14 [cs].
> (let #:∀ (a ...) ([thk : (→ (Values a ... a)) (λ () (values 1 2 3))])
    (thk))
- : (values Integer Integer Integer) [more precisely: (Values One Positive-Byte Positive-Byte)]
1
2
3

> (let #:∀ (a ...) ([thk : (→ (Values a ... a)) (λ () (values 1 2 3))]) : (Values a ... a)
    (thk))
string:1:80: Type Checker: Error in macro expansion -- parse error in type;
 type variable must be used with ...
  variable: a
  in: a
 [,bt for context]

Equivalent code that works by wrapping Values inside a function type:

> (: f (∀ (a ...) (→ (→ (Values a ... a)) (Values a ... a))))
> (define (f thk) (thk))
> (f (λ () (values 1 2 3)))
- : (values Integer Integer Integer) [more precisely: (Values One Positive-Byte Positive-Byte)]
1
2
3

> (: g (∀ (a ...) (→ (→ (Values a ... a)) (Values a ... a))))
> (define (g thk1)
    (: thk2 (→ (Values a ... a)))
    (define thk2 thk1)
    (thk2))
> (g (λ () (values 1 2 3)))
- : (values Integer Integer Integer) [more precisely: (Values One Positive-Byte Positive-Byte)]
1
2
3

2. Using Values in let/cc:

Welcome to Racket v8.14 [cs].
> (require typed/racket/unsafe)
> (unsafe-require/typed racket/base
    [call-in-continuation
     (∀ (a ...)
        (case→ (→ (→ a ... a Nothing) (→ (Values a ... a)) Nothing)
               (→ (→ Any * Nothing) (→ AnyValues) Nothing)))])

> (: h (∀ (a ...) (→ (→ (Values a ... a)) (Values a ... a))))
> (define (h thk)
    (let/cc k : (Values a ... a)
      (call-in-continuation k thk)))
string:2:2: Type Checker: Polymorphic function `call/cc' could not be applied to arguments:
Types: (-> (-> Nothing) (values))  -> (values)
       (-> (-> Nothing) (values)) Prompt-TagTop  -> (values)
       (-> (-> a c ... c Nothing) (values b c ... c))  -> (values (U a b) c ... c)
       (-> (-> a c ... c Nothing) (values b c ... c)) Prompt-TagTop  -> (values (U a b) c ... c)
Arguments: (-> (-> a ... a Nothing) Nothing)
Expected result: (values)
  in: (let/cc k : (Values a ... a) (call-in-continuation k thk))
 [,bt for context]

A working alternative:

> (: i (∀ (a ...) (→ (→ (Values a ... a)) (→ (→ a ... a Nothing) (Values a ... a)))))
> (define ((i thk) k) (call-in-continuation k thk))
> (call/cc (i (λ () (values 1 2 3))))
- : (values Integer Integer Integer) [more precisely: (Values One Positive-Byte Positive-Byte)]
1
2
3