From 714c628bca89e462c2eb2adef18003a67e7da4ff Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Thu, 13 Dec 2012 14:54:02 -0500 Subject: [PATCH] Fix unsound type variable scoping Closes PR 13123 original commit: 13b831f0ec03f908d836cb1d27aa66c898a8b469 --- collects/tests/typed-racket/fail/pr13123.rkt | 14 +++++ .../fail/type-variable-scope-1.rkt | 10 ++++ .../fail/type-variable-scope-2.rkt | 13 +++++ .../fail/type-variable-scope-3.rkt | 9 ++++ .../typed-racket/succeed/discrete-dist.rkt | 22 ++++++++ .../succeed/type-variable-scope.rkt | 24 +++++++++ .../unit-tests/parse-type-tests.rkt | 5 +- collects/typed-racket/env/tvar-env.rkt | 54 ++++++++++++++++--- collects/typed-racket/private/parse-type.rkt | 2 +- collects/typed-racket/rep/type-rep.rkt | 38 +++++++++++-- .../typed-racket/typecheck/tc-lambda-unit.rkt | 31 ++++++++--- 11 files changed, 202 insertions(+), 20 deletions(-) create mode 100644 collects/tests/typed-racket/fail/pr13123.rkt create mode 100644 collects/tests/typed-racket/fail/type-variable-scope-1.rkt create mode 100644 collects/tests/typed-racket/fail/type-variable-scope-2.rkt create mode 100644 collects/tests/typed-racket/fail/type-variable-scope-3.rkt create mode 100644 collects/tests/typed-racket/succeed/discrete-dist.rkt create mode 100644 collects/tests/typed-racket/succeed/type-variable-scope.rkt diff --git a/collects/tests/typed-racket/fail/pr13123.rkt b/collects/tests/typed-racket/fail/pr13123.rkt new file mode 100644 index 00000000..5ef84986 --- /dev/null +++ b/collects/tests/typed-racket/fail/pr13123.rkt @@ -0,0 +1,14 @@ +#lang typed/racket + +(: unsound-cast (All (a b) (a b -> a))) +(define (unsound-cast w r) + (let: ([x : a w]) + (: set-x (All (a) + (a -> Void))) + (define (set-x y) + (set! x y)) + (set-x r) + x)) + +(: wrong Integer) +(define wrong (unsound-cast 42 'oops)) diff --git a/collects/tests/typed-racket/fail/type-variable-scope-1.rkt b/collects/tests/typed-racket/fail/type-variable-scope-1.rkt new file mode 100644 index 00000000..5ae8837d --- /dev/null +++ b/collects/tests/typed-racket/fail/type-variable-scope-1.rkt @@ -0,0 +1,10 @@ +#; +(exn:pred (lambda (e) (regexp-match? "Expected 1 type variables" e))) +#lang typed/racket + +;; Testing type variable scope + +;; This should fail because of the type variable arities +(: f (All (b) (b -> b))) +(define f + (plambda: (a b) ([x : b]) x)) \ No newline at end of file diff --git a/collects/tests/typed-racket/fail/type-variable-scope-2.rkt b/collects/tests/typed-racket/fail/type-variable-scope-2.rkt new file mode 100644 index 00000000..c7b86e4d --- /dev/null +++ b/collects/tests/typed-racket/fail/type-variable-scope-2.rkt @@ -0,0 +1,13 @@ +#; +(exn:pred (lambda (e) (regexp-match? "Mutation only allowed" e))) +#lang typed/racket + +;; Testing type variable scope + +;; This should fail for the same reason as PR 13123 +(: i (All (x) (x -> x))) +(define i + (plambda: (b) ([x : b]) + (plambda: (b) ([y : b]) + (set! x y)) + x)) \ No newline at end of file diff --git a/collects/tests/typed-racket/fail/type-variable-scope-3.rkt b/collects/tests/typed-racket/fail/type-variable-scope-3.rkt new file mode 100644 index 00000000..bbc388ad --- /dev/null +++ b/collects/tests/typed-racket/fail/type-variable-scope-3.rkt @@ -0,0 +1,9 @@ +#; +(exn:pred (lambda (e) (regexp-match? "Mutation only allowed" e))) +#lang typed/racket + +;; Test type variable scope + +;; The 'a' is bound in two different scopes +(plambda: (a) ([x : a]) + (plambda: (a) ([y : a]) (set! x y))) \ No newline at end of file diff --git a/collects/tests/typed-racket/succeed/discrete-dist.rkt b/collects/tests/typed-racket/succeed/discrete-dist.rkt new file mode 100644 index 00000000..2c5caf5a --- /dev/null +++ b/collects/tests/typed-racket/succeed/discrete-dist.rkt @@ -0,0 +1,22 @@ +#lang typed/racket + +;; A test case boiled down from code in the math collection + +(require racket/promise) + +(: sequence->normalized-weighted-samples + (All (A) (Symbol (Sequenceof A) -> (Values (Listof A) (Listof Positive-Flonum))))) +(define (sequence->normalized-weighted-samples name xs) + ;; the implementation of this is not important for this test + (values (sequence->list xs) '(1.0))) + +(: discrete-dist + ;; the case-> type here causes the problem + (All (A) (case-> ((Sequenceof A) -> (Sequenceof A)) + ((Sequenceof A) (Option (Sequenceof Real)) -> (Sequenceof A))))) +(define (discrete-dist xs [ws #f]) + (let-values ([(xs _) (sequence->normalized-weighted-samples 'discrete-dist xs)]) + ;; the bug this test is supposed to catch causes the + ;; following annotation to fail due to two type variables + ;; not being equal + (ann xs (Listof A)))) diff --git a/collects/tests/typed-racket/succeed/type-variable-scope.rkt b/collects/tests/typed-racket/succeed/type-variable-scope.rkt new file mode 100644 index 00000000..bb77a952 --- /dev/null +++ b/collects/tests/typed-racket/succeed/type-variable-scope.rkt @@ -0,0 +1,24 @@ +#lang typed/racket + +;; Testing type variable scope +;; +;; These should all succeed + +(: f (All (b) (b -> b))) +(define f + (plambda: (a) ([x : a]) x)) + +(: g (All (a) (a -> a))) +(define g + (plambda: (b) ([x : b]) x)) + +(: h (All (x y) (x -> x))) +(define h + (plambda: (a b) ([x : a]) x)) + +(: i (All (x) (x -> x))) +(define i + (plambda: (b) ([x : b]) + (plambda: (b) ([y : b]) + y) + x)) diff --git a/collects/tests/typed-racket/unit-tests/parse-type-tests.rkt b/collects/tests/typed-racket/unit-tests/parse-type-tests.rkt index 93b52fe9..c819613a 100644 --- a/collects/tests/typed-racket/unit-tests/parse-type-tests.rkt +++ b/collects/tests/typed-racket/unit-tests/parse-type-tests.rkt @@ -8,7 +8,8 @@ (base-env base-types base-types-extra colon) (for-template (base-env base-types base-types-extra base-env colon)) (private parse-type) - rackunit) + rackunit + racket/dict) (provide parse-type-tests) @@ -109,7 +110,7 @@ [(Listof Number) (make-Listof N)] - [a (-v a) (cons 'a initial-tvar-env)] + [a (-v a) (dict-set initial-tvar-env 'a (-v a))] [(All (a ...) (a ... -> Number)) (-polydots (a) ((list) [a a] . ->... . N))] diff --git a/collects/typed-racket/env/tvar-env.rkt b/collects/typed-racket/env/tvar-env.rkt index c8dd82d7..1cb0336a 100644 --- a/collects/typed-racket/env/tvar-env.rkt +++ b/collects/typed-racket/env/tvar-env.rkt @@ -5,19 +5,61 @@ ;; this environment maps type variables names (symbols) ;; to types representing the type variable -;; technically, the mapped-to type is unnecessary, but it's convenient to have it around? maybe? +;; +;; The mapped-to type is used to distinguish type variables bound +;; at different scopes -(provide (all-defined-out)) +(require "../utils/utils.rkt" + (rep type-rep) + racket/dict) + +(provide initial-tvar-env + current-tvars + extend-tvars + extend-tvars/new + bound-tvar? + lookup-tvar) ;; the initial type variable environment - empty ;; this is used in the parsing of types -(define initial-tvar-env (list)) +(define initial-tvar-env '()) ;; a parameter for the current type variables (define current-tvars (make-parameter initial-tvar-env)) -;; takes a list of vars +;; extend-tvars +;; takes a list of vars and extends the current type variable +;; environment (define-syntax-rule (extend-tvars vars . body) - (parameterize ([current-tvars (append vars (current-tvars))]) . body)) + (parameterize ([current-tvars (extend/many (current-tvars) vars)]) + . body)) + +;; extend-tvars/new +;; extend with new type variables (provided by, e.g., Poly-fresh:) +(define-syntax-rule (extend-tvars/new vars fresh-vars . body) + (parameterize ([current-tvars + (extend/many (current-tvars) vars fresh-vars)]) + . body)) + +;; bound-tvar? : symbol -> boolean +;; returns #t if the given type variable is bound +(define (bound-tvar? v) + (dict-has-key? (current-tvars) v)) + +;; lookup-tvar : symbol -> type +;; returns the mapped-to type or #f +(define (lookup-tvar var) + (dict-ref (current-tvars) var #f)) + +;; extend : type-env symbol option -> type-env +;; extend type environment with a free type reference +(define (extend env var [fresh-var #f]) + (dict-set env var (make-F (or fresh-var var)))) + +;; extend/many : type-env list option> -> type-env +;; extend type environment for many symbols +(define (extend/many env vars [fresh-vars #f]) + (let ([fresh-vars (or fresh-vars (for/list ([_ vars]) #f))]) + (for/fold ([env env]) ([var vars] [fresh-var fresh-vars]) + (extend env var fresh-var)))) -(define (bound-tvar? v) (memq v (current-tvars))) diff --git a/collects/typed-racket/private/parse-type.rkt b/collects/typed-racket/private/parse-type.rkt index 6fe291c7..036d5cb1 100644 --- a/collects/typed-racket/private/parse-type.rkt +++ b/collects/typed-racket/private/parse-type.rkt @@ -324,7 +324,7 @@ (cond ;; if it's a type variable, we just produce the corresponding reference (which is in the HT) [(bound-tvar? (syntax-e #'id)) - (make-F (syntax-e #'id))] + (lookup-tvar (syntax-e #'id))] ;; if it was in current-indexes, produce a better error msg [(bound-index? (syntax-e #'id)) (tc-error diff --git a/collects/typed-racket/rep/type-rep.rkt b/collects/typed-racket/rep/type-rep.rkt index bb2e429c..908c765a 100644 --- a/collects/typed-racket/rep/type-rep.rkt +++ b/collects/typed-racket/rep/type-rep.rkt @@ -603,10 +603,21 @@ (instantiate (*F name) scope)])) ;; the 'smart' constructor -(define (Poly* names body) +;; +;; Corresponds to closing a type in locally nameless representation +;; (turns free `names` into bound De Bruijn vars) +;; Also keeps track of the original name in a table to recover names +;; for debugging or to correlate with surface syntax +;; +;; Provide #:original-names if the names that you are closing off +;; are *different* from the names you want recorded in the table. +;; +;; list type #:original-names list -> type +;; +(define (Poly* names body #:original-names [orig names]) (if (null? names) body (let ([v (*Poly (length names) (abstract-many names body))]) - (hash-set! name-table v names) + (hash-set! name-table v orig) v))) ;; the 'smart' destructor @@ -667,6 +678,11 @@ (list sym (Mu-body* sym t)))) (list np bp)))]))) +;; These match expanders correspond to opening up a type in +;; locally nameless representation. When the type is opened, +;; the nameless bound variables are replaced with free +;; variables with names. +;; ;; This match expander wraps the smart constructor ;; names are generated with gensym (define-match-expander Poly:* @@ -692,6 +708,21 @@ (list syms (Poly-body* syms t)))) (list nps bp)))]))) +;; This match expander creates new fresh names for exploring the body +;; of the polymorphic type. When lexical scoping of type variables is a concern, you +;; should use this form. +(define-match-expander Poly-fresh: + (lambda (stx) + (syntax-case stx () + [(_ nps freshp bp) + #'(? Poly? + (app (lambda (t) + (let* ([n (Poly-n t)] + [syms (hash-ref name-table t (lambda _ (build-list n (lambda _ (gensym)))))] + [fresh-syms (map gensym syms)]) + (list syms fresh-syms (Poly-body* fresh-syms t)))) + (list nps freshp bp)))]))) + ;; This match expander wraps the smart constructor ;; names are generated with gensym (define-match-expander PolyDots:* @@ -720,7 +751,8 @@ ;(trace subst subst-all) (provide - Mu-name: Poly-names: + Mu-name: + Poly-names: Poly-fresh: PolyDots-names: Type-seq Mu-unsafe: Poly-unsafe: diff --git a/collects/typed-racket/typecheck/tc-lambda-unit.rkt b/collects/typed-racket/typecheck/tc-lambda-unit.rkt index f9ff0443..0587a667 100644 --- a/collects/typed-racket/typecheck/tc-lambda-unit.rkt +++ b/collects/typed-racket/typecheck/tc-lambda-unit.rkt @@ -291,16 +291,28 @@ [(tc-result1: (and v (Values: _))) (maybe-loop form formals bodies (values->tc-results v #f))] [_ (int-err "expected not an appropriate tc-result: ~a" expected)])) (match expected - [(tc-result1: (and t (Poly-names: ns expected*))) + [(tc-result1: (and t (Poly-fresh: ns fresh-ns expected*))) (let* ([tvars (let ([p (plambda-prop form)]) (when (and (pair? p) (eq? '... (car (last p)))) (tc-error "Expected a polymorphic function without ..., but given function had ...")) - (or (and p (map syntax-e (syntax->list p))) - ns))] - [ty (extend-tvars tvars - (maybe-loop form formals bodies (ret expected*)))]) - ;(printf "plambda: ~a ~a ~a \n" literal-tvars new-tvars ty) + (and p (map syntax-e (syntax->list p))))]) + ;; make sure the declared type variable arity matches up with the + ;; annotated type variable arity + (when tvars + (unless (= (length tvars) (length ns)) + (tc-error "Expected ~a type variables, but given ~a" + (length ns) (length tvars)))) + ;; check the bodies appropriately + (if tvars + ;; make both annotated and given type variables point to the + ;; same actual type variables (the fresh names) + (extend-tvars/new ns fresh-ns + (extend-tvars/new tvars fresh-ns + (maybe-loop form formals bodies (ret expected*)))) + ;; no plambda: type variables given + (extend-tvars/new ns fresh-ns + (maybe-loop form formals bodies (ret expected*)))) t)] [(tc-result1: (and t (PolyDots-names: (list ns ... dvar) expected*))) (let-values @@ -325,10 +337,13 @@ (tc/mono-lambda/type formals bodies #f)))]) (make-PolyDots (append tvars (list dotted-var)) ty))] [tvars - (let* ([ty (extend-tvars tvars + (let* (;; manually make some fresh names since + ;; we don't use a match expander + [fresh-tvars (map gensym tvars)] + [ty (extend-tvars/new tvars fresh-tvars (tc/mono-lambda/type formals bodies #f))]) ;(printf "plambda: ~a ~a ~a \n" literal-tvars new-tvars ty) - (make-Poly tvars ty))])] + (make-Poly fresh-tvars ty #:original-names tvars))])] [(tc-result1: t) (check-below (tc/plambda form formals bodies #f) t)] [_ (int-err "not a good expected value: ~a" expected)]))