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.
This commit is contained in:
Asumu Takikawa 2014-09-30 18:17:52 -04:00
parent 96714934b6
commit 994c54c722
3 changed files with 42 additions and 17 deletions

View File

@ -605,22 +605,18 @@
[((Instance: (Class: _ _ field-map method-map augment-map _)) [((Instance: (Class: _ _ field-map method-map augment-map _))
(Instance: (Class: _ _ field-map* method-map* augment-map* _))) (Instance: (Class: _ _ field-map* method-map* augment-map* _)))
(define (subtype-clause? map map*) (define (subtype-clause? map map*)
;; invariant: map and map* are sorted by key (and (for/and ([key+type (in-list map*)])
(let loop ([A A0] [map map] [map* map*]) (match-define (list key type) key+type)
(cond [(or (empty? map) (empty? map*)) #t] (assq key map))
[else (let/ec escape
(match-define (list name type) (car map)) (for/fold ([A A0])
(match-define (list name* type*) (car map*)) ([key+type (in-list map)])
(cond [;; quit if 2nd obj lacks a name in 1st obj (match-define (list key type) key+type)
(symbol<? name* name) (define result (assq (car key+type) map*))
#f] (or (and (not result) A)
[;; if 1st obj lacks a name in 2nd obj, try (let ([type* (cadr result)])
;; the next one (or (subtype* A type type*)
(symbol<? name name*) (escape #f))))))))
(loop A (cdr map) map*)]
[else
(define A* (subtype* A type type*))
(and A* (loop A* (cdr map) (cdr map*)))])])))
(and ;; Note that init & augment clauses don't matter for objects (and ;; Note that init & augment clauses don't matter for objects
(subtype-clause? method-map method-map*) (subtype-clause? method-map method-map*)
(subtype-clause? field-map field-map*))] (subtype-clause? field-map field-map*))]

View File

@ -735,6 +735,12 @@
(define x (new c%)) (define x (new c%))
(void)) (void))
-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 ;; test use of `this` in field default
[tc-e (let () [tc-e (let ()
(class object% (class object%

View File

@ -312,12 +312,35 @@
[(-object #:method ((m (-> -Nat)) (n (-> -Nat)))) [(-object #:method ((m (-> -Nat)) (n (-> -Nat))))
(-object #:method ((m (-> -Nat))))] (-object #:method ((m (-> -Nat))))]
[(-object #:method ((f (-> -Nat))) #:augment ((m (-> -Nat)) (n (-> -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 #:field ((a -Nat)) #:method ((m (-> -Nat)) (n (-> -Nat))))
(-object #:method ((m (-> -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 [FAIL
(-object #:method ((m (-> -Nat)) (n (-> -Nat)))) (-object #:method ((m (-> -Nat)) (n (-> -Nat))))
(-object #:method ((l (-> -Nat)) (m (-> -Nat))))] (-object #:method ((l (-> -Nat)) (m (-> -Nat))))]
[(-object #:method ((m (-> -Nat)) (n (-> -Nat))))
(-object #:method ((n (-> -Nat)) (m (-> -Nat))))]
[FAIL [FAIL
(-class #:method ((m (-> -Nat)))) (-class #:method ((m (-> -Nat))))
(-class #:method ((m (-> -Nat))) #:augment ((m (-> -Nat))))] (-class #:method ((m (-> -Nat))) #:augment ((m (-> -Nat))))]