From 6512b52b1d6e7ecdad11e23fc6f6697d5ccfbf7f Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Fri, 7 Aug 2015 12:08:45 -0400 Subject: [PATCH] Fix polymorphic recursion check for type aliases The old check was broken for cases with type constructors with more than one type argument and was also too conservative in some cases (e.g., when one cycle refers to another cycle of aliases in a non-recursive manner). The new check is still conservative, but it allows more types than before. Closes GH issue #157 --- .../typed-racket/env/type-alias-helper.rkt | 11 ++++++++- .../typed-racket/types/resolve.rkt | 23 +++++++++++-------- .../fail/polymorphic-recursion-4.rkt | 19 +++++++++++++++ typed-racket-test/succeed/gh-issue-157.rkt | 10 ++++++++ 4 files changed, 53 insertions(+), 10 deletions(-) create mode 100644 typed-racket-test/fail/polymorphic-recursion-4.rkt create mode 100644 typed-racket-test/succeed/gh-issue-157.rkt diff --git a/typed-racket-lib/typed-racket/env/type-alias-helper.rkt b/typed-racket-lib/typed-racket/env/type-alias-helper.rkt index 72477092..5f7e851e 100644 --- a/typed-racket-lib/typed-racket/env/type-alias-helper.rkt +++ b/typed-racket-lib/typed-racket/env/type-alias-helper.rkt @@ -217,6 +217,13 @@ (define (reset-resolver-cache!) (resolver-cache-remove! name-types)) (reset-resolver-cache!) + ;; Checks whether two aliases are in the same connected component. + ;; Used for the polymorphic recursion check below. + (define (in-same-component? id id2) + (for/or ([component (in-list (append components class-components))]) + (and (member id component free-identifier=?) + (member id2 component free-identifier=?)))) + ;; Finish registering recursive aliases ;; names-to-refine : Listof ;; types-to-refine : Listof @@ -229,7 +236,9 @@ (define type ;; make sure to reject the type if it uses polymorphic ;; recursion (see resolve.rkt) - (parameterize ([current-check-polymorphic-recursion args]) + (parameterize ([current-check-polymorphic-recursion + `#s(poly-rec-info ,(λ (id2) (in-same-component? id id2)) + ,args)]) (parse-type type-stx))) (reset-resolver-cache!) (register-type-name id type) diff --git a/typed-racket-lib/typed-racket/types/resolve.rkt b/typed-racket-lib/typed-racket/types/resolve.rkt index 2ff8c20d..e507bd45 100644 --- a/typed-racket-lib/typed-racket/types/resolve.rkt +++ b/typed-racket-lib/typed-racket/types/resolve.rkt @@ -17,14 +17,16 @@ (define-struct poly (name vars) #:prefab) -;; Parameter>> +;; (Parameter (Option Poly-Rec-Info)) ;; This parameter controls whether or not the resolving process ;; should check for polymorphic recursion in implicit recursive ;; type names. This should only need to be enabled at type alias ;; definition time. ;; -;; If not #f, it should be a list of symbols that correspond -;; to the type parameters of the type being parsed. +;; If not #f, it should be a record of a procedure that checks if an +;; alias is in the same connected component as the original alias +;; and a list of symbols that correspond to the type parameters of +;; the type being parsed. (define current-check-polymorphic-recursion (make-parameter #f)) (define (resolve-name t) @@ -60,7 +62,7 @@ " does not match the given number:" " expected " num-poly ", given " num-rands))))] - [(Name: _ num-args #f) + [(Name: name-id num-args #f) (cond [(> num-args 0) (define num-rands (length rands)) (unless (= num-rands num-args) @@ -92,15 +94,18 @@ ;; Check argument to make sure there's no polymorphic recursion (define (check-argument given-type arg-name) (define ok? - (if (F? given-type) - (type-equal? given-type (make-F (syntax-e arg-name))) + (or (F? given-type) (not (member (syntax-e arg-name) (fv given-type))))) (unless ok? (tc-error (~a "Recursive type " rator " cannot be applied at" " a different type in its recursive invocation")))) - (define current-vars (current-check-polymorphic-recursion)) - (when current-vars - (for-each check-argument rands current-vars))] + (match (current-check-polymorphic-recursion) + [`#s(poly-rec-info ,same-component? ,current-vars) + #:when (same-component? name-id) + (for* ([rand (in-list rands)] + [var (in-list current-vars)]) + (check-argument rand var))] + [_ (void)])] [else (tc-error "Type ~a cannot be applied, arguments were: ~a" rator rands)])] [(Mu: _ _) (void)] diff --git a/typed-racket-test/fail/polymorphic-recursion-4.rkt b/typed-racket-test/fail/polymorphic-recursion-4.rkt new file mode 100644 index 00000000..74572201 --- /dev/null +++ b/typed-racket-test/fail/polymorphic-recursion-4.rkt @@ -0,0 +1,19 @@ +#; +(exn-pred #rx"applied at a different type") +#lang typed/racket + +;; These aliases should be not allowed because there's +;; polymorphic recursion +;; +;; Related to GH issue #157 + +(define-type (a T U) (-> (b U))) +(define-type (b T) (-> (a (Listof T) (Listof T)))) + +;; Because the check is conservative, there are some types +;; that are disallowed even if they are ok. Here is one +;; example: + +(define-type (c T U) (-> (d U))) +;; ok because (Listof T) is thrown away +(define-type (d T) (-> (c (Listof T) Integer))) diff --git a/typed-racket-test/succeed/gh-issue-157.rkt b/typed-racket-test/succeed/gh-issue-157.rkt new file mode 100644 index 00000000..1b72bfea --- /dev/null +++ b/typed-racket-test/succeed/gh-issue-157.rkt @@ -0,0 +1,10 @@ +#lang typed/racket + +;; These aliases should be allowed because there's no +;; polymorphic recursion +;; +;; Tests for GH issue #157 + +(define-type (a T U) (-> (b U))) +(define-type (b T) (-> (a T Integer))) +(define-type (c T) (a (c T) Number))