Fix unsound type variable scoping

Closes PR 13123

original commit: 13b831f0ec03f908d836cb1d27aa66c898a8b469

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))

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))

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))

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)))

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))))

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))

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))]
 

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<symbol> -> 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<symbol> option<list<symbol>> -> 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)))

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

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<symbol> type #:original-names list<symbol> -> 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:

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)]))