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

Don't let map introduce type variables.

Browse Source 
Closes PR 13581.

original commit: 67dd956b6acf5533cd2551cac7fd618eca839261
This commit is contained in:
Eric Dobson 2013-03-23 11:13:46 -07:00
parent 929134d7ce
commit 7e7641c8e9
6 changed files with 28 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
collects/tests/typed-racket/fail/pr13581.rkt Normal file
View File

@ -0,0 +1,14 @@
#lang typed/racket
(: g (All (a ...) (a ... a -> (List a ... a))))
(define (g . rst)
(map
;; 'a' is in scope due to map rule
(lambda: ([y : a])
(map
;; in scope again
(lambda: ([z : a])
(set! y z)
z)
rst)
y)
rst))

2
collects/tests/typed-racket/fail/values-dots.rkt
View File

@ -7,7 +7,7 @@
(: map-with-funcs (All (b ...) ((b ... b -> b) ... b -> (b ... b -> (values b ... b)))))
(define (map-with-funcs . fs)
(lambda bs
(apply values (map (lambda: ([f : (b ... b -> b)])
(apply values (map (plambda: (c) ([f : (b ... b -> c)])
(apply f bs)) fs))))
(map-with-funcs (lambda () 1))

2
collects/tests/typed-racket/succeed/nested-poly.rkt
View File

@ -13,7 +13,7 @@
(B ... B -> (values A ... A))))))
(define (map-with-funcs . fs)
(lambda as
(apply values (map (lambda: ([f : (B ... B -> A)])
(apply values (map (plambda: (C) ([f : (B ... B -> C)])
(apply f as))
fs))))

2
collects/tests/typed-racket/succeed/values-dots.rkt
View File

@ -13,7 +13,7 @@
(: map-with-funcs (All (b ...) ((b ... b -> b) ... b -> (b ... b -> (values b ... b)))))
(define (map-with-funcs . fs)
(lambda bs
(apply values (map (lambda: ([f : (b ... b -> b)])
(apply values (map (plambda: (c) ([f : (b ... b -> c)])
(apply f bs)) fs))))
(map-with-funcs + - * /)

8
collects/typed-racket/typecheck/check-below.rkt
View File

@ -95,9 +95,13 @@
(unless (for/and ([t t1] [s t2]) (subtype t s))
(tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
expected]
[((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound))
[((tc-results: t1 f o dty1 dbound) (tc-results: t2 f o dty2 dbound))
(unless (= (length t1) (length t2))
(tc-error/expr "Expected ~a non dotted values, but got ~a" (length t2) (length t1)))
(unless (andmap subtype t1 t2)
(tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
(unless (subtype dty1 dty2)
(tc-error/expr "Expected ~a in ..., but got ~a" dty2 dty1))
expected]
[((tc-results: t1 fs os) (tc-results: t2 fs os))
(unless (= (length t1) (length t2))
@ -136,5 +140,5 @@
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
expected]
[((tc-results: ts fs os dty dbound) (tc-results: ts* fs* os* dty* dbound*))
(int-err "dotted types in check-below nyi: ~a ~a" dty dty*)]
(int-err "dotted types with different bounds/filters/objects in check-below nyi: ~a ~a" tr1 expected)]
[(a b) (int-err "unexpected input for check-below: ~a ~a" a b)]))

7
collects/typed-racket/typecheck/tc-app/tc-app-list.rkt
View File

@ -42,9 +42,12 @@
...))
(=> fail)
(unless (for/and ([b bound]) (or (not b) (eq? bound0 b))) (fail))
;; Do not check this in an environment where bound0 is a type variable.
(define f-type (tc-expr #'f))
;; Check that the function applies successfully to the element type
;; We need the bound to be considered a type var here so that inference works
(match (extend-tvars (list bound0)
;; just check that the function applies successfully to the element type
(tc/funapp #'f #'(arg0 arg ...) (tc-expr #'f) (cons (ret t0) (map ret t)) expected))
(tc/funapp #'f #'(arg0 arg ...) f-type (cons (ret t0) (map ret t)) expected))
[(tc-result1: t) (ret (make-ListDots t bound0))]
[(tc-results: ts)
(tc-error/expr #:return (ret (Un))