From 994c54c72252e4d39a2ff1315f5bcc6fcf3075a8 Mon Sep 17 00:00:00 2001
From: Asumu Takikawa <asumu@ccs.neu.edu>
Date: Tue, 30 Sep 2014 18:17:52 -0400
Subject: [PATCH] Fix embarrassing bug in OO subtyping

Subtyping on objects was unsound due to an attempt to
make the algorithm more clever. This was a good lesson in
the danger of premature optimization.
---
 .../typed-racket/types/subtype.rkt            | 28 ++++++++-----------
 .../typed-racket/unit-tests/class-tests.rkt   |  6 ++++
 .../typed-racket/unit-tests/subtype-tests.rkt | 25 ++++++++++++++++-
 3 files changed, 42 insertions(+), 17 deletions(-)

diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
index 95480b8c86..fd70379ad8 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
@@ -605,22 +605,18 @@
          [((Instance: (Class: _ _ field-map method-map augment-map _))
            (Instance: (Class: _ _ field-map* method-map* augment-map* _)))
           (define (subtype-clause? map map*)
-            ;; invariant: map and map* are sorted by key
-            (let loop ([A A0] [map map] [map* map*])
-              (cond [(or (empty? map) (empty? map*)) #t]
-                    [else
-                     (match-define (list name type) (car map))
-                     (match-define (list name* type*) (car map*))
-                     (cond [;; quit if 2nd obj lacks a name in 1st obj
-                            (symbol<? name* name)
-                            #f]
-                           [;; if 1st obj lacks a name in 2nd obj, try
-                            ;; the next one
-                            (symbol<? name name*)
-                            (loop A (cdr map) map*)]
-                           [else
-                            (define A* (subtype* A type type*))
-                            (and A* (loop A* (cdr map) (cdr map*)))])])))
+            (and (for/and ([key+type (in-list map*)])
+                   (match-define (list key type) key+type)
+                   (assq key map))
+                 (let/ec escape
+                   (for/fold ([A A0])
+                             ([key+type (in-list map)])
+                     (match-define (list key type) key+type)
+                     (define result (assq (car key+type) map*))
+                     (or (and (not result) A)
+                         (let ([type* (cadr result)])
+                           (or (subtype* A type type*)
+                               (escape #f))))))))
           (and ;; Note that init & augment clauses don't matter for objects
                (subtype-clause? method-map method-map*)
                (subtype-clause? field-map field-map*))]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt
index ee6abd19f6..ceb73dad82 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt
@@ -735,6 +735,12 @@
            (define x (new c%))
            (void))
          -Void]
+   ;; failing instance subtyping
+   [tc-err (let ()
+             (define x (new (class object% (super-new) (define/public (m) "m"))))
+             (ann x (Object [n (-> String)]))
+             (error "foo"))
+           #:msg #rx"expected: .*n.*given:.*m.*"]
    ;; test use of `this` in field default
    [tc-e (let ()
            (class object%
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/subtype-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/subtype-tests.rkt
index 576ad4ac4a..7eda6560c5 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/subtype-tests.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/subtype-tests.rkt
@@ -312,12 +312,35 @@
    [(-object #:method ((m (-> -Nat)) (n (-> -Nat))))
     (-object #:method ((m (-> -Nat))))]
    [(-object #:method ((f (-> -Nat))) #:augment ((m (-> -Nat)) (n (-> -Nat))))
-    (-object #:method ((m (-> -Nat))))]
+    (-object #:augment ((m (-> -Nat))))]
    [(-object #:field ((a -Nat)) #:method ((m (-> -Nat)) (n (-> -Nat))))
     (-object #:method ((m (-> -Nat))))]
+   [(-object #:field ((x -Symbol)))
+    (-object #:field ((x -Symbol)))]
+   [(-object #:field ((x -Symbol)))
+    (-object #:field ((x (Un -Symbol (-val #f)))))]
+   [FAIL
+    (-object #:field ((a -Symbol)))
+    (-object #:field ((x -Symbol)))]
+   [FAIL
+    (-object #:field ((a -Symbol)))
+    (-object #:field ((x -String)))]
+   [FAIL
+    (-object #:field ((x -Symbol)))
+    (-object #:field ((x -String)))]
+   [FAIL
+    (-object #:method ((m (-> -String)) (n (-> -String))))
+    (-object #:method ((x (-> -String))))]
+   [(-object #:method ((m (-> -String)) (n (-> -String))))
+    (-object #:method ((m (-> -String))))]
+   [FAIL
+    (-object #:method ())
+    (-object #:method ((m (-> -String))))]
    [FAIL
     (-object #:method ((m (-> -Nat)) (n (-> -Nat))))
     (-object #:method ((l (-> -Nat)) (m (-> -Nat))))]
+   [(-object #:method ((m (-> -Nat)) (n (-> -Nat))))
+    (-object #:method ((n (-> -Nat)) (m (-> -Nat))))]
    [FAIL
     (-class #:method ((m (-> -Nat))))
     (-class #:method ((m (-> -Nat))) #:augment ((m (-> -Nat))))]