From 905d3550653f9e90ca7743ee6d9496603c8e4a13 Mon Sep 17 00:00:00 2001
From: Asumu Takikawa <asumu@ccs.neu.edu>
Date: Sat, 11 Jan 2014 00:56:18 -0500
Subject: [PATCH] Fix subtyping for keyword function types

Closes PR 14252
Closes PR 14257

original commit: 0efd90f846913d87aba53d9d73483960a98e63a8
---
 .../typed-racket/types/subtype.rkt            | 26 +++++++++-----
 .../typed-racket/unit-tests/subtype-tests.rkt | 34 +++++++++++++++++++
 2 files changed, 52 insertions(+), 8 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 73e3b1f3..a6193143 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
@@ -66,23 +66,33 @@
         (syntax/loc stx (let*/and (clauses ...)
 			   A-last))))]))
 
+;; kw-subtypes : (Listof (Pairof Num Num)) (Listof Keyword) (Listof Keyword)
+;;               -> (Option (Listof (Pairof Num Num)))
+;;
+;; Given function types F_s and F_t, this procedure is called to check that the
+;; keyword types t-kws for F_t are subtypes of the keyword types s-kws for F_s
+;; when checking that F_s <: F_t (but *not* F_t <: F_s).
+;;
+;; Note that in terms of width, s-kws may have more keywords (i.e., F_s accepts
+;; all keywords that F_t does) but the types in s-kws must be supertypes of those
+;; in t-kws (i.e., F_s domain types are at least as permissive as those of F_t).
 (define (kw-subtypes* A0 t-kws s-kws)
   (let loop ([A A0] [t t-kws] [s s-kws])
     (and
      A
      (match* (t s)
-       [((list (Keyword: kt tt rt) rest-t) (list (Keyword: ks ts rs) rest-s))
+       [((cons (Keyword: kt tt rt) rest-t) (cons (Keyword: ks ts rs) rest-s))
 	(cond [(eq? kt ks)
-	       (and ;; if s is optional, t must be as well
-		(or rs (not rt))
+	       (and ;; if t is optional, s must be as well
+		(or rt (not rs))
 		(loop (subtype* A tt ts) rest-t rest-s))]
-	      ;; extra keywords in t are ok
+	      ;; optional extra keywords in s are ok
 	      ;; we just ignore them
-	      [(keyword<? kt ks) (loop A rest-t s)]
-	      ;; extra keywords in s are a problem
+	      [(and (not rs) (keyword<? ks kt)) (loop A t rest-s)]
+	      ;; extra keywords in t are a problem
 	      [else #f])]
-       ;; no more keywords to satisfy
-       [(_ '()) A]
+       ;; no more keywords to satisfy, the rest in t must be optional
+       [('() _) (and (andmap (match-lambda [(Keyword: _ _ rs) (not rs)]) s) A)]
        ;; we failed to satisfy all the keyword
        [(_ _) #f]))))
 
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 76828af6..d9552c96 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
@@ -253,4 +253,38 @@
    [FAIL (make-ListDots (-box (make-F 'a)) 'a) (-lst (-box Univ))]
    [(make-ListDots (-> -Symbol (make-F 'a)) 'a) (-lst (-> -Symbol Univ))]
 
+   ;; keyword function types
+   [(->key #:x -Symbol #f Univ) (->key Univ)]
+   [FAIL (->key #:x -Symbol #t Univ) (->key Univ)]
+   [FAIL (->key Univ) (->key #:x -Symbol #t Univ)]
+   [(->key #:x -Symbol #f #:y -Symbol #f Univ) (->key Univ)]
+   [FAIL (->key #:x -Symbol #f #:y -Symbol #t Univ) (->key Univ)]
+   [(->key #:x -Symbol #f #:y -Symbol #f Univ) (->key #:x -Symbol #f Univ)]
+   [(->key #:x -Symbol #f #:y -Symbol #f Univ) (->key #:x -Symbol #t Univ)]
+   [FAIL (->key #:x -Symbol #f Univ) (->key #:x -Symbol #f #:y -Symbol #f Univ)]
+   [(->key #:x -Symbol #f #:y -Symbol #f Univ)
+    (->key #:x -Symbol #t #:y -Symbol #t Univ)]
+   [FAIL
+    (->key #:x -Symbol #t #:y -Symbol #f Univ)
+    (->key #:x -Symbol #f #:y -Symbol #t Univ)]
+   [(->key #:x (-opt -String) #f #:y -Symbol #f Univ)
+    (->key #:x -String #t Univ)]
+   [FAIL
+    (->key #:x -String #f #:y -Symbol #f Univ)
+    (->key #:x (-opt -String) #t Univ)]
+   [(->key -String #:x -Symbol #f #:y -Symbol #f Univ)
+    (->key -String #:x -Symbol #t Univ)]
+   [FAIL
+    (->key -String #:x -Symbol #f #:y -Symbol #f Univ)
+    (->key -Void #:x -Symbol #t Univ)]
+   [(->optkey -String [-String] #:x -Symbol #f #:y -Symbol #f Univ)
+    (->key -String #:x -Symbol #t Univ)]
+   [(->optkey -String [-String] #:x -Symbol #f #:y -Symbol #f Univ)
+    (->optkey -String [-String] #:x -Symbol #t Univ)]
+   [FAIL
+    (->optkey -String [-String] #:x -Symbol #f #:y -Symbol #f Univ)
+    (->optkey -String [-Void] #:x -Symbol #t Univ)]
+   [FAIL
+    (->key -String #:x -Symbol #f #:y -Symbol #f Univ)
+    (->optkey -String [-Void] #:x -Symbol #t Univ)]
    ))