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))