suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Fill hole in recursive type soundness. Fixes PR 11372.

Browse Source
This commit is contained in:
Eric Dobson 2012-08-04 15:53:21 -07:00 committed by Vincent St-Amour
parent 9f453676d1
commit e6d4fb2ee2
2 changed files with 18 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
collects/tests/typed-racket/unit-tests/typecheck-tests.rkt
View File

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

19
collects/typed-racket/private/parse-type.rkt
View File

@ -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*))))]