Forbid non-productive recursive types.

original commit: ef2acecb96900e52c08170f81e5e69eaf9737f8d
This commit is contained in:
Vincent St-Amour 2011-09-23 14:39:46 -04:00
parent cd4b331886
commit 0386141c38
3 changed files with 38 additions and 4 deletions

View File

@ -0,0 +1,6 @@
#;
(exn-pred 1)
#lang typed/racket/base
(define-type Hole (Rec Hole (U Number Hole)))
(ann "aaa" Hole)

View File

@ -0,0 +1,19 @@
#;
(exn-pred 1)
#lang typed/racket
(define-struct: node ({left : Tree} {right : Tree}) #:transparent)
(define-type Tree (Rec Tree (U Number Tree)))
;; Tree = Number | (node Tree Tree)
(: tree-sum (Tree -> Number))
;; sum up all numbers in the tree
(define (tree-sum t)
(cond
[(number? t) t]
[else (+ (tree-sum (node-left t)) (tree-sum (node-right t)))]))
(define n (node (node 12000000000000.1 .0000000000000000000000001) 2))
(tree-sum n)

View File

@ -200,10 +200,19 @@
[tvar (make-F var)])
(add-disappeared-use #'kw)
(extend-tvars (list var)
(let ([t (parse-type #'t)])
(if (memq var (fv t))
(make-Mu var t)
t))))]
(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
(tc-error/stx
stx
"Recursive types are not allowed as members of unions directly inside their definition"))
(if (memq var (fv t*))
(make-Mu var t*)
t*))))]
[((~and kw t:U) ts ...)
(add-disappeared-use #'kw)
(apply Un (map parse-type (syntax->list #'(ts ...))))]