From 57a60ad4037d0f31d27b2eb1d41be9c710e68d2d Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Tue, 26 Feb 2013 22:25:28 -0800 Subject: [PATCH] Make PolyDots actually subtype correctly. original commit: 6335de099e7161447ec444ad320c6751f2c2af4d --- .../typed-racket/unit-tests/subtype-tests.rkt | 21 ++++++++++++ collects/typed-racket/base-env/base-env.rkt | 6 ++-- collects/typed-racket/types/substitute.rkt | 3 +- collects/typed-racket/types/subtype.rkt | 33 +++++++++++++++++-- 4 files changed, 57 insertions(+), 6 deletions(-) diff --git a/collects/tests/typed-racket/unit-tests/subtype-tests.rkt b/collects/tests/typed-racket/unit-tests/subtype-tests.rkt index a4e5e1f1..67091af6 100644 --- a/collects/tests/typed-racket/unit-tests/subtype-tests.rkt +++ b/collects/tests/typed-racket/unit-tests/subtype-tests.rkt @@ -185,6 +185,27 @@ [FAIL -Fixnum (-seq -Fixnum)] [FAIL -NonNegFixnum (-seq -Index)] [FAIL (-val 5.0) (-seq -Nat)] + + [(-polydots (a) (->... (list Univ) (a a) (make-ValuesDots null a 'a))) + (-polydots (a) (->... (list -String) (a a) (make-ValuesDots null a 'a)))] + + [(-polydots (a) (->... null (Univ a) (make-ValuesDots (list (-result a)) a 'a))) + (-polydots (a) (->... null (-String a) (make-ValuesDots (list (-result a)) a 'a)))] + + [(-polydots (a) (->... null (a a) (make-ValuesDots (list (-result -String)) -String 'a))) + (-polydots (a) (->... null (a a) (make-ValuesDots (list (-result Univ)) Univ 'a)))] + + [(-polydots (a) (->... null (Univ a) (-values (list Univ)))) + (->* null Univ Univ)] + + + [(-polydots (a) (->... null (a a) (make-ListDots a 'a))) + (-> -String -Symbol (-Tuple (list -String -Symbol)))] + [(-> -String -Symbol (-Tuple (list -String -Symbol))) + (-polydots (a) (-> -String -Symbol (-lst (Un -String -Symbol))))] + + [(-polydots (a) (->... null (a a) (make-ListDots a 'a))) + (-poly (a b) (-> a b (-Tuple (list a b))))] )) (define-go diff --git a/collects/typed-racket/base-env/base-env.rkt b/collects/typed-racket/base-env/base-env.rkt index 081043b9..1c893aa2 100644 --- a/collects/typed-racket/base-env/base-env.rkt +++ b/collects/typed-racket/base-env/base-env.rkt @@ -1392,8 +1392,10 @@ -[values (-polydots (b a) (cl->* (->acc (list b) b null) - (null (a a) . ->... . (make-ValuesDots null a 'a))))] +[values (-polydots (a b) (cl->* + (-> (-values null)) + (->acc (list a) a null) + ((list a) (b b) . ->... . (make-ValuesDots (list (-result a)) b 'b))))] [call-with-values (-polydots (b a) ((-> (make-ValuesDots null a 'a)) (null (a a) . ->... . b) . -> . b))] [read-accept-reader (-Param B B)] diff --git a/collects/typed-racket/types/substitute.rkt b/collects/typed-racket/types/substitute.rkt index d9253720..47174599 100644 --- a/collects/typed-racket/types/substitute.rkt +++ b/collects/typed-racket/types/substitute.rkt @@ -135,7 +135,8 @@ ;; substitute-dotted : Type Name Name Type -> Type (define (substitute-dotted image image-bound name target) (define (sb t) (substitute-dotted image image-bound name t)) - (if (set-member? (free-vars-names (free-idxs* target)) name) + (if (or (set-member? (free-vars-names (free-idxs* target)) name) + (set-member? (free-vars-names (free-vars* target)) name)) (type-case (#:Type sb #:Filter (sub-f sb)) target [#:ValuesDots types dty dbound diff --git a/collects/typed-racket/types/subtype.rkt b/collects/typed-racket/types/subtype.rkt index e933fe37..6b9f1a4f 100644 --- a/collects/typed-racket/types/subtype.rkt +++ b/collects/typed-racket/types/subtype.rkt @@ -7,6 +7,7 @@ (env type-name-env) racket/match unstable/match racket/function + racket/list racket/lazy-require (prefix-in c: racket/contract) (for-syntax racket/base syntax/parse)) @@ -357,15 +358,38 @@ [((Poly: ns b1) (Poly: ms b2)) (=> unmatch) (unless (= (length ns) (length ms)) - (unmatch)) + (unmatch)) (subtype* A0 b1 (subst-all (make-simple-substitution ms (map make-F ns)) b2))] + [((PolyDots: (list ns ... n-dotted) b1) + (PolyDots: (list ms ... m-dotted) b2)) + (=> unmatch) + (unless (= (length ns) (length ms)) + (unmatch)) + (define subst + (hash-set (make-simple-substitution ms (map make-F ns)) + m-dotted (i-subst/dotted null (make-F n-dotted) n-dotted))) + (subtype* A0 b1 (subst-all subst b2))] + [((PolyDots: (list ns ... n-dotted) b1) + (Poly: (list ms ...) b2)) + (=> unmatch) + (unless (<= (length ns) (length ms)) + (unmatch)) + (define subst + (hash-set (make-simple-substitution ns (map make-F (take ms (length ns)))) + n-dotted (i-subst (map make-F (drop ms (length ns)))))) + (subtype* A0 (subst-all subst b1) b2)] [((Refinement: par _ _) t) (subtype* A0 par t)] ;; use unification to see if we can use the polytype here [((Poly: vs b) s) (=> unmatch) (if (infer vs null (list b) (list s) (make-Univ)) A0 (unmatch))] - [(s (Poly: vs b)) + [((PolyDots: (list vs ... vdotted) b) s) + (=> unmatch) + (if (infer vs (list vdotted) (list b) (list s) (make-Univ) ) + A0 + (unmatch))] + [(s (or (Poly: vs b) (PolyDots: vs b))) (=> unmatch) (if (null? (fv b)) (subtype* A0 s b) (unmatch))] ;; rec types, applications and names (that aren't the same) @@ -477,7 +501,9 @@ (subtype* A0 parent other)] ;; subtyping on values is pointwise [((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)] - [((or (Values: _) (AnyValues:)) (AnyValues:)) A0] + [((ValuesDots: s-rs s-dty dbound) (ValuesDots: t-rs t-dty dbound)) + (subtype* (subtypes* A0 s-rs t-rs) s-dty t-dty)] + [((or (ValuesDots: _ _ _) (Values: _) (AnyValues:)) (AnyValues:)) A0] ;; trivial case for Result [((Result: t f o) (Result: t* f o)) (subtype* A0 t t*)] @@ -513,6 +539,7 @@ (provide type-compare? subtypes/varargs subtypes) +;(require racket/trace) ;(trace subtype*) ;(trace supertype-of-one/arr) ;(trace arr-subtype*/no-fail)