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-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<Id>
   ;; types-to-refine : Listof<Type>
@@ -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)

typed-racket-lib/typed-racket/types/resolve.rkt

@@ -17,14 +17,16 @@
 
 (define-struct poly (name vars) #:prefab)
 
-;; Parameter<Option<Listof<Symbol>>>
+;; (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)]

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

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