From 46365587b236cf1fe0423c2b17161ef64608fca3 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Tue, 12 Jan 2010 20:36:30 +0000 Subject: [PATCH] Reject some cases of nested types. svn: r17619 original commit: 91629fd31ace6700a6864c0db826c89e2987c1a2 --- collects/typed-scheme/private/parse-type.ss | 9 ++++++-- collects/typed-scheme/typecheck/tc-structs.ss | 3 ++- collects/typed-scheme/types/resolve.ss | 23 ++++++++++++++----- collects/typed-scheme/types/subtype.ss | 4 ++-- collects/typed-scheme/types/utils.ss | 7 +++++- 5 files changed, 34 insertions(+), 12 deletions(-) diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss index 390b07e0..c85c5bb2 100644 --- a/collects/typed-scheme/private/parse-type.ss +++ b/collects/typed-scheme/private/parse-type.ss @@ -12,13 +12,14 @@ (for-template scheme/base "base-types-extra.ss" "colon.ss") (for-template (prefix-in t: "base-types-extra.ss"))) +(define-struct poly (name vars) #:prefab) + (p/c [parse-type (syntax? . c:-> . Type/c)] [parse-type/id (syntax? c:any/c . c:-> . Type/c)] [parse-tc-results (syntax? . c:-> . tc-results?)] [parse-tc-results/id (syntax? c:any/c . c:-> . tc-results?)]) (provide star ddd/bound) - (define enable-mu-parsing (make-parameter #t)) (define ((parse/id p) loc datum) @@ -280,7 +281,11 @@ ([rator (parse-type #'id)] [args (map parse-type (syntax->list #'(arg args ...)))]) (match rator - [(Name: _) + [(Name: n) + (when (and (current-poly-struct) + (free-identifier=? n (poly-name (current-poly-struct))) + (not (andmap type-equal? args (poly-vars (current-poly-struct))))) + (tc-error "Structure type constructor ~a applied to non-regular arguments ~a" rator args)) (make-App rator args stx)] [(Poly: ns _) (unless (= (length args) (length ns)) diff --git a/collects/typed-scheme/typecheck/tc-structs.ss b/collects/typed-scheme/typecheck/tc-structs.ss index 5f313573..99fd72e6 100644 --- a/collects/typed-scheme/typecheck/tc-structs.ss +++ b/collects/typed-scheme/typecheck/tc-structs.ss @@ -159,7 +159,8 @@ ;; 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))]) + (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))) ;; instantiate the parent if necessary, with new-tvars diff --git a/collects/typed-scheme/types/resolve.ss b/collects/typed-scheme/types/resolve.ss index a558255b..d2baa705 100644 --- a/collects/typed-scheme/types/resolve.ss +++ b/collects/typed-scheme/types/resolve.ss @@ -6,28 +6,38 @@ (utils tc-utils) (types utils) scheme/match - scheme/contract - mzlib/trace) + scheme/contract) (provide resolve-name resolve-app needs-resolving? resolve) (p/c [resolve-once (Type/c . -> . (or/c Type/c #f))]) +(define-struct poly (name vars) #:prefab) + (define (resolve-name t) (match t [(Name: n) (let ([t (lookup-type-name n)]) (if (Type? t) t #f))] [_ (int-err "resolve-name: not a name ~a" t)])) +(define already-resolving? (make-parameter #f)) + (define (resolve-app rator rands stx) - (parameterize ([current-orig-stx stx]) + (parameterize ([current-orig-stx stx] + + [already-resolving? #t]) (match rator [(Poly-unsafe: n _) (unless (= n (length rands)) (tc-error "wrong number of arguments to polymorphic type: expected ~a and got ~a" n (length rands))) (instantiate-poly rator rands)] - [(Name: _) (let ([r (resolve-name rator)]) - (and r (resolve-app r rands stx)))] + [(Name: n) + (when (and (current-poly-struct) + (free-identifier=? n (poly-name (current-poly-struct))) + (not (andmap type-equal? rands (poly-vars (current-poly-struct))))) + (tc-error "Structure type constructor ~a applied to non-regular arguments ~a" rator rands)) + (let ([r (resolve-name rator)]) + (and r (resolve-app r rands stx)))] [(Mu: _ _) (resolve-app (unfold rator) rands)] [(App: r r* s) (resolve-app (resolve-app r r* s) rands)] [_ (tc-error "cannot apply a non-polymorphic type: ~a" rator)]))) @@ -38,7 +48,8 @@ (define (resolve-once t) (match t [(Mu: _ _) (unfold t)] - [(App: r r* s) (resolve-app r r* s)] + [(App: r r* s) + (resolve-app r r* s)] [(Name: _) (resolve-name t)])) (define (resolve t) diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss index 3f6e8303..9c53bcb1 100644 --- a/collects/typed-scheme/types/subtype.ss +++ b/collects/typed-scheme/types/subtype.ss @@ -5,7 +5,7 @@ (types utils comparison resolve abbrev) (env type-name-env) (only-in (infer infer-dummy) unify) - scheme/match unstable/match + scheme/match unstable/match unstable/debug mzlib/trace (rename-in scheme/contract [-> c->] [->* c->*]) @@ -308,7 +308,7 @@ (subtypes* A0 (cons proc flds) (cons proc* flds*))] ;; subtyping on structs follows the declared hierarchy [((Struct: nm (? Type? parent) flds proc _ _ _) other) - ;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other) + ;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other) (subtype* A0 parent other)] ;; Promises are covariant [((Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)] diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss index affbc234..75454175 100644 --- a/collects/typed-scheme/types/utils.ss +++ b/collects/typed-scheme/types/utils.ss @@ -31,7 +31,8 @@ tc-error/expr lookup-fail lookup-type-fail - combine-results) + combine-results + current-poly-struct) ;; substitute : Type Name Type -> Type @@ -305,3 +306,7 @@ (define (lookup-type-fail i) (tc-error/expr "~a is not bound as a type" (syntax-e i))) + +;; a parameter for the current polymorphic structure being defined +;; to allow us to prevent non-regular datatypes +(define current-poly-struct (make-parameter #f)) \ No newline at end of file