From dab83ca0b05c14553740a34b1fc4c9189ae7f70c Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Sat, 4 Aug 2012 15:53:21 -0700 Subject: [PATCH] Fill hole in recursive type soundness. Fixes PR 11372. original commit: e6d4fb2ee247cfec157175788ff29f94e6aec3e5 --- .../unit-tests/typecheck-tests.rkt | 5 +++++ collects/typed-racket/private/parse-type.rkt | 19 +++++++++++++------ 2 files changed, 18 insertions(+), 6 deletions(-) diff --git a/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt b/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt index 272f2e4f..4f6dc1b0 100644 --- a/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt +++ b/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt @@ -772,6 +772,11 @@ (if (number? x) (begin (f) (add1 x)) 12))] + + [tc-err (ann 3 (Rec a a))] + [tc-err (ann 3 (Rec a (U a 3)))] + [tc-err (ann 3 (Rec a (Rec b a)))] + #; [tc-err (lambda: ([x : Any]) (if (number? (not (not x))) diff --git a/collects/typed-racket/private/parse-type.rkt b/collects/typed-racket/private/parse-type.rkt index 6e98936c..3b46d9a3 100644 --- a/collects/typed-racket/private/parse-type.rkt +++ b/collects/typed-racket/private/parse-type.rkt @@ -212,14 +212,21 @@ (extend-tvars (list var) (let ([t* (parse-type #'t)]) ;; is t in a productive position? - (unless (match t* - [(Union: es) - (define seq-tvar (Type-seq tvar)) - (not (memf (λ (e) (eq? (Type-seq e) seq-tvar)) es))] - [_ #t]) ; it's fine + (define productive + (let loop ((ty t*)) + (match ty + [(Union: elems) (andmap loop elems)] + [(F: _) (not (equal? ty tvar))] + [(App: rator rands stx) + (loop (resolve-app rator rands stx))] + [(Mu: _ body) (loop body)] + [(Poly: names body) (loop body)] + [(PolyDots: names body) (loop body)] + [else #t]))) + (unless productive (tc-error/stx stx - "Recursive types are not allowed as members of unions directly inside their definition")) + "Recursive types are not allowed directly inside their definition")) (if (memq var (fv t*)) (make-Mu var t*) t*))))]