From 0386141c38c968c69a7d5978361ac73503dfdd55 Mon Sep 17 00:00:00 2001 From: Vincent St-Amour Date: Fri, 23 Sep 2011 14:39:46 -0400 Subject: [PATCH] Forbid non-productive recursive types. original commit: ef2acecb96900e52c08170f81e5e69eaf9737f8d --- .../typed-racket/fail/non-productive-rec.rkt | 6 ++++++ .../typed-racket/fail/non-productive-rec2.rkt | 19 +++++++++++++++++++ collects/typed-racket/private/parse-type.rkt | 17 +++++++++++++---- 3 files changed, 38 insertions(+), 4 deletions(-) create mode 100644 collects/tests/typed-racket/fail/non-productive-rec.rkt create mode 100644 collects/tests/typed-racket/fail/non-productive-rec2.rkt diff --git a/collects/tests/typed-racket/fail/non-productive-rec.rkt b/collects/tests/typed-racket/fail/non-productive-rec.rkt new file mode 100644 index 00000000..83101903 --- /dev/null +++ b/collects/tests/typed-racket/fail/non-productive-rec.rkt @@ -0,0 +1,6 @@ +#; +(exn-pred 1) + +#lang typed/racket/base +(define-type Hole (Rec Hole (U Number Hole))) +(ann "aaa" Hole) diff --git a/collects/tests/typed-racket/fail/non-productive-rec2.rkt b/collects/tests/typed-racket/fail/non-productive-rec2.rkt new file mode 100644 index 00000000..12e0d20c --- /dev/null +++ b/collects/tests/typed-racket/fail/non-productive-rec2.rkt @@ -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) diff --git a/collects/typed-racket/private/parse-type.rkt b/collects/typed-racket/private/parse-type.rkt index 45046205..b74b1d8f 100644 --- a/collects/typed-racket/private/parse-type.rkt +++ b/collects/typed-racket/private/parse-type.rkt @@ -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 ...))))]