diff --git a/typed-racket-lib/typed-racket/env/type-alias-helper.rkt b/typed-racket-lib/typed-racket/env/type-alias-helper.rkt index 2aa04ce8..6478bd88 100644 --- a/typed-racket-lib/typed-racket/env/type-alias-helper.rkt +++ b/typed-racket-lib/typed-racket/env/type-alias-helper.rkt @@ -111,15 +111,15 @@ ;; recursive type aliases should be initialized. (define-values (type-alias-dependency-map type-alias-class-map) (for/lists (_1 _2) - ([entry (in-list type-alias-map)]) - (match-define (cons name alias-info) entry) + ([(name alias-info) (in-assoc type-alias-map)]) (define links-box (box null)) (define class-box (box null)) - (define type - (parameterize ([current-type-alias-name name] - [current-referenced-aliases links-box] - [current-referenced-class-parents class-box]) - (parse-type (car alias-info)))) + ;; parse types for effect + (parameterize ([current-type-alias-name name] + [current-referenced-aliases links-box] + [current-referenced-class-parents class-box] + [check-type-invariants-while-parsing? #f]) + (parse-type (car alias-info))) (define pre-dependencies (remove-duplicates (unbox links-box) free-identifier=?)) (define (filter-by-type-alias-names names) diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt index fd403d10..160952dc 100644 --- a/typed-racket-lib/typed-racket/private/parse-type.rkt +++ b/typed-racket-lib/typed-racket/private/parse-type.rkt @@ -45,7 +45,8 @@ (provide star ddd/bound current-referenced-aliases current-referenced-class-parents - current-type-alias-name) + current-type-alias-name + check-type-invariants-while-parsing?) ;; current-term-names : Parameter<(Listof Id)> ;; names currently "bound" by a type we are parsing @@ -96,6 +97,14 @@ (parameterize ([current-arities (cons arity (current-arities))]) e ...)) + +;; code in type-alias-helper.rkt calls `parse-type` for effect to build up +;; info about how types depend on eachother -- during this parsing, we can't +;; check certain invariant successfully (i.e. when a user writes `(car p)` +;; `p` is <: (Pair Any Any), etc), so we use this flag to disable/enable +;; invariant checking while parsing +(define check-type-invariants-while-parsing? (make-parameter #t)) + (define-literal-syntax-class #:for-label car) (define-literal-syntax-class #:for-label cdr) (define-literal-syntax-class #:for-label vector-length) @@ -379,7 +388,8 @@ (pattern o:symbolic-object #:do [(define obj (attribute o.val)) (define obj-ty (lookup-obj-type/lexical obj))] - #:fail-unless (subtype obj-ty -Int) + #:fail-when (and (check-type-invariants-while-parsing?) + (not (subtype obj-ty -Int))) (format "terms in linear constraints must be integers, got ~a for ~a" obj-ty obj) #:attr val (attribute o.val))) @@ -398,7 +408,8 @@ (pattern (:*^ ~! n:exact-integer o:symbolic-object-w/o-lexp) #:do [(define obj (attribute o.val)) (define obj-ty (lookup-obj-type/lexical obj))] - #:fail-unless (subtype obj-ty -Int) + #:fail-when (and (check-type-invariants-while-parsing?) + (not (subtype obj-ty -Int))) (format "terms in linear constraints must be integers, got ~a for ~a" obj-ty obj) #:attr val (-lexp (list (syntax->datum #'n) (attribute o.val)))) @@ -424,21 +435,24 @@ (pattern (:car^ ~! o:symbolic-object-w/o-lexp) #:do [(define obj (attribute o.val)) (define obj-ty (lookup-obj-type/lexical obj))] - #:fail-unless (subtype obj-ty (-pair Univ Univ)) + #:fail-when (and (check-type-invariants-while-parsing?) + (not (subtype obj-ty (-pair Univ Univ)))) (format "car expects a pair, but got ~a for ~a" obj-ty obj) #:attr val (-car-of (attribute o.val))) (pattern (:cdr^ ~! o:symbolic-object-w/o-lexp) #:do [(define obj (attribute o.val)) (define obj-ty (lookup-obj-type/lexical obj))] - #:fail-unless (subtype obj-ty (-pair Univ Univ)) + #:fail-when (and (check-type-invariants-while-parsing?) + (not (subtype obj-ty (-pair Univ Univ)))) (format "cdr expects a pair, but got ~a for ~a" obj-ty obj) #:attr val (-cdr-of (attribute o.val))) (pattern (:vector-length^ ~! o:symbolic-object-w/o-lexp) #:do [(define obj (attribute o.val)) (define obj-ty (lookup-obj-type/lexical obj))] - #:fail-unless (subtype obj-ty -VectorTop) + #:fail-when (and (check-type-invariants-while-parsing?) + (not (subtype obj-ty -VectorTop))) (format "vector-length expects a vector, but got ~a for ~a" obj-ty obj) #:attr val (-vec-len-of (attribute o.val)))) @@ -461,7 +475,8 @@ (pattern (:*^ ~! coeff:exact-integer o:symbolic-object-w/o-lexp) #:do [(define obj (attribute o.val)) (define obj-ty (lookup-obj-type/lexical obj))] - #:fail-unless (subtype obj-ty -Int) + #:fail-when (and (check-type-invariants-while-parsing?) + (not (subtype obj-ty -Int))) (format "terms in linear expressions must be integers, got ~a for ~a" obj-ty obj) #:attr val (-lexp (list (syntax->datum #'coeff) (attribute o.val)))) @@ -470,7 +485,8 @@ (pattern o:symbolic-object-w/o-lexp #:do [(define obj (attribute o.val)) (define obj-ty (lookup-obj-type/lexical obj))] - #:fail-unless (subtype obj-ty -Int) + #:fail-when (and (check-type-invariants-while-parsing?) + (not (subtype obj-ty -Int))) (format "terms in linear expressions must be integers, got ~a for ~a" obj-ty obj) #:attr val (attribute o.val)) diff --git a/typed-racket-test/succeed/refinements-and-aliases.rkt b/typed-racket-test/succeed/refinements-and-aliases.rkt new file mode 100644 index 00000000..4aa3220d --- /dev/null +++ b/typed-racket-test/succeed/refinements-and-aliases.rkt @@ -0,0 +1,16 @@ +#lang typed/racket/base #:with-refinements + +(define-type Pear (Pair Integer Integer)) +(define-type SomeVectorsInAPair (Pair (Vectorof String) + (Vectorof String))) + +(define-type Pear1 + (Refine [p : Pear] (= (car p) 5))) + +(define-type Pear2 + (Refine [p : Pear] (= (cdr p) 5))) + +(define-type Vec + (Refine [p : SomeVectorsInAPair] + (= (vector-length (car p)) + (vector-length (cdr p))))) \ No newline at end of file