From 9fe3747a19e38d2041814d897f7db0e67d02a0e0 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Wed, 19 May 2010 12:23:32 -0500
Subject: [PATCH] Allow expected type to have weaker filters and objects. 
 Closes PR 10729.

---
 .../typed-scheme/succeed/pr10718+10755.rkt    | 15 ++++++++++
 .../tests/typed-scheme/succeed/pr10729.rkt    |  4 +++
 collects/tests/typed-scheme/xfail/pr10618.rkt | 12 ++++++++
 .../typed-scheme/typecheck/tc-expr-unit.rkt   | 29 +++++++++++++++----
 4 files changed, 54 insertions(+), 6 deletions(-)
 create mode 100644 collects/tests/typed-scheme/succeed/pr10718+10755.rkt
 create mode 100644 collects/tests/typed-scheme/succeed/pr10729.rkt
 create mode 100644 collects/tests/typed-scheme/xfail/pr10618.rkt

diff --git a/collects/tests/typed-scheme/succeed/pr10718+10755.rkt b/collects/tests/typed-scheme/succeed/pr10718+10755.rkt
new file mode 100644
index 0000000000..a0909006b2
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/pr10718+10755.rkt
@@ -0,0 +1,15 @@
+#lang typed/scheme
+
+(: g ((U Integer #f) -> Integer))
+(define (g x)
+  (cond
+    [(or (equal? x 0) (equal? x #f)) 0]
+    [else x]))
+
+(define-type-alias Source (U Symbol #f))
+
+(: source? (Any -> Boolean : Source))
+(define (source? x)
+  (if (false? x)
+      #t
+      (symbol? x)))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/pr10729.rkt b/collects/tests/typed-scheme/succeed/pr10729.rkt
new file mode 100644
index 0000000000..ab79d45724
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/pr10729.rkt
@@ -0,0 +1,4 @@
+#lang typed/scheme
+(: lon? (Any -> Boolean : (Listof Number)))
+(define (lon? x)
+  (and (list? x) (andmap number? x)))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/xfail/pr10618.rkt b/collects/tests/typed-scheme/xfail/pr10618.rkt
new file mode 100644
index 0000000000..57ad03d797
--- /dev/null
+++ b/collects/tests/typed-scheme/xfail/pr10618.rkt
@@ -0,0 +1,12 @@
+#lang scheme/load
+
+(module bar scheme
+  (define (f x) x)
+  (provide f))
+
+(module foo typed/scheme
+  (require/typed 'bar (f (Node -> Integer)))
+  (define-struct: node ({x : Integer}))
+  (define-type-alias Node node))
+
+(require 'foo)
diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.rkt b/collects/typed-scheme/typecheck/tc-expr-unit.rkt
index 4e27132da9..06f04b5ebb 100644
--- a/collects/typed-scheme/typecheck/tc-expr-unit.rkt
+++ b/collects/typed-scheme/typecheck/tc-expr-unit.rkt
@@ -5,7 +5,7 @@
 (require syntax/kerncase mzlib/trace
          scheme/match (prefix-in - scheme/contract)
          "signatures.rkt" "tc-envops.rkt" "tc-metafunctions.rkt" "tc-subst.rkt"
-         (types utils convenience union subtype remove-intersect type-table)
+         (types utils convenience union subtype remove-intersect type-table filter-ops)
          (private-in parse-type type-annotation)
          (rep type-rep)
          (only-in (infer infer) restrict)
@@ -170,6 +170,18 @@
 ;;                   (Type Results -> Type)
 ;;                   (Type Type -> Type))
 (define (check-below tr1 expected)     
+  (define (filter-better? f1 f2)
+    (match* (f1 f2)
+      [(f f) #t]
+      [((FilterSet: f1+ f1-) (FilterSet: f2+ f2-))
+       (and (implied-atomic? f2+ f1+)
+            (implied-atomic? f2- f1-))]
+      [(_ _) #f]))
+  (define (object-better? o1 o2)
+    (match* (o1 o2)
+      [(o o) #t]
+      [(o (or (NoObject:) (Empty:))) #t]
+      [(_ _) #f]))
   (define (maybe-abstract r)
     (define l (hash-ref to-be-abstr expected #f))
     (define (sub-one proc i)
@@ -212,12 +224,17 @@
        (cond 
          [(not (subtype t1 t2))
           (tc-error/expr "Expected ~a, but got ~a" t2 t1)]
-         [(and (not (filter-equal? f1 f2))
-               (object-equal? o1 o2))
+         [(and (not (filter-better? f1 f2))
+               (object-better? o1 o2))
           (tc-error/expr "Expected result with filter ~a, got filter ~a" f2 f1)]
-         [(not (and (equal? f1 f2) (equal? 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]
+         [(and (filter-better? f1 f2)
+               (not (object-better? o1 o2)))
+          (tc-error/expr "Expected result with object ~a, got object ~a" o2 o1)]
+         [(and (not (filter-better? f1 f2))
+               (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))]
+         [else
+          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)))