Disallow non-productive PolyRow types

Closes PR 14554
This commit is contained in:
Asumu Takikawa 2014-06-09 13:55:58 -04:00
parent bbc6a6b42d
commit 4ee5f3f653
4 changed files with 8 additions and 0 deletions

View File

@ -68,6 +68,7 @@
[((Mu: _ body)) (check body)] [((Mu: _ body)) (check body)]
[((Poly: names body)) (check body)] [((Poly: names body)) (check body)]
[((PolyDots: names body)) (check body)] [((PolyDots: names body)) (check body)]
[((PolyRow: _ _ body)) (check body)]
[(_) #t]) [(_) #t])
(unless (check type) (unless (check type)
(tc-error/stx (tc-error/stx

View File

@ -376,6 +376,7 @@
[(Mu: _ body) (loop body)] [(Mu: _ body) (loop body)]
[(Poly: names body) (loop body)] [(Poly: names body) (loop body)]
[(PolyDots: names body) (loop body)] [(PolyDots: names body) (loop body)]
[(PolyRow: _ _ body) (loop body)]
[else #t]))) [else #t])))
(unless productive (unless productive
(parse-error (parse-error

View File

@ -117,6 +117,10 @@
(-polydots (a) ((list) [a a] . ->... . N))] (-polydots (a) ((list) [a a] . ->... . N))]
[(All (a ...) (-> (values a ...))) [(All (a ...) (-> (values a ...)))
(-polydots (a) (t:-> (make-ValuesDots (list) a 'a)))] (-polydots (a) (t:-> (make-ValuesDots (list) a 'a)))]
;; PR 14554, non-productive recursive type
[FAIL (Rec x (All (A #:row) x))]
[(case-lambda (Number -> Boolean) (Number Number -> Number)) (cl-> [(N) B] [(case-lambda (Number -> Boolean) (Number Number -> Number)) (cl-> [(N) B]
[(N N) N])] [(N N) N])]
[(case-> (Number -> Boolean) (Number Number -> Number)) (cl-> [(N) B] [(case-> (Number -> Boolean) (Number Number -> Number)) (cl-> [(N) B]

View File

@ -2616,6 +2616,8 @@
#:msg "Recursive #:implements clause not allowed"] #:msg "Recursive #:implements clause not allowed"]
[tc-err (let () (define-type-alias X (U X #f)) "dummy") [tc-err (let () (define-type-alias X (U X #f)) "dummy")
#:msg "Recursive types are not allowed directly inside"] #:msg "Recursive types are not allowed directly inside"]
[tc-err (let () (define-type-alias X (All (A #:row) X)) "dummy")
#:msg "Recursive types are not allowed directly inside"]
;; Check the more precise Tarjan's algorithm-based letrec-values type checking ;; Check the more precise Tarjan's algorithm-based letrec-values type checking
[tc-e ;; An example from Eric Dobson (see gh372) that shows that precisely [tc-e ;; An example from Eric Dobson (see gh372) that shows that precisely