From 92c48f65211c6fe68fe124539006df4fb0207bca Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 28 May 2010 11:53:54 -0400 Subject: [PATCH] Subtyping between (List T ... a) and (Listof T[Any/a]) original commit: fd5a662ccc7aa2fbc3f29974c075dcabf2a870fe --- collects/tests/typed-scheme/succeed/list-dots.rkt | 9 +++++++++ collects/typed-scheme/types/subtype.rkt | 2 ++ 2 files changed, 11 insertions(+) diff --git a/collects/tests/typed-scheme/succeed/list-dots.rkt b/collects/tests/typed-scheme/succeed/list-dots.rkt index a6fe64aa..4b3ac8b8 100644 --- a/collects/tests/typed-scheme/succeed/list-dots.rkt +++ b/collects/tests/typed-scheme/succeed/list-dots.rkt @@ -7,3 +7,12 @@ (define (g . x) x) (g 7 7 7) + +(: h (All (a ...) (a ... -> (Listof Any)))) +(define (h . x) x) + +(: h2 (All (a ...) ((Pair String a) ... -> (Listof (Pair String Any))))) +(define (h2 . x) x) + +(: h3 (All (a ...) ((Pair String a) ... -> (Listof Any)))) +(define (h3 . x) x) diff --git a/collects/typed-scheme/types/subtype.rkt b/collects/typed-scheme/types/subtype.rkt index 36c939c1..7b5d91de 100644 --- a/collects/typed-scheme/types/subtype.rkt +++ b/collects/typed-scheme/types/subtype.rkt @@ -298,6 +298,8 @@ ;; recur structurally on dotted lists, assuming same bounds [((ListDots: s-dty dbound) (ListDots: t-dty dbound)) (subtype* A0 s-dty t-dty)] + [((ListDots: s-dty dbound) (Listof: t-elem)) + (subtype* A0 (substitute Univ dbound s-dty) t-elem)] ;; quantification over two types preserves subtyping [((Poly: ns b1) (Poly: ms b2)) (=> unmatch)