From c70910aaa0872aef6051a524f9a98385e932165b Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Wed, 1 Apr 2015 18:51:40 -0400 Subject: [PATCH] Fix type restriction in values->tc-results Previously the restriction didn't account for traversing the object type with the given path. This also relies on the previous commit that adds subtyping on filters. (because this change seems to introduce filters which only differ by an unrolling of a recursive type, but the old subtyping only worked for identical types) --- .../typed-racket/typecheck/tc-subst.rkt | 12 ++++++++++-- .../unit-tests/metafunction-tests.rkt | 15 +++++++++++++++ 2 files changed, 25 insertions(+), 2 deletions(-) diff --git a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt index 7c29118c..31d3b1f0 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt @@ -6,7 +6,8 @@ (require "../utils/utils.rkt" racket/match racket/list (contract-req) - (except-in (types abbrev utils filter-ops) -> ->* one-of/c) + (except-in (types abbrev utils filter-ops path-type) + -> ->* one-of/c) (only-in (infer infer) restrict) (rep type-rep object-rep filter-rep rep-utils)) @@ -135,8 +136,15 @@ [(Empty:) (if polarity -top -bot)] [_ + ;; `ty` alone doesn't account for the path, so + ;; first traverse it with the path to match `t` + (define ty/path (path-type p ty)) (maker - (restrict ty (subst-type t k o polarity ty)) + ;; don't restrict if the path doesn't match the type + (if (equal? ty/path Err) + (subst-type t k o polarity ty) + (restrict ty/path + (subst-type t k o polarity ty))) (-acc-path p o))])] [(index-free-in? k t) (if polarity -top -bot)] [else f])) diff --git a/typed-racket-test/unit-tests/metafunction-tests.rkt b/typed-racket-test/unit-tests/metafunction-tests.rkt index 7d692f11..cf02e5a4 100644 --- a/typed-racket-test/unit-tests/metafunction-tests.rkt +++ b/typed-racket-test/unit-tests/metafunction-tests.rkt @@ -151,6 +151,21 @@ (values->tc-results (make-Values (list (-result -Boolean (-FS (-filter -PosReal '(0 0)) (-filter -NonPosReal '(0 0)))))) (list (make-Path null #'x)) (list -Integer)) (ret -Boolean (-FS (-filter -PosInt #'x) (-filter -NonPosInt #'x)))) + + ;; Filter restriction accounts for paths + (check-equal? + (values->tc-results + (make-Values + (list (-result -Boolean + (-FS (make-TypeFilter -PosReal + (make-Path (list -car) '(0 0))) + (make-TypeFilter -NonPosReal + (make-Path (list -car) '(0 0))))))) + (list (make-Path null #'x)) + (list (-lst -Integer))) + (ret -Boolean + (-FS (make-TypeFilter -PosInt (make-Path (list -car) #'x)) + (make-TypeFilter -NonPosInt (make-Path (list -car) #'x))))) ) (test-suite "replace-names"