From 3fd969651fbb7c90983ae76542c80391624e1f39 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 19 Jun 2008 11:57:07 -0400
Subject: [PATCH] Fix type of filter, and inference w/ effects.

---
 collects/typed-scheme/private/base-env.ss   | 13 ++++++++++++-
 collects/typed-scheme/private/infer-unit.ss | 20 ++++++++++++++++++--
 collects/typed-scheme/private/subtype.ss    |  7 +++++--
 collects/typed-scheme/private/type-utils.ss |  5 ++++-
 4 files changed, 39 insertions(+), 6 deletions(-)

diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 95df2174fa..115f783814 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -9,10 +9,13 @@
  '#%paramz
  (only-in scheme/match/runtime match:error))
 
+
+
 ;; these are all for constructing the types given to variables
 (require (for-syntax
           scheme/base
           "init-envs.ss"
+          "effect-rep.ss"
           (except-in "type-rep.ss" make-arr)
           "type-effect-convenience.ss"
           (only-in "type-effect-convenience.ss" [make-arr* make-arr])
@@ -132,7 +135,15 @@
              (cl-> [((a b . -> . b) b (make-lst a)) b]
                    [((a b c . -> . c) c (make-lst a) (make-lst b)) c]))]
      [foldr  (-poly (a b c) ((a b . -> . b) b (-lst a) . -> . b))]
-     [filter (-poly (a) ((a . -> . B) (-lst a) . -> . (-lst a)))]
+     [filter (-poly (a b) (cl->*
+                           ((a . -> . B
+                               :
+                               (list (make-Latent-Restrict-Effect b))
+                               (list (make-Latent-Remove-Effect b)))
+                            (-lst a)
+                            . -> .
+                            (-lst b))
+                           ((a . -> . B) (-lst a) . -> . (-lst a))))]
      [take   (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
      [drop   (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
      [last   (-poly (a) ((-lst a) . -> . a))]
diff --git a/collects/typed-scheme/private/infer-unit.ss b/collects/typed-scheme/private/infer-unit.ss
index 9def9e8c0a..f1445f35e2 100644
--- a/collects/typed-scheme/private/infer-unit.ss
+++ b/collects/typed-scheme/private/infer-unit.ss
@@ -91,13 +91,29 @@
                         (filter (lambda (te) (not (ormap (lambda (s) (type-equal? s te)) ss))) ts))])
     (cgen/list V X ss* ts*)))
 
+;; t and s must be *latent* effects
+(define (cgen/eff V X t s)
+  (match* (t s)
+    [(e e) (empty-cset X)]
+    [((Latent-Restrict-Effect: t) (Latent-Restrict-Effect: s))
+     (cset-meet (cgen V X t s) (cgen V X s t))]
+    [((Latent-Remove-Effect: t) (Latent-Remove-Effect: s))
+     (cset-meet (cgen V X t s) (cgen V X s t))]
+    [(_ _) (fail! t s)]))
+
+(define (cgen/eff/list V X ts ss)
+  (cset-meet* (for/list ([t ts] [s ss]) (cgen/eff V X t s))))
+
 (define (cgen/arr V X t-arr s-arr)
   (define (cg S T) (cgen V X S T))
   (match* (t-arr s-arr)
           [((arr: ts t #f #f t-thn-eff t-els-eff)
             (arr: ss s #f #f s-thn-eff s-els-eff))
-           (cset-meet (cgen/list X V ss ts)
-                      (cg t s))]
+           (cset-meet* 
+            (list (cgen/list X V ss ts)
+                  (cg t s)
+                  (cgen/eff/list V X t-thn-eff s-thn-eff)
+                  (cgen/eff/list V X t-els-eff s-els-eff)))]
           [((arr: ts t t-rest #f t-thn-eff t-els-eff)
             (arr: ss s s-rest #f s-thn-eff s-els-eff))
            (let ([arg-mapping 
diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss
index 01698ffbba..398fe7b226 100644
--- a/collects/typed-scheme/private/subtype.ss
+++ b/collects/typed-scheme/private/subtype.ss
@@ -108,8 +108,11 @@
            (or (and (null? thn-eff*) (null? els-eff*))
                (and (effects-equal? thn-eff thn-eff*)
                     (effects-equal? els-eff els-eff*))
-               (and (andmap sub-eff thn-eff thn-eff*)
-                    (andmap sub-eff els-eff els-eff*)))
+               (and 
+                (= (length thn-eff) (length thn-eff*))
+                (= (length els-eff) (length els-eff*))
+                (andmap sub-eff thn-eff thn-eff*)
+                (andmap sub-eff els-eff els-eff*)))
          (fail! s t))
        ;; either the effects have to be the same, or the supertype can't have effects
        (let ([A (subtypes*/varargs A0 t1 s1 s3)])
diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index e32f735f5f..9da1fe368c 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -130,7 +130,10 @@
 ;; equality - good
 
 (define tc-result-equal? equal?)
-(define (effects-equal? fs1 fs2) (andmap eq? fs1 fs2))
+(define (effects-equal? fs1 fs2) 
+  (and 
+   (= (length fs1) (length fs2))
+   (andmap eq? fs1 fs2)))
 
 
 ;; fv : Type -> Listof[Name]