Fix typechecking of polymorphic structs with parent types.

Closes PR12998.

original commit: e9f209977b5d437589265ca5e9e69c74d45b9d47
This commit is contained in:
Eric Dobson 2012-08-12 14:36:27 -07:00 committed by Sam Tobin-Hochstadt
parent 467c46360c
commit cfe59c4980
9 changed files with 86 additions and 13 deletions

View File

@ -0,0 +1,8 @@
#lang typed/racket
(define-struct: (A) Box ([value : A]) #:transparent)
(define-struct: (A) (Child-Box Box) () #:transparent)
(ann (Box-value (Child-Box 'sym)) Nothing)

View File

@ -0,0 +1,7 @@
#;
("Could not instantiate parent struct type")
#lang typed/racket
(define-struct: (A) Box ([value : A]) #:transparent)
(define-struct: (Child-Box Box) () #:transparent)

View File

@ -0,0 +1,9 @@
#;
("Could not instantiate parent struct type")
#lang typed/racket
(define-struct: (A B) Box ([value : A]
[other : B]) #:transparent)
(define-struct: (C) (Child-Box Box) () #:transparent)

View File

@ -0,0 +1,30 @@
#lang typed/racket
(define-struct: (A) Box ([value : A]) #:transparent)
(define-struct: (A B) (Child-Box Box) ([other-value : B]) #:transparent)
(: v1 Symbol)
(define v1 (Box-value (Child-Box 'sym "str")))
(: v2 String)
(define v2 (Child-Box-other-value (Child-Box 'sym "str")))
(struct: (A) Box2 ([proc : (-> A)]))
(struct: (A) Strict-Box2 Box2 ())
(struct: (A) Mutable-Box2 Strict-Box2 ([value : (Vector A)]))
(: box-mutable2 (All (A) ((Box2 A) -> (Mutable-Box2 A))))
(define (box-mutable2 b)
(define v ((Box2-proc b)))
(define vs (vector v))
(Mutable-Box2 (λ () (vector-ref vs 0)) vs))
(: box-strict2 (All (A) ((Box2 A) -> (Box2 A))))
(define (box-strict2 b)
(cond
[(Strict-Box2? b) b]
[else (box-mutable2 b)]))
(box-mutable2 (Box2 (λ () 0)))
(box-strict2 (box-mutable2 (Box2 (λ () 0))))
(ann (ann (box-mutable2 (Box2 (λ () 0))) (Mutable-Box2 Integer)) (Box2 Number))

View File

@ -10,11 +10,11 @@
(env type-name-env index-env tvar-env))
make-env -> ->* one-of/c)
"constraint-structs.rkt"
"signatures.rkt"
"signatures.rkt"
racket/match
mzlib/etc
racket/contract
unstable/sequence unstable/list unstable/hash
unstable/sequence unstable/list unstable/hash
racket/list)
(import dmap^ constraints^ promote-demote^)
@ -31,7 +31,7 @@
(listof (cons/c exact-nonnegative-integer? exact-nonnegative-integer?)))
(cons (seen-before s t) A))
(define/cond-contract (seen? s t)
(Type? Type? . -> . boolean?)
(Type? Type? . -> . any/c)
(member (seen-before s t) (current-seen)))
@ -421,9 +421,9 @@
(for/list ([e es])
(with-handlers ([exn:infer? (λ _ #f)]) (cg S e)))))]
;; two structs with the same name and parent
;; two structs with the same name
;; just check pairwise on the fields
[((Struct: nm p flds proc _ _ _ _) (Struct: nm* p flds* proc* _ _ _ _)) (=> nevermind)
[((Struct: nm _ flds proc _ _ _ _) (Struct: nm* _ flds* proc* _ _ _ _)) (=> nevermind)
(unless (free-identifier=? nm nm*) (nevermind))
(let ([proc-c
(cond [(and proc proc*)
@ -517,6 +517,12 @@
(let ((T* (resolve-once T)))
(if T* (cg S T*) (fail! S T)))]
;; If the struct names don't match, try the parent of S
;; Needs to be done after App and Mu in case T is actually the current struct
;; but not currently visible
[((Struct: nm (? Type? parent) _ _ _ _ _ _) other)
(cg parent other)]
;; vectors are invariant - generate constraints *both* ways
[((Vector: e) (Vector: e*))
(cset-meet (cg e e*) (cg e* e))]

View File

@ -246,7 +246,10 @@ types. In most cases, use of @racket[:] is preferred to use of @racket[define:]
When @racket[parent] is present, the
structure is a substructure of @racket[parent]. When
@racket[maybe-type-vars] is present, the structure is polymorphic in the type
variables @racket[v].
variables @racket[v]. If @racket[parent] is also a polymorphic struct, then
there must be at least as many type variables as in the parent type, and the
parent type is instantiated with a prefix of the type variables matching the
amount it needs.
Options provided have the same meaning as for the @racket[struct] form.}

View File

@ -39,7 +39,7 @@
(syntax-parse expr
[((~literal quote) i:number)
(let ((type (tc-literal #'i)))
(add-typeof-expr expr type)
(add-typeof-expr expr (ret type))
(values type (syntax-e #'i)))]
[_
(match (tc-expr expr)

View File

@ -11,6 +11,7 @@
syntax/struct
racket/function
racket/match
racket/list
(only-in racket/contract
listof any/c or/c
[->* c->*]
@ -228,14 +229,18 @@
;; instantiate the parent if necessary, with new-tvars
(define concrete-parent
(if (Poly? parent)
(instantiate-poly parent new-tvars)
(if (> (Poly-n parent) (length new-tvars))
(tc-error "Could not instantiate parent struct type. Required ~a type variables, recieved ~a."
(Poly-n parent)
(length new-tvars))
(instantiate-poly parent (take new-tvars (Poly-n parent))))
parent))
;; get the fields of the parent, if it exists
(define parent-field-types (get-parent-flds concrete-parent))
;; create the actual structure type, and the types of the fields
;; that the outside world will see
;; then register them
(mk/register-sty nm flds parent-name parent-field-types types
(mk/register-sty nm flds concrete-parent parent-field-types types
#:maker maker
#:mutable mutable
#:struct-info (syntax-property nm/par 'struct-info)
@ -268,6 +273,11 @@
(if proc-ty
(parse-type proc-ty)
#f))
(when (Poly? parent)
(tc-error "Could not instantiate parent struct type. Required ~a type variables, recieved none."
(Poly-n parent)))
;; create the actual structure type, and the types of the fields
;; that the outside world will see
(mk/register-sty nm flds parent-name (get-parent-flds parent) types
@ -276,7 +286,7 @@
#:maker maker
#:predicate pred
#:struct-info (syntax-property nm/par 'struct-info)
#:constructor-return (and cret (parse-type cret))
#:constructor-return (and cret (parse-type cret))
#:mutable mutable
#:type-only type-only))

View File

@ -45,7 +45,7 @@
;; is s a subtype of t?
;; type type -> boolean
(define/cond-contract (subtype s t)
(c-> Type/c Type/c boolean?)
(c:-> (c:or/c Type/c Values?) (c:or/c Type/c Values?) boolean?)
(define k (cons (Type-seq s) (Type-seq t)))
(define lookup? (hash-ref subtype-cache k 'no))
(if (eq? 'no lookup?)
@ -432,7 +432,7 @@
[((MPair: _ _) (MPairTop:)) A0]
[((Hashtable: _ _) (HashtableTop:)) A0]
;; subtyping on structs follows the declared hierarchy
[((Struct: nm (? Type? parent) flds proc _ _ _ _) other)
[((Struct: nm (? Type? parent) _ _ _ _ _ _) other)
;(dprintf "subtype - hierarchy : ~a ~a ~a\n" nm parent other)
(subtype* A0 parent other)]
;; subtyping on values is pointwise
@ -464,7 +464,7 @@
(provide/cond-contract
[subtype (c-> Type/c Type/c boolean?)])
[subtype (c:-> (c:or/c Type/c Values?) (c:or/c Type/c Values?) boolean?)])
(provide
type-compare? subtypes/varargs subtypes)