From a51f55d04ef68ef1cb1ba379cba91ee08ac81130 Mon Sep 17 00:00:00 2001
From: Eric Dobson <eric.n.dobson@gmail.com>
Date: Sat, 9 Feb 2013 09:25:29 -0800
Subject: [PATCH] Make lists with minimum lengths be a subtype of sequences.

original commit: 5ed26e806bb890db0aa4c3482c5780d9203a6637
---
 .../typed-racket/unit-tests/subtype-tests.rkt   |  3 +++
 collects/typed-racket/infer/infer-unit.rkt      |  2 ++
 collects/typed-racket/types/abbrev.rkt          | 12 +-----------
 collects/typed-racket/types/base-abbrev.rkt     | 17 +++++++++++++++--
 collects/typed-racket/types/subtype.rkt         |  3 +++
 5 files changed, 24 insertions(+), 13 deletions(-)

diff --git a/collects/tests/typed-racket/unit-tests/subtype-tests.rkt b/collects/tests/typed-racket/unit-tests/subtype-tests.rkt
index 30faa798..1c8af2ed 100644
--- a/collects/tests/typed-racket/unit-tests/subtype-tests.rkt
+++ b/collects/tests/typed-racket/unit-tests/subtype-tests.rkt
@@ -151,6 +151,9 @@
    [(-val 0.0f0) -SingleFlonum]
    [(-val -0.0f0) -SingleFlonum]
    [(-val 1.0f0) -SingleFlonum]
+   [(-pair -String (-lst -String)) (-seq -String)]
+   [FAIL (-pair -String (-lst -Symbol)) (-seq -String)]
+   [FAIL (-pair -String (-vec -String)) (-seq -String)]
    ))
 
 (define-go
diff --git a/collects/typed-racket/infer/infer-unit.rkt b/collects/typed-racket/infer/infer-unit.rkt
index a577b9b1..aaa6af5b 100644
--- a/collects/typed-racket/infer/infer-unit.rkt
+++ b/collects/typed-racket/infer/infer-unit.rkt
@@ -449,6 +449,8 @@
            (cgen/list V X Y ts ts*)]
           [((Listof: t) (Sequence: (list t*)))
            (cg t t*)]
+          [((Pair: t1 t2) (Sequence: (list t*)))
+           (cset-meet (cg t1 t*) (cg t2 (-lst t*)))]
           [((List: ts) (Sequence: (list t*)))
            (cset-meet* (for/list ([t (in-list ts)])
                          (cg t t*)))]
diff --git a/collects/typed-racket/types/abbrev.rkt b/collects/typed-racket/types/abbrev.rkt
index 79cf4ed9..78376e84 100644
--- a/collects/typed-racket/types/abbrev.rkt
+++ b/collects/typed-racket/types/abbrev.rkt
@@ -26,8 +26,7 @@
 
 (provide (except-out (all-defined-out) make-Base)
          (all-from-out "base-abbrev.rkt" "match-expanders.rkt")
-         (rename-out [make-Listof -lst]
-                     [make-MListof -mlst]))
+         (rename-out [make-MListof -mlst]))
 
 ;; all the types defined here are not numeric
 (define (make-Base name contract predicate marshaled)
@@ -56,7 +55,6 @@
 
 
 
-(define (make-Listof elem) (-mu list-rec (Un (-val null) (-pair elem list-rec))))
 (define (make-MListof elem) (-mu mlist-rec (Un (-val null) (-mpair elem mlist-rec))))
 
 (define (-lst* #:tail [tail (-val null)] . args)
@@ -299,9 +297,6 @@
 
 ;; convenient syntax
 
-(define-syntax -v
-  (syntax-rules ()
-    [(_ x) (make-F 'x)]))
 
 (define-syntax -poly
   (syntax-rules ()
@@ -316,11 +311,6 @@
            [vars (-v vars)] ...)
        (make-PolyDots (list 'vars ... 'dotted) ty))]))
 
-(define-syntax -mu
-  (syntax-rules ()
-    [(_ var ty)
-     (let ([var (-v var)])
-       (make-Mu 'var ty))]))
 
 ;; function type constructors
 
diff --git a/collects/typed-racket/types/base-abbrev.rkt b/collects/typed-racket/types/base-abbrev.rkt
index 235fe07e..e5f52133 100644
--- a/collects/typed-racket/types/base-abbrev.rkt
+++ b/collects/typed-racket/types/base-abbrev.rkt
@@ -7,7 +7,8 @@
          racket/match racket/list
          (for-template racket/base))
 
-(provide (all-defined-out))
+(provide (all-defined-out)
+         (rename-out [make-Listof -lst]))
 
 ;Top and error types
 (define Univ (make-Univ))
@@ -18,8 +19,9 @@
 ;return type of functions
 (define ManyUniv (make-AnyValues))
 
-;; Char type (needed because of how sequences are checked in subtype)
+;; Char type and List type (needed because of how sequences are checked in subtype)
 (define -Char (make-Base 'Char #'char? char? #'-Char #f))
+(define (make-Listof elem) (-mu list-rec (simple-Un (make-Value null) (make-Pair elem list-rec))))
 
 
 ;; Simple union type, does not check for overlaps
@@ -50,3 +52,14 @@
       [(t) t]
       [args
        (make-union* (remove-dups (sort (append-map flat args) type<?)))])))
+
+;; Recursive types
+(define-syntax -v
+  (syntax-rules ()
+    [(_ x) (make-F 'x)]))
+
+(define-syntax -mu
+  (syntax-rules ()
+    [(_ var ty)
+     (let ([var (-v var)])
+       (make-Mu 'var ty))]))
diff --git a/collects/typed-racket/types/subtype.rkt b/collects/typed-racket/types/subtype.rkt
index dddab1ce..37b83b64 100644
--- a/collects/typed-racket/types/subtype.rkt
+++ b/collects/typed-racket/types/subtype.rkt
@@ -279,6 +279,9 @@
                (subtypes* A0 ts ts*)]
               [((Listof: t) (Sequence: (list t*)))
                (subtype* A0 t t*)]
+              [((Pair: t1 t2) (Sequence: (list t*)))
+               (let ([A1 (subtype* A0 t1 t*)])
+                 (and A1 (subtype* A1 t2 (-lst t*))))]
               [((List: ts) (Sequence: (list t*)))
                (subtypes* A0 ts (map (λ _ t*) ts))]
               [((HeterogeneousVector: ts) (Sequence: (list t*)))