Fix polydots

- parsing of polydots values was fixed
 - certain polydots error cases are now reported
 - the custom application rule for values was fixed

Closes PR 13365

Please merge to 5.3.2

original commit: f577b49a4df973aab1cfc8cdb45f93320637009d

collects/tests/typed-racket/fail/pr13365-variation-1.rkt

@@ -0,0 +1,6 @@
+#;
+(exn-pred #rx"Expected 0 values and a ...")
+#lang typed/racket
+
+(: f (All (a ...) (a ... a -> (Values a ... a))))
+(define (f . x) x)

collects/tests/typed-racket/fail/pr13365-variation-2.rkt

@@ -0,0 +1,6 @@
+#;
+(exn-pred #rx"Expected String, but got")
+#lang typed/racket
+
+(: f (All (a ...) (a ... a -> (Values String a ... a))))
+(define (f . x) x)

collects/tests/typed-racket/fail/pr13365-variation-3.rkt

@@ -0,0 +1,6 @@
+#;
+(exn-pred #rx"Expected a ...")
+#lang typed/racket
+
+(: f (All (a ...) (a ... a -> (Values a ... a))))
+(define (f . x) (values 1))

collects/tests/typed-racket/fail/pr13365.rkt

@@ -0,0 +1,6 @@
+#;
+(exn-pred #rx"Expected 0 values and a ...")
+#lang typed/racket
+
+(: f (All (a ...) (a ... a -> (Values a ... a))))
+(define f (lambda: (x : a ... a) x))

collects/typed-racket/private/parse-type.rkt

@@ -418,17 +418,17 @@
            (if (bound-tvar? var)
                (tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." var)
                (tc-error/stx #'bound "Type variable ~a is unbound" var)))
-         (make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
-                          (extend-tvars (list var)
-                            (parse-type #'dty))
-                          var))]
+         (-values-dots (map parse-type (syntax->list #'(tys ...)))
+                       (extend-tvars (list var)
+                         (parse-type #'dty))
+                       var))]
       [((~and kw (~or t:Values values)) tys ... dty _:ddd)
        (add-disappeared-use #'kw)
        (let ([var (infer-index stx)])
-         (make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
-                          (extend-tvars (list var)
-                              (parse-type #'dty))
-                            var))]
+         (-values-dots (map parse-type (syntax->list #'(tys ...)))
+                       (extend-tvars (list var)
+                         (parse-type #'dty))
+                       var))]
       [((~and kw (~or t:Values values)) tys ...)
        (add-disappeared-use #'kw)
        (-values (map parse-type (syntax->list #'(tys ...))))]

collects/typed-racket/typecheck/check-below.rkt

@@ -76,6 +76,22 @@
              (not (object-better? o1 o2)))
         (tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))])
      expected]
+    ;; case where expected is like (Values a ... a) but got something else
+    [((tc-results: t1 f o) (tc-results: t2 f o dty dbound))
+     (unless (= (length t1) (length t2))
+       (tc-error/expr "Expected ~a values and ~a ..., but got ~a values"
+                      (length t2) dty (length t1)))
+     (unless (for/and ([t t1] [s t2]) (subtype t s))
+       (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
+     expected]
+    ;; case where you have (Values a ... a) but expected something else
+    [((tc-results: t1 f o dty dbound) (tc-results: t2 f o))
+     (unless (= (length t1) (length t2))
+       (tc-error/expr "Expected ~a values, but got ~a values and ~a ..."
+                      (length t2) (length t1) dty))
+     (unless (for/and ([t t1] [s t2]) (subtype t s))
+       (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
+     expected]
     [((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound))
      (unless (andmap subtype t1 t2)
        (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))

collects/typed-racket/typecheck/tc-app/tc-app-values.rkt

@@ -34,7 +34,12 @@
       (single-value #'arg) ;Type check the argument, to find other errors
       (tc-error/expr #:return expected
         "wrong number of values: expected ~a but got one"
-         (length ts))]))
+         (length ts))]
+     ;; match polydots case and error
+     [(tc-results: ts _ _ dty dbound)
+      (single-value #'arg)
+      (tc-error/expr #:return expected
+        "Expected ~a ..., but got only one value" dty)]))
   ;; handle `values' specially
   (pattern (values . args)
     (match expected

collects/typed-racket/types/abbrev.rkt

@@ -75,11 +75,21 @@
   (c:->* (Type/c) (FilterSet? Object?) Result?)
   (make-Result t f o))
 
+;; convenient constructor for Values
+;; (wraps arg types with Result)
 (define/cond-contract (-values args)
-     (c:-> (listof Type/c) (or/c Type/c Values?))
-     (match args
-       ;[(list t) t]
-       [_ (make-Values (for/list ([i args]) (-result i)))]))
+  (c:-> (listof Type/c) (or/c Type/c Values?))
+  (match args
+    ;[(list t) t]
+    [_ (make-Values (for/list ([i args]) (-result i)))]))
+
+;; convenient constructor for ValuesDots
+;; (wraps arg types with Result)
+(define/cond-contract (-values-dots args dty dbound)
+  (c:-> (listof Type/c) Type/c (or/c symbol? natural-number/c)
+        ValuesDots?)
+  (make-ValuesDots (for/list ([i args]) (-result i))
+                   dty dbound))
 
 ;; basic types