Forbid non-productive recursive types.
This commit is contained in:
parent
3851727c73
commit
ef2acecb96
6
collects/tests/typed-racket/fail/non-productive-rec.rkt
Normal file
6
collects/tests/typed-racket/fail/non-productive-rec.rkt
Normal file
|
@ -0,0 +1,6 @@
|
||||||
|
#;
|
||||||
|
(exn-pred 1)
|
||||||
|
|
||||||
|
#lang typed/racket/base
|
||||||
|
(define-type Hole (Rec Hole (U Number Hole)))
|
||||||
|
(ann "aaa" Hole)
|
19
collects/tests/typed-racket/fail/non-productive-rec2.rkt
Normal file
19
collects/tests/typed-racket/fail/non-productive-rec2.rkt
Normal 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)
|
|
@ -200,10 +200,19 @@
|
||||||
[tvar (make-F var)])
|
[tvar (make-F var)])
|
||||||
(add-disappeared-use #'kw)
|
(add-disappeared-use #'kw)
|
||||||
(extend-tvars (list var)
|
(extend-tvars (list var)
|
||||||
(let ([t (parse-type #'t)])
|
(let ([t* (parse-type #'t)])
|
||||||
(if (memq var (fv t))
|
;; is t in a productive position?
|
||||||
(make-Mu var t)
|
(unless (match t*
|
||||||
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 ...)
|
[((~and kw t:U) ts ...)
|
||||||
(add-disappeared-use #'kw)
|
(add-disappeared-use #'kw)
|
||||||
(apply Un (map parse-type (syntax->list #'(ts ...))))]
|
(apply Un (map parse-type (syntax->list #'(ts ...))))]
|
||||||
|
|
Loading…
Reference in New Issue
Block a user