From 1e98e1c1fd415efb9a9497989f0769e51fa8428d Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 28 May 2010 14:11:32 -0400 Subject: [PATCH] Add index-env. - Remove Dotted and DottedBoth values from tvar-env - Abstract env extension and lookup for tvar/index-env - Abstract index inference - Remove pointless parameterizations original commit: d570006db81dda68e69b7058fd3edfb68cc3d042 --- collects/typed-scheme/env/index-env.rkt | 31 ++++ collects/typed-scheme/env/tvar-env.rkt | 13 +- collects/typed-scheme/infer/infer-unit.rkt | 9 +- collects/typed-scheme/private/parse-type.rkt | 156 +++++++----------- collects/typed-scheme/private/with-types.rkt | 2 - collects/typed-scheme/tc-setup.rkt | 2 - collects/typed-scheme/typecheck/tc-app.rkt | 16 +- .../typed-scheme/typecheck/tc-expr-unit.rkt | 11 +- .../typed-scheme/typecheck/tc-lambda-unit.rkt | 49 ++---- .../typed-scheme/typecheck/tc-structs.rkt | 8 +- collects/typed-scheme/types/utils.rkt | 18 +- 11 files changed, 143 insertions(+), 172 deletions(-) create mode 100644 collects/typed-scheme/env/index-env.rkt diff --git a/collects/typed-scheme/env/index-env.rkt b/collects/typed-scheme/env/index-env.rkt new file mode 100644 index 00000000..c2237755 --- /dev/null +++ b/collects/typed-scheme/env/index-env.rkt @@ -0,0 +1,31 @@ +#lang racket/base + +;; this implements the Theta environment from the TOPLAS paper + +;; 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? + +(require racket/require "type-env-structs.rkt" (path-up "utils/tc-utils.rkt" "rep/type-rep.rkt")) +(provide (all-defined-out)) + +;; the initial type variable environment - empty +;; this is used in the parsing of types +(define initial-index-env (make-empty-env #hasheq())) + +;; a parameter for the current type variables +(define current-indexes (make-parameter initial-index-env)) + +;; takes a single index +(define-syntax-rule (extend-indexes index . body) + (parameterize ([current-indexes (extend (current-indexes) index (make-F index))]) . body)) + +(define (bound-index? v) (lookup (current-indexes) v (lambda (_) #f))) + +(define (infer-index stx) + (define bounds (env-keys+vals (current-indexes))) + (when (null? bounds) + (tc-error/stx stx "No type variable bound with ... in scope for ... type")) + (unless (null? (cdr bounds)) + (tc-error/stx stx "Cannot infer bound for ... type")) + (car (car bounds))) \ No newline at end of file diff --git a/collects/typed-scheme/env/tvar-env.rkt b/collects/typed-scheme/env/tvar-env.rkt index f457e70c..dbe26849 100644 --- a/collects/typed-scheme/env/tvar-env.rkt +++ b/collects/typed-scheme/env/tvar-env.rkt @@ -1,10 +1,13 @@ #lang racket/base +;; this implements the Delta environment from the TOPLAS paper +;; (as well as every other paper on System F) + ;; 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? -(require "type-env-structs.rkt") +(require racket/require "type-env-structs.rkt" (path-up "rep/type-rep.rkt")) (provide (all-defined-out)) ;; the initial type variable environment - empty @@ -12,4 +15,10 @@ (define initial-tvar-env (make-empty-env #hasheq())) ;; a parameter for the current type variables -(define current-tvars (make-parameter initial-tvar-env)) \ No newline at end of file +(define current-tvars (make-parameter initial-tvar-env)) + +;; takes a list of vars +(define-syntax-rule (extend-tvars vars . body) + (parameterize ([current-tvars (extend-env vars (map make-F vars) (current-tvars))]) . body)) + +(define (bound-tvar? v) (lookup (current-tvars) v (lambda (_) #f))) \ No newline at end of file diff --git a/collects/typed-scheme/infer/infer-unit.rkt b/collects/typed-scheme/infer/infer-unit.rkt index cf7bfe66..92c35874 100644 --- a/collects/typed-scheme/infer/infer-unit.rkt +++ b/collects/typed-scheme/infer/infer-unit.rkt @@ -6,10 +6,9 @@ "utils/utils.rkt" "utils/tc-utils.rkt" "rep/free-variance.rkt" "rep/type-rep.rkt" "rep/filter-rep.rkt" "rep/rep-utils.rkt" "types/convenience.rkt" "types/union.rkt" "types/subtype.rkt" "types/remove-intersect.rkt" "types/resolve.rkt" - "env/type-name-env.rkt") + "env/type-name-env.rkt" "env/index-env.rkt" "env/tvar-env.rkt") make-env) - (except-in (path-up "types/utils.rkt") Dotted) - (only-in (path-up "env/type-env-structs.rkt" "env/tvar-env.rkt") lookup current-tvars) + (path-up "types/utils.rkt") "constraint-structs.rkt" "signatures.rkt" scheme/match @@ -272,14 +271,14 @@ [((F: (? (lambda (e) (memq e X)) v)) S) (when (match S [(F: v*) - (just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))] + (and (bound-index? v*) (not (bound-tvar? v*)))] [_ #f]) (fail! S T)) (singleton (Un) v (var-demote S V))] [(S (F: (? (lambda (e) (memq e X)) v))) (when (match S [(F: v*) - (just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))] + (and (bound-index? v*) (not (bound-tvar? v*)))] [_ #f]) (fail! S T)) (singleton (var-promote S V) v Univ)] diff --git a/collects/typed-scheme/private/parse-type.rkt b/collects/typed-scheme/private/parse-type.rkt index 6e2c4f3e..ee9cd9dd 100644 --- a/collects/typed-scheme/private/parse-type.rkt +++ b/collects/typed-scheme/private/parse-type.rkt @@ -6,7 +6,7 @@ (utils tc-utils stxclass-util) syntax/stx (prefix-in c: scheme/contract) syntax/parse - (env type-env-structs tvar-env type-name-env type-alias-env lexical-env) + (env type-env-structs tvar-env type-name-env type-alias-env lexical-env index-env) scheme/match unstable/debug (for-template scheme/base "colon.ss") ;; needed at this phase for tests @@ -69,17 +69,15 @@ (syntax-parse stx #:literals (t:All) [((~and kw t:All) (vars:id ... v:id dd:ddd) . t) (let* ([vars (map syntax-e (syntax->list #'(vars ...)))] - [tvars (map make-F vars)] - [v (syntax-e #'v)] - [tv (make-Dotted (make-F v))]) + [v (syntax-e #'v)]) (add-type-name-reference #'kw) - (parameterize ([current-tvars (extend-env (cons v vars) (cons tv tvars) (current-tvars))]) - (make-PolyDots (append vars (list v)) (parse-all-body #'t))))] + (extend-indexes v + (extend-tvars vars + (make-PolyDots (append vars (list v)) (parse-all-body #'t)))))] [((~and kw t:All) (vars:id ...) . t) - (let* ([vars (map syntax-e (syntax->list #'(vars ...)))] - [tvars (map make-F vars)]) + (let* ([vars (map syntax-e (syntax->list #'(vars ...)))]) (add-type-name-reference #'kw) - (parameterize ([current-tvars (extend-env vars tvars (current-tvars))]) + (extend-tvars vars (make-Poly vars (parse-all-body #'t))))] [(t:All (_:id ...) _ _ _ ...) (tc-error "All: too many forms in body of All type")] [(t:All . rest) (tc-error "All: bad syntax")])) @@ -179,10 +177,7 @@ (let* ([var (syntax-e #'x)] [tvar (make-F var)]) (add-type-name-reference #'kw) - (parameterize ([current-tvars (extend-env - (list var) - (list tvar) - (current-tvars))]) + (extend-tvars (list var) (let ([t (parse-type #'t)]) (if (memq var (fv t)) (make-Mu var t) @@ -223,41 +218,27 @@ #:kws (attribute kws.Keyword))))] [(dom:expr ... rest:expr :ddd/bound (~and kw t:->) rng) (add-type-name-reference #'kw) - (let ([var (lookup (current-tvars) (syntax-e #'bound) (lambda (_) #f))]) - (if (not (Dotted? var)) - (tc-error/stx #'bound - "Used a type variable (~a) not bound with ... as a bound on a ..." - (syntax-e #'bound)) - (make-Function - (list - (make-arr-dots (map parse-type (syntax->list #'(dom ...))) - (parse-values-type #'rng) - (parameterize - ([current-tvars - (extend-env - (list (syntax-e #'bound)) - (list (make-DottedBoth (make-F (syntax-e #'bound)))) - (current-tvars))]) - (parse-type #'rest)) - (syntax-e #'bound))))))] + (let* ([bnd (syntax-e #'bound)]) + (unless (bound-index? bnd) + (tc-error/stx #'bound + "Used a type variable (~a) not bound with ... as a bound on a ..." + bnd)) + (make-Function + (list + (make-arr-dots (map parse-type (syntax->list #'(dom ...))) + (parse-values-type #'rng) + (extend-tvars (list bnd) + (parse-type #'rest)) + bnd))))] [(dom:expr ... rest:expr _:ddd (~and kw t:->) rng) (add-type-name-reference #'kw) - (let ([bounds (env-keys+vals (env-filter (compose Dotted? cdr) (current-tvars)))]) - (when (null? bounds) - (tc-error/stx stx "No type variable bound with ... in scope for ... type")) - (unless (null? (cdr bounds)) - (tc-error/stx stx "Cannot infer bound for ... type")) - (match-let ([(cons var (struct Dotted (t))) (car bounds)]) - (make-Function - (list - (make-arr-dots (map parse-type (syntax->list #'(dom ...))) - (parse-values-type #'rng) - (parameterize ([current-tvars - (extend-env (list var) - (list (make-DottedBoth t)) - (current-tvars))]) - (parse-type #'rest)) - var)))))] + (let ([var (infer-index stx)]) + (make-Function + (list + (make-arr-dots (map parse-type (syntax->list #'(dom ...))) + (parse-values-type #'rng) + (extend-tvars (list var) (parse-type #'rest)) + var))))] #| ;; has to be below the previous one [(dom:expr ... (~and kw t:->) rng) (add-type-name-reference #'kw) @@ -275,14 +256,13 @@ [id:identifier (cond ;; if it's a type variable, we just produce the corresponding reference (which is in the HT) - [(lookup (current-tvars) (syntax-e #'id) (lambda (_) #f)) - => - (lambda (e) (cond [(DottedBoth? e) (Dotted-t e)] - [(Dotted? e) - (tc-error - "Type variable ~a must be used with ..." - (syntax-e #'id))] - [else e]))] + [(bound-tvar? (syntax-e #'id)) + (make-F (syntax-e #'id))] + ;; if it was in current-indexes, produce a better error msg + [(bound-index? (syntax-e #'id)) + (tc-error + "Type variable ~a must be used with ..." + (syntax-e #'id))] ;; if it's a type alias, we expand it (the expanded type is stored in the HT) [(lookup-type-alias #'id parse-type (lambda () #f)) => @@ -354,31 +334,24 @@ (syntax-parse stx #:literals (t:List) [((~and kw t:List) tys ... dty :ddd/bound) (add-type-name-reference #'kw) - (let ([var (lookup (current-tvars) (syntax-e #'bound) (lambda (_) #f))]) - (if (not (Dotted? var)) - (tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." (syntax-e #'bound)) - (-Tuple* (map parse-type (syntax->list #'(tys ...))) - (make-ListDots - (parameterize ([current-tvars (extend-env (list (syntax-e #'bound)) - (list (make-DottedBoth (make-F (syntax-e #'bound)))) - (current-tvars))]) - (parse-type #'dty)) - (syntax-e #'bound)))))] + (let ([var (syntax-e #'bound)]) + (unless (bound-index? var) + (if (bound-tvar? var) + (tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." var) + (tc-error/stx #'bound "Type variable ~a is unbound" var))) + (-Tuple* (map parse-type (syntax->list #'(tys ...))) + (make-ListDots + (extend-tvars (list var) + (parse-type #'dty)) + var)))] [((~and kw t:List) tys ... dty _:ddd) (add-type-name-reference #'kw) - (let ([bounds (env-keys+vals (env-filter (compose Dotted? cdr) (current-tvars)))]) - (when (null? bounds) - (tc-error/stx stx "No type variable bound with ... in scope for ... type")) - (unless (null? (cdr bounds)) - (tc-error/stx stx "Cannot infer bound for ... type")) - (match-let ([(cons var (struct Dotted (t))) (car bounds)]) - (-Tuple* (map parse-type (syntax->list #'(tys ...))) + (let ([var (infer-index stx)]) + (-Tuple* (map parse-type (syntax->list #'(tys ...))) (make-ListDots - (parameterize ([current-tvars (extend-env (list var) - (list (make-DottedBoth t)) - (current-tvars))]) + (extend-tvars (list var) (parse-type #'dty)) - var))))] + var)))] [((~and kw t:List) tys ...) (add-type-name-reference #'kw) (-Tuple (map parse-type (syntax->list #'(tys ...))))]))) @@ -388,29 +361,22 @@ (syntax-parse stx #:literals (values t:All) [((~and kw values) tys ... dty :ddd/bound) (add-type-name-reference #'kw) - (let ([var (lookup (current-tvars) (syntax-e #'bound) (lambda (_) #f))]) - (if (not (Dotted? var)) - (tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." (syntax-e #'bound)) - (make-ValuesDots (map parse-type (syntax->list #'(tys ...))) - (parameterize ([current-tvars (extend-env (list (syntax-e #'bound)) - (list (make-DottedBoth (make-F (syntax-e #'bound)))) - (current-tvars))]) - (parse-type #'dty)) - (syntax-e #'bound))))] + (let ([var (syntax-e #'bound)]) + (unless (bound-index? var) + (if (bound-tvar? var) + (tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." var) + (tc-error/stx #'bound "Type variable ~a is unbound" var))) + (make-ValuesDots (map parse-type (syntax->list #'(tys ...))) + (extend-tvars (list var) + (parse-type #'dty)) + var))] [((~and kw values) tys ... dty _:ddd) (add-type-name-reference #'kw) - (let ([bounds (env-keys+vals (env-filter (compose Dotted? cdr) (current-tvars)))]) - (when (null? bounds) - (tc-error/stx stx "No type variable bound with ... in scope for ... type")) - (unless (null? (cdr bounds)) - (tc-error/stx stx "Cannot infer bound for ... type")) - (match-let ([(cons var (struct Dotted (t))) (car bounds)]) - (make-ValuesDots (map parse-type (syntax->list #'(tys ...))) - (parameterize ([current-tvars (extend-env (list var) - (list (make-DottedBoth t)) - (current-tvars))]) + (let ([var (infer-index stx)]) + (make-ValuesDots (map parse-type (syntax->list #'(tys ...))) + (extend-tvars (list var) (parse-type #'dty)) - var)))] + var))] [((~and kw values) tys ...) (add-type-name-reference #'kw) (-values (map parse-type (syntax->list #'(tys ...))))] diff --git a/collects/typed-scheme/private/with-types.rkt b/collects/typed-scheme/private/with-types.rkt index e5cd04f6..601bdb38 100644 --- a/collects/typed-scheme/private/with-types.rkt +++ b/collects/typed-scheme/private/with-types.rkt @@ -71,8 +71,6 @@ [infer-param infer] ;; do we report multiple errors [delay-errors? #t] - ;; this parameter is for parsing types - [current-tvars initial-tvar-env] ;; this parameter is just for printing types ;; this is a parameter to avoid dependency issues [current-type-names diff --git a/collects/typed-scheme/tc-setup.rkt b/collects/typed-scheme/tc-setup.rkt index 26c67c12..66d1ea32 100644 --- a/collects/typed-scheme/tc-setup.rkt +++ b/collects/typed-scheme/tc-setup.rkt @@ -36,8 +36,6 @@ [infer-param infer] ;; do we report multiple errors [delay-errors? #t] - ;; this parameter is for parsing types - [current-tvars initial-tvar-env] ;; this parameter is just for printing types ;; this is a parameter to avoid dependency issues [current-type-names diff --git a/collects/typed-scheme/typecheck/tc-app.rkt b/collects/typed-scheme/typecheck/tc-app.rkt index b26f8e5e..84f6004b 100644 --- a/collects/typed-scheme/typecheck/tc-app.rkt +++ b/collects/typed-scheme/typecheck/tc-app.rkt @@ -16,7 +16,7 @@ (types utils abbrev union subtype resolve convenience type-table) (utils tc-utils) (only-in srfi/1 alist-delete) - (except-in (env type-env-structs tvar-env) extend) + (except-in (env type-env-structs tvar-env index-env) extend) (rep type-rep filter-rep object-rep) (r:infer infer) '#%paramz @@ -410,11 +410,10 @@ (not (eq? tail-bound (cdr (car drests*)))) (= (length (car doms*)) (length arg-tys)) - (parameterize ([current-tvars (extend-env (list tail-bound (cdr (car drests*))) - (list (make-DottedBoth (make-F tail-bound)) - (make-DottedBoth (make-F (cdr (car drests*))))) - (current-tvars))]) - (infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*))))) + (extend-tvars (list tail-bound (cdr (car drests*))) + (extend-indexes (cdr (car drests*)) + ;; don't need to add tail-bound - it must already be an index + (infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*)))))) => (lambda (substitution) (define drest-bound (cdr (car drests*))) (do-ret (substitute-dotted (cadr (assq drest-bound substitution)) @@ -636,9 +635,8 @@ (match (single-value #'arg) ;; if the argument is a ListDots [(tc-result1: (ListDots: t bound)) - (match (parameterize ([current-tvars (extend-env (list bound) - (list (make-DottedBoth (make-F bound))) - (current-tvars))]) + + (match (extend-tvars (list bound) ;; just check that the function applies successfully to the element type (tc/funapp #'f #'(arg) (tc-expr #'f) (list (ret t)) expected)) [(tc-result1: t) (ret (make-ListDots t bound))] diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.rkt b/collects/typed-scheme/typecheck/tc-expr-unit.rkt index 65ba6a06..84c4d0d0 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.rkt +++ b/collects/typed-scheme/typecheck/tc-expr-unit.rkt @@ -10,8 +10,7 @@ (rep type-rep) (only-in (infer infer) restrict) (except-in (utils tc-utils stxclass-util)) - (env lexical-env) - (only-in (env type-env-structs tvar-env) lookup current-tvars extend-env) + (env lexical-env type-env-structs tvar-env index-env) racket/private/class-internal unstable/debug (except-in syntax/parse id) (only-in srfi/1 split-at)) @@ -118,15 +117,11 @@ (let-values ([(all-but-last last-stx) (split-last (syntax->list inst))]) (match (syntax-e last-stx) [(cons last-ty-stx (? identifier? last-id-stx)) - (unless (Dotted? (lookup (current-tvars) (syntax-e last-id-stx) (lambda _ #f))) + (unless (bound-index? (syntax-e last-id-stx)) (tc-error/stx last-id-stx "~a is not a type variable bound with ..." (syntax-e last-id-stx))) (if (= (length all-but-last) (sub1 (PolyDots-n ty))) (let* ([last-id (syntax-e last-id-stx)] - [last-ty - (parameterize ([current-tvars (extend-env (list last-id) - (list (make-DottedBoth (make-F last-id))) - (current-tvars))]) - (parse-type last-ty-stx))]) + [last-ty (extend-tvars (list last-id) (parse-type last-ty-stx))]) (instantiate-poly-dotted ty (map parse-type all-but-last) last-ty last-id)) (tc-error/expr #:return (Un) "Wrong number of fixed type arguments to polymorphic type ~a:~nexpected: ~a~ngot: ~a" ty (sub1 (PolyDots-n ty)) (length all-but-last)))] diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.rkt b/collects/typed-scheme/typecheck/tc-lambda-unit.rkt index 056689e8..66494e60 100644 --- a/collects/typed-scheme/typecheck/tc-lambda-unit.rkt +++ b/collects/typed-scheme/typecheck/tc-lambda-unit.rkt @@ -13,7 +13,7 @@ [make-arr* make-arr]) (private type-annotation) (types abbrev utils) - (env type-env-structs lexical-env tvar-env) + (env type-env-structs lexical-env tvar-env index-env) (utils tc-utils) unstable/debug scheme/match) @@ -138,14 +138,11 @@ [(dotted? #'rest) => (lambda (bound) - (unless (Dotted? (lookup (current-tvars) bound - (lambda _ (tc-error/stx #'rest - "Bound on ... type (~a) was not in scope" bound)))) - (tc-error "Bound on ... type (~a) is not an appropriate type variable" bound)) - (let ([rest-type (parameterize ([current-tvars - (extend-env (list bound) - (list (make-DottedBoth (make-F bound))) - (current-tvars))]) + (unless (bound-index? bound) + (if (bound-tvar? bound) + (tc-error "Bound on ... type (~a) is not an appropriate type variable" bound) + (tc-error/stx #'rest "Bound on ... type (~a) was not in scope" bound))) + (let ([rest-type (extend-tvars (list bound) (get-type #'rest #:default Univ))]) (with-lexical-env/extend (cons #'rest arg-list) @@ -252,9 +249,7 @@ "Expected a polymorphic function without ..., but given function had ...")) (or (and p (map syntax-e (syntax->list p))) ns))] - [literal-tvars tvars] - [new-tvars (map make-F literal-tvars)] - [ty (parameterize ([current-tvars (extend-env literal-tvars new-tvars (current-tvars))]) + [ty (extend-tvars tvars (maybe-loop form formals bodies (ret expected*)))]) ;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty) t)] @@ -268,31 +263,23 @@ (values var dvar)] [_ (tc-error "Expected a polymorphic function with ..., but given function had no ...")]) (values ns dvar)))]) - (let* ([literal-tvars tvars] - [new-tvars (map make-F literal-tvars)] - [ty (parameterize ([current-tvars (extend-env (cons dotted literal-tvars) - (cons (make-Dotted (make-F dotted)) - new-tvars) - (current-tvars))]) - (maybe-loop form formals bodies (ret expected*)))]) - t))] + ;; check the body for side effect + (extend-indexes dotted + (extend-tvars tvars + (maybe-loop form formals bodies (ret expected*)))) + t)] [#f (match (map syntax-e (syntax->list (syntax-property form 'typechecker:plambda))) [(list tvars ... dotted-var '...) - (let* ([literal-tvars tvars] - [new-tvars (map make-F literal-tvars)] - [ty (parameterize ([current-tvars (extend-env (cons dotted-var literal-tvars) - (cons (make-Dotted (make-F dotted-var)) new-tvars) - (current-tvars))]) - (tc/mono-lambda/type formals bodies #f))]) - (make-PolyDots (append literal-tvars (list dotted-var)) ty))] + (let* ([ty (extend-indexes dotted-var + (extend-tvars tvars + (tc/mono-lambda/type formals bodies #f)))]) + (make-PolyDots (append tvars (list dotted-var)) ty))] [tvars - (let* ([literal-tvars tvars] - [new-tvars (map make-F literal-tvars)] - [ty (parameterize ([current-tvars (extend-env literal-tvars new-tvars (current-tvars))]) + (let* ([ty (extend-tvars tvars (tc/mono-lambda/type formals bodies #f))]) ;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty) - (make-Poly literal-tvars ty))])] + (make-Poly tvars ty))])] [(tc-result1: t) (unless (check-below (tc/plambda form formals bodies #f) t) (tc-error/expr #:return expected diff --git a/collects/typed-scheme/typecheck/tc-structs.rkt b/collects/typed-scheme/typecheck/tc-structs.rkt index a4945ca3..828f36ff 100644 --- a/collects/typed-scheme/typecheck/tc-structs.rkt +++ b/collects/typed-scheme/typecheck/tc-structs.rkt @@ -181,10 +181,10 @@ ;; parse the types (define types ;; add the type parameters of this structure to the tvar env - (parameterize ([current-tvars (extend-env tvars new-tvars (current-tvars))] - [current-poly-struct `#s(poly ,nm ,new-tvars)]) - ;; parse the field types - (map parse-type tys))) + (extend-tvars tvars + (parameterize ([current-poly-struct `#s(poly ,nm ,new-tvars)]) + ;; parse the field types + (map parse-type tys)))) ;; instantiate the parent if necessary, with new-tvars (define concrete-parent (if (Poly? parent) diff --git a/collects/typed-scheme/types/utils.rkt b/collects/typed-scheme/types/utils.rkt index f32aae39..024b7b66 100644 --- a/collects/typed-scheme/types/utils.rkt +++ b/collects/typed-scheme/types/utils.rkt @@ -5,6 +5,7 @@ (require (rep type-rep filter-rep object-rep rep-utils) (utils tc-utils) (only-in (rep free-variance) combine-frees) + (env index-env tvar-env) scheme/match scheme/list mzlib/trace @@ -25,9 +26,6 @@ effects-equal? tc-result-t unfold - (struct-out Dotted) - (struct-out DottedBoth) - just-Dotted? tc-error/expr lookup-fail lookup-type-fail @@ -48,7 +46,7 @@ (begin (when (and (pair? drest) (eq? name (cdr drest)) - (just-Dotted? name)) + (not (bound-tvar? name))) (int-err "substitute used on ... variable ~a in type ~a" name target)) (make-arr (map sb dom) (sb rng) @@ -57,12 +55,12 @@ (map sb kws)))] [#:ValuesDots types dty dbound (begin - (when (eq? name dbound) + (when (and (eq? name dbound) (not (bound-tvar? name))) (int-err "substitute used on ... variable ~a in type ~a" name target)) (make-ValuesDots (map sb types) (sb dty) dbound))] [#:ListDots dty dbound (begin - (when (eq? name dbound) + (when (and (eq? name dbound) (not (bound-tvar? name))) (int-err "substitute used on ... variable ~a in type ~a" name target)) (make-ListDots (sb dty) dbound))]) target)) @@ -299,14 +297,6 @@ ;; fv/list : Listof[Type] -> Listof[Name] (define (fv/list ts) (hash-map (combine-frees (map free-vars* ts)) (lambda (k v) k))) -;; t is (make-F v) -(define-struct Dotted (t)) -(define-struct (DottedBoth Dotted) ()) - -(define (just-Dotted? S) - (and (Dotted? S) - (not (DottedBoth? S)))) - (define (tc-error/expr msg #:return [return (make-Union null)] #:stx [stx (current-orig-stx)] . rest) (tc-error/delayed #:stx stx (apply format msg rest)) return)