Fix subtyping of (ListDots t 'a) <: (Listof t).

Closes PR 13636.

original commit: 6898a7c880f1a37219e61d420ed6610a4d24f384

collects/tests/typed-racket/unit-tests/subtype-tests.rkt

@@ -223,6 +223,9 @@
     (-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))
     (-> Univ -Boolean : (-FS (-filter -String 0) (-not-filter -String 0)))]
 
+   [FAIL (make-ListDots (-box (make-F 'a)) 'a) (-lst (-box Univ))]
+   [(make-ListDots (-> -Symbol (make-F 'a)) 'a) (-lst (-> -Symbol Univ))]
+
    ))
 
 (define-go

collects/typed-racket/types/abbrev.rkt

@@ -269,23 +269,6 @@
 (define -force (make-ForcePE))
 
 
-;; convenient syntax
-
-
-(define-syntax -poly
-  (syntax-rules ()
-    [(_ (vars ...) ty)
-     (let ([vars (-v vars)] ...)
-       (make-Poly (list 'vars ...) ty))]))
-
-(define-syntax -polydots
-  (syntax-rules ()
-    [(_ (vars ... dotted) ty)
-     (let ([dotted (-v dotted)]
-           [vars (-v vars)] ...)
-       (make-PolyDots (list 'vars ... 'dotted) ty))]))
-
-
 ;; function type constructors
 
 (define top-func (make-Function (list (make-top-arr))))

collects/typed-racket/types/base-abbrev.rkt

@@ -233,3 +233,18 @@
 
 (define (make-arr-dots dom rng dty dbound)
   (make-arr* dom rng #:drest (cons dty dbound)))
+
+
+;; convenient syntax
+(define-syntax -poly
+  (syntax-rules ()
+    [(_ (vars ...) ty)
+     (let ([vars (-v vars)] ...)
+       (make-Poly (list 'vars ...) ty))]))
+
+(define-syntax -polydots
+  (syntax-rules ()
+    [(_ (vars ... dotted) ty)
+     (let ([dotted (-v dotted)]
+           [vars (-v vars)] ...)
+       (make-PolyDots (list 'vars ... 'dotted) ty))]))

collects/typed-racket/types/subtype.rkt

@@ -361,8 +361,11 @@
               ;; recur structurally on dotted lists, assuming same bounds
               [((ListDots: s-dty dbound) (ListDots: t-dty dbound))
                (subtype* A0 s-dty t-dty)]
+              ;; For dotted lists and regular lists, we check that (All (dbound) s-dty) is a subtype
+              ;; of t-elem, so that no matter what dbound is instatiated with s-dty is still a subtype
+              ;; of t-elem. We cannot just replace dbound with Univ because of variance issues.
               [((ListDots: s-dty dbound) (Listof: t-elem))
-               (subtype* A0 (substitute Univ dbound s-dty) t-elem)]
+               (subtype* A0 (-poly (dbound) s-dty) t-elem)]
               ;; quantification over two types preserves subtyping
               [((Poly: ns b1) (Poly: ms b2))
                (=> unmatch)