diff --git a/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/guide/more.scrbl b/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/guide/more.scrbl index f5cb6258..b8f0fee2 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/guide/more.scrbl +++ b/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/guide/more.scrbl @@ -207,6 +207,7 @@ Any type can be given a name with @racket[define-type]. @racketblock[(define-type NN (-> Number Number))] Anywhere the name @racket[NN] is used, it is expanded to -@racket[(-> Number Number)]. Type names may not be recursive. +@racket[(-> Number Number)]. Type names may be recursive +or even mutually recursive. @(close-eval the-eval) diff --git a/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl b/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl index e201b369..6ac58ca6 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl +++ b/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl @@ -408,15 +408,34 @@ corresponding to @|define-struct-id| from @racketmodname[racket/base].} The first form defines @racket[name] as type, with the same meaning as @racket[t]. The second form is equivalent to @racket[(define-type name (All (v ...) t))]. Type names may -refer to other types defined in the same module, but -cycles among them are prohibited. +refer to other types defined in the same or enclosing scopes. @ex[(define-type IntStr (U Integer String)) (define-type (ListofPairs A) (Listof (Pair A A)))] If @racket[#:omit-define-syntaxes] is specified, no definition of @racket[name] is created. In this case, some other definition of @racket[name] -is necessary.} +is necessary. + +If the body of the type definition refers to itself, then the +type definition is recursive. Recursion may also occur mutually, +if a type refers to a chain of other types that eventually refers +back to itself. + +@ex[(define-type BT (U Number (Pair BT BT))) + (let () + (define-type (Even A) (U Null (Pairof A (Odd A)))) + (define-type (Odd A) (Pairof A (Even A))) + (: even-lst (Even Integer)) + (define even-lst '(1 2)) + even-lst)] + +However, the recursive reference may not occur immediately inside +the type: + +@ex[(define-type Foo Foo) + (define-type Bar (U Bar False))] +} @section{Generating Predicates Automatically} diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-structs.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-structs.rkt index 58d6c856..d6bb8e1f 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-structs.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-structs.rkt @@ -35,10 +35,11 @@ ...) ...)])) -(define -Srcloc (make-Name #'srcloc)) -(define -Date (make-Name #'date)) -(define -Arity-At-Least (make-Name #'arity-at-least)) -(define -Exn (make-Name #'exn)) +(define -Srcloc (make-Name #'srcloc null #f #t)) +(define -Date (make-Name #'date null #f #t)) +(define -Arity-At-Least + (make-Name #'arity-at-least null #f #t)) +(define -Exn (make-Name #'exn null #f #t)) (define (initialize-structs) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt index e5e5cb1a..4dbb6661 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt @@ -504,22 +504,35 @@ This file defines two sorts of primitives. All of them are provided into any mod (syntax/loc stx ((plambda: (A ...) (bn ...) . body) e ...))])) +;; Syntax classes for `define-type-alias` +(begin-for-syntax + (define-syntax-class type-alias-rest + #:literals (All) + #:attributes (args) + (pattern (All (arg:id ...) rest) + #:with args #'(arg ...)) + (pattern type:expr #:with args #'#f))) + (define-syntax (define-type-alias stx) (syntax-parse stx - [(_ tname:id rest (~optional (~and omit #:omit-define-syntaxes) - #:defaults - ([omit #f]))) + [(_ tname:id rest:type-alias-rest + (~optional (~and omit #:omit-define-syntaxes) + #:defaults + ([omit #f]))) + (define/with-syntax stx-err-fun + #'(lambda (stx) + (raise-syntax-error + 'type-check + "type name used out of context" + stx + (and (stx-pair? stx) (stx-car stx))))) #`(begin #,(if (not (attribute omit)) - (ignore #'(define-syntax tname - (lambda (stx) - (raise-syntax-error - 'type-check - "type name used out of context" - stx - (and (stx-pair? stx) (stx-car stx)))))) + (ignore #'(define-syntax tname stx-err-fun)) #'(begin)) - #,(internal (syntax/loc stx (define-type-alias-internal tname rest))))] + #,(internal (syntax/loc stx + (define-type-alias-internal tname rest + rest.args))))] [(_ (tname:id args:id ...) rest) (syntax/loc stx (define-type-alias tname (All (args ...) rest)))])) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt index 2908c82f..5e4cacb0 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt @@ -78,7 +78,12 @@ `(->acc (list ,@(map sub dom)) ,(sub t) ,(sub pth))] [(Union: elems) (split-union elems)] [(Base: n cnt pred _) (int-err "Base type not in predefined-type-table" n)] - [(Name: stx) `(make-Name (quote-syntax ,stx))] + [(Name: stx deps args struct?) + `(make-Name (quote-syntax ,stx) + (list ,@(map (λ (x) `(quote-syntax ,x)) deps)) + ,(and args + `(list ,@(map (λ (x) `(quote-syntax ,x)) args))) + ,struct?)] [(fld: t acc mut) `(make-fld ,(sub t) (quote-syntax ,acc) ,mut)] [(Struct: name parent flds proc poly? pred-id) `(make-Struct (quote-syntax ,name) ,(sub parent) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/type-alias-helper.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/type-alias-helper.rkt new file mode 100644 index 00000000..7b0ecbfc --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/type-alias-helper.rkt @@ -0,0 +1,326 @@ +#lang racket/base + +;; This module provides helper functions for type aliases + +(require "../utils/utils.rkt" + (utils tc-utils) + (env type-alias-env type-name-env) + (rep type-rep) + (private parse-type) + (typecheck internal-forms) + (types resolve base-abbrev) + data/queue + racket/dict + racket/format + racket/list + racket/match + syntax/id-table + syntax/kerncase + (for-template + (typecheck internal-forms) + racket/base)) + +(provide find-strongly-connected-type-aliases + check-type-alias-contractive + get-type-alias-info + register-all-type-aliases + parse-type-alias) + +;; A Vertex is a +;; (vertex Identifier Boolean Option Option Listof) +;; +;; interp. a vertex in a graph, we only use this for Tarjan's algorithm +;; id - identifier (labels vertices) +;; stack? - whether this vertex is on the stack (for speed) +;; index - index tracked in Tarjan's algorithm +;; lowlink - see index +;; adjacent - list of adjacent vertices +(struct vertex (id [stack? #:mutable] [index #:mutable] + [lowlink #:mutable] adjacent) + #:transparent) + +;; Dict)> -> Listof> +;; Find strongly connected type aliases in order to +;; find mutually recursive aliases +;; +;; Returns the components in topologically sorted order +(define (find-strongly-connected-type-aliases dep-map) + (define vertex-map (make-free-id-table)) + (for ([(id adjacent) (in-dict dep-map)]) + (free-id-table-set! vertex-map id (vertex id #f #f #f adjacent))) + ;; Implements Tarjan's algorithm. See Wikipedia + ;; http://en.wikipedia.org/wiki/Tarjan's_strongly_connected_components_algorithm + (define (tarjan vertices) + (define (strongly-connected vtx) + (set-vertex-index! vtx index) + (set-vertex-lowlink! vtx index) + (set! index (add1 index)) + (enqueue-front! stack vtx) + (set-vertex-stack?! vtx #t) + (for ([successor-id (in-list (vertex-adjacent vtx))]) + (define successor (free-id-table-ref vertices successor-id)) + (cond [(not (vertex-index successor)) + (strongly-connected successor) + (set-vertex-lowlink! vtx + (min (vertex-lowlink vtx) + (vertex-lowlink successor)))] + [(vertex-stack? successor) + (set-vertex-lowlink! vtx + (min (vertex-lowlink vtx) + (vertex-index successor)))])) + ;; sets a result component if this was a root vertex + (when (= (vertex-lowlink vtx) (vertex-index vtx)) + (define new-scc + (for/list ([elem (in-queue stack)] + #:final (equal? vtx elem)) + (dequeue! stack) + (set-vertex-stack?! elem #f) + (vertex-id elem))) + (set! sccs (cons new-scc sccs)))) + + ;; the body + (define index 0) + (define stack (make-queue)) + (define sccs '()) + (for ([(id vtx) (in-dict vertices)] + #:unless (vertex-index vtx)) + (strongly-connected vtx)) + sccs) + (tarjan vertex-map)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Data definitions for aliases +;; +;; A TypeAliasInfo is a (list Syntax (Listof Identifier)) +;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; check-type-alias-contractive : Id Type -> Void +;; +;; This function checks if the given type alias is +;; "contractive" or "productive" +;; i.e., that you can unfold a good type like μx.int->x to +;; μx.int->int->int->...x but a type like +;; μx.x only unfolds to itself +;; +(define (check-type-alias-contractive id type) + (define/match (check type) + [((Union: elems)) (andmap check elems)] + [((Name: name-id _ _ _)) + (and (not (free-identifier=? name-id id)) + (check (resolve-once type)))] + [((App: rator rands stx)) + (and (check rator) (check rands))] + [((Mu: _ body)) (check body)] + [((Poly: names body)) (check body)] + [((PolyDots: names body)) (check body)] + [(_) #t]) + (unless (check type) + (tc-error/stx + id + "Recursive types are not allowed directly inside their definition"))) + +;; get-type-alias-info : Listof -> Listof Dict +;; +;; Given the syntaxes representing type alias definitions, return +;; the information needed to register them later +(define (get-type-alias-info type-aliases) + (for/lists (_1 _2) ([type-alias (in-list type-aliases)]) + (define-values (id type-stx args) (parse-type-alias type-alias)) + ;; Register type alias names with a dummy value so that it's in + ;; scope for the registration later. + ;; + ;; The `(make-Value (gensym))` expression is used to make sure + ;; that unions don't collapse the aliases too soon. + (register-resolved-type-alias id Err) + (register-type-name + id + (if args + (make-Poly (map syntax-e args) (make-Value (gensym))) + (make-Value (gensym)))) + (values id (list id type-stx args)))) + +;; register-all-type-aliases : Listof Dict -> Void +;; +;; Given parsed type aliases and a type alias map, do the work +;; of actually registering the type aliases. If struct names or +;; other definitions need to be registered, do that before calling +;; this function. +(define (register-all-type-aliases type-alias-names type-alias-map) + ;; Disable resolve caching for the extent of this setup. + ;; Makes sure Name types don't get cached too soon. + (parameterize ([current-cache-resolve? #f]) + ;; Find type alias dependencies + ;; The two maps defined here contains the dependency structure + ;; of type aliases in two senses: + ;; (1) other type aliases referenced in a type alias + ;; (2) other type aliases referenced by some class in a + ;; type alias in a #:implements clause + ;; + ;; The second is necessary in order to prevent recursive + ;; #:implements clauses and to determine the order in which + ;; recursive type aliases should be initialized. + (define-values (type-alias-dependency-map type-alias-class-map) + (for/lists (_1 _2) + ([(name alias-info) (in-dict 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)))) + (define pre-dependencies + (remove-duplicates (unbox links-box) free-identifier=?)) + (define (filter-by-type-alias-names names) + (for/list ([id (in-list names)] + #:when (memf (λ (id2) (free-identifier=? id id2)) + type-alias-names)) + id)) + (define alias-dependencies + (filter-by-type-alias-names pre-dependencies)) + (define class-dependencies + (filter-by-type-alias-names (unbox class-box))) + (values (cons name alias-dependencies) + (cons name class-dependencies)))) + + (define components + (find-strongly-connected-type-aliases type-alias-dependency-map)) + + (define class-components + (find-strongly-connected-type-aliases type-alias-class-map)) + + ;; helper function for defining singletons + (define (has-self-cycle? component [map type-alias-dependency-map]) + (define id (car component)) + (memf (λ (id2) (free-identifier=? id id2)) + (dict-ref map id))) + + ;; A singleton component can be either a self-cycle or a node that + ;; that does not participate in cycles, so we disambiguate + (define-values (acyclic-singletons recursive-aliases) + (for/fold ([singletons '()] [other '()]) + ([component (in-list components)]) + (if (and (= (length component) 1) + (not (has-self-cycle? component))) + (values (cons (car component) singletons) other) + (values singletons (append component other))))) + + ;; Check that no #:implements clauses are recursive + (define counterexample + (for/or ([component class-components]) + (and (or (not (= (length component) 1)) + (has-self-cycle? component type-alias-class-map)) + component))) + (when counterexample + (tc-error/stx + (car counterexample) + "Recursive #:implements clause not allowed")) + + ;; Split recursive aliases into those involving classes + ;; (in reverse topological order) and the rest of the aliases + (define class-aliases + (for/list ([component (in-list (reverse class-components))] + #:when (member (car component) + recursive-aliases + free-identifier=?)) + (car component))) + (define other-recursive-aliases + (for/list ([alias (in-list recursive-aliases)] + #:unless (member alias + class-aliases + free-identifier=?)) + alias)) + + ;; Reconstruct type alias dependency map based on class parent + ;; information. This ensures that the `deps` field is precise + ;; in all type aliases involving class types + (define (get-all-parent-deps id) + (define (get-deps parent) + (cdr (assoc parent type-alias-dependency-map free-identifier=?))) + (define parents (cdr (assoc id type-alias-class-map free-identifier=?))) + (cond [(null? parents) null] + [else + (define all-deps + (for/list ([parent parents]) + (append (get-deps parent) + (get-all-parent-deps parent)))) + (apply append all-deps)])) + + (define new-dependency-map/classes + (for/list ([(id deps) (in-dict type-alias-dependency-map)]) + (cond [(dict-has-key? type-alias-class-map id) + (define new-deps + (remove-duplicates (append (get-all-parent-deps id) deps) + free-identifier=?)) + (cons id new-deps)] + [else (cons id deps)]))) + + ;; Do another pass on dependency map, using the connected + ;; components analysis data to determine which dependencies are + ;; actually needed for mutual recursion. Drop all others. + (define new-dependency-map + (for/list ([(id deps) (in-dict new-dependency-map/classes)]) + ;; find the component this `id` participated in so + ;; that we can drop `deps` that aren't in that component + (define component + (findf (λ (component) (member id component free-identifier=?)) + components)) + (define new-deps + (filter (λ (dep) (member dep component free-identifier=?)) deps)) + (cons id new-deps))) + + ;; Actually register recursive type aliases + (for ([id (in-list recursive-aliases)]) + (define record (dict-ref type-alias-map id)) + (match-define (list _ args) record) + (define deps (dict-ref new-dependency-map id)) + (register-resolved-type-alias id (make-Name id deps args #f))) + + ;; Register non-recursive type aliases + ;; + ;; Note that the connected component algorithm returns results + ;; in topologically sorted order, so we want to go through in the + ;; reverse order of that to avoid unbound type aliases. + (for ([id (in-list acyclic-singletons)]) + (define type-stx (car (dict-ref type-alias-map id))) + (register-resolved-type-alias id (parse-type type-stx))) + + ;; Finish registering recursive aliases + ;; names-to-refine : Listof + ;; types-to-refine : Listof + ;; tvarss : Listof> + (define-values (names-to-refine types-to-refine tvarss) + (for/lists (_1 _2 _3) + ([id (in-list (append other-recursive-aliases class-aliases))]) + (define record (dict-ref type-alias-map id)) + (match-define (list type-stx args) record) + (define type + ;; make sure to reject the type if it uses polymorphic + ;; recursion (see resolve.rkt) + (parameterize ([current-check-polymorphic-recursion args]) + (parse-type type-stx))) + (register-type-name id type) + (add-constant-variance! id args) + (check-type-alias-contractive id type) + (values id type args))) + + ;; Finally, do a last pass to refine the variance + (refine-variance! names-to-refine types-to-refine tvarss))) + +;; Syntax -> Syntax Syntax Syntax Option +;; Parse a type alias internal declaration +(define (parse-type-alias form) + (kernel-syntax-case* form #f + (define-type-alias-internal values) + [(define-values () + (begin (quote-syntax (define-type-alias-internal nm ty args)) + (#%plain-app values))) + (values #'nm #'ty (syntax-e #'args))] + ;; this version is for `let`-like bodies + [(begin (quote-syntax (define-type-alias-internal nm ty args)) + (#%plain-app values)) + (values #'nm #'ty (syntax-e #'args))] + [_ (int-err "not define-type-alias")])) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/type-name-env.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/type-name-env.rkt index c80432b2..24d0e96b 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/type-name-env.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/type-name-env.rkt @@ -7,7 +7,7 @@ (require syntax/id-table (env type-alias-env) (utils tc-utils) - (rep type-rep) + (rep type-rep free-variance) (types utils)) (provide register-type-name @@ -18,7 +18,9 @@ register-type-variance! lookup-type-variance - type-variance-env-map) + type-variance-env-map + add-constant-variance! + refine-variance!) ;; a mapping from id -> type (where id is the name of the type) (define the-mapping @@ -50,7 +52,9 @@ (define (add-alias from to) (when (lookup-type-name to (lambda () #f)) - (register-resolved-type-alias from (make-Name to)))) + (register-resolved-type-alias + from + (make-Name to null #f #t)))) ;; a mapping from id -> listof[Variance] (where id is the name of the type) @@ -62,13 +66,38 @@ (define (register-type-variance! id variance) (free-id-table-set! variance-mapping id variance)) -(define (lookup-type-variance id ) - (free-id-table-ref variance-mapping id)) +(define (lookup-type-variance id) + (free-id-table-ref + variance-mapping id + (lambda () (lookup-variance-fail id)))) ;; map over the-mapping, producing a list ;; (id variance -> T) -> listof[T] (define (type-variance-env-map f) (free-id-table-map variance-mapping f)) +;; Listof Listof>> -> Void +;; Refines the variance of a type in the name environment +(define (refine-variance! names types tvarss) + (let loop () + (define sames? + (for/and ([name (in-list names)] + [type (in-list types)] + [tvars (in-list tvarss)]) + (cond + [(or (not tvars) (null? tvars)) #t] + [else + (define free-vars (free-vars-hash (free-vars* type))) + (define variance (map (λ (v) (hash-ref free-vars v Constant)) tvars)) + (define old-variance (lookup-type-variance name)) + (register-type-variance! name variance) + (equal? variance old-variance)]))) + (unless sames? (loop)))) + +;; Id Option> -> Void +;; Initialize variance of the given id to Constant for all type vars +(define (add-constant-variance! name vars) + (unless (or (not vars) (null? vars)) + (register-type-variance! name (map (lambda (_) Constant) vars)))) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt index fcc7a3fd..7726f2f9 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt @@ -450,6 +450,12 @@ ;; constrain v to be above S (but don't mention V) (singleton (var-promote S V) v Univ)] + ;; recursive names should get resolved as they're seen + [(s (? Name? t)) + (cg s (resolve-once t))] + [((? Name? s) t) + (cg (resolve-once s) t)] + ;; constrain b1 to be below T, but don't mention the new vars [((Poly: v1 b1) T) (cgen (append v1 V) X Y b1 T)] @@ -477,7 +483,7 @@ (cset-meet proc-c (cgen/flds V X Y flds flds*)))] ;; two struct names, need to resolve b/c one could be a parent - [((Name: n) (Name: n*)) + [((Name: n _ _ #t) (Name: n* _ _ #t)) (if (free-identifier=? n n*) null (let ((rn (resolve-once S)) (rn* (resolve-once T))) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt index 4349aab4..d2818a76 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt @@ -37,7 +37,32 @@ [parse-tc-results/id (syntax? c:any/c . c:-> . tc-results/c)] [parse-literal-alls (syntax? . c:-> . (c:listof (c:or/c (c:listof identifier?) (c:list/c (c:listof identifier?) identifier?))))]) -(provide star ddd/bound) +(provide star ddd/bound + current-referenced-aliases + current-referenced-class-parents + current-type-alias-name) + +;; current-type-alias-name : Parameter<(Option Id)> +;; This parameter stores the name of the type alias that is +;; being parsed (set in type-alias-helper.rkt), #f if the +;; parsing is not for a type alias +(define current-type-alias-name (make-parameter #f)) + +;; current-referenced-aliases : Parameter>>> +;; This parameter is used to coordinate with the type-checker to determine +;; if a type alias should be recursive or not +;; +;; interp. the argument is #f if not checking for type aliases. +;; Otherwise, it should be a box containing a list of +;; identifiers (i.e., type aliases in the syntax) +(define current-referenced-aliases (make-parameter #f)) + +;; current-referenced-class-parents : Parameter>>> +;; This parameter is used to coordinate with the type-checker about +;; the dependency structure of class types using #:implements +;; +;; interp. same as above +(define current-referenced-class-parents (make-parameter #f)) (define-literal-syntax-class #:for-label car) (define-literal-syntax-class #:for-label cdr) @@ -450,13 +475,11 @@ => (lambda (t) ;(printf "found a type alias ~a\n" #'id) + (when (current-referenced-aliases) + (define alias-box (current-referenced-aliases)) + (set-box! alias-box (cons #'id (unbox alias-box)))) (add-disappeared-use (syntax-local-introduce #'id)) t)] - ;; if it's a type name, we just use the name - [(lookup-type-name #'id (lambda () #f)) - (add-disappeared-use (syntax-local-introduce #'id)) - ;(printf "found a type name ~a\n" #'id) - (make-Name #'id)] [(free-identifier=? #'id #'->) (tc-error/delayed "Incorrect use of -> type constructor") Err] @@ -481,7 +504,7 @@ [args (parse-types #'(arg args ...))]) (resolve-app-check-error rator args stx) (match rator - [(Name: _) (make-App rator args stx)] + [(Name: _ _ _ _) (make-App rator args stx)] [(Poly: _ _) (instantiate-poly rator args)] [(Mu: _ _) (loop (unfold rator) args)] [(Error:) Err] @@ -560,10 +583,10 @@ ;;; Utilities for (Class ...) type parsing -;; process-class-clauses : Option Syntax FieldDict MethodDict AugmentDict +;; process-class-clauses : Option Type Stx FieldDict MethodDict AugmentDict ;; -> Option FieldDict MethodDict AugmentDict ;; Merges #:implements class type and the current class clauses appropriately -(define (merge-with-parent-type row-var stx fields methods augments) +(define (merge-with-parent-type row-var parent-type parent-stx fields methods augments) ;; (Listof Symbol) Dict Dict String -> (Values Dict Dict) ;; check for duplicates in a class clause (define (check-duplicate-clause names super-names types super-types err-msg) @@ -583,18 +606,16 @@ types (dict-remove super-types maybe-dup) err-msg)] [else - (tc-error/stx stx err-msg maybe-dup)])] + (tc-error/stx parent-stx err-msg maybe-dup)])] [else (values types super-types)])) - (define parent-type (parse-type stx)) (define (match-parent-type parent-type) - (match parent-type + (define resolved (resolve parent-type)) + (match resolved [(Class: row-var _ fields methods augments _) (values row-var fields methods augments)] - [(? Mu?) - (match-parent-type (unfold parent-type))] [_ (tc-error "expected a class type for #:implements clause, got ~a" - parent-type)])) + resolved)])) (define-values (super-row-var super-fields super-methods super-augments) (match-parent-type parent-type)) @@ -670,8 +691,8 @@ (syntax-parse stx [(kw (~var clause (class-type-clauses parse-type))) (add-disappeared-use #'kw) - - (define parent-types (stx->list #'clause.extends-types)) + (define parent-stxs (stx->list #'clause.extends-types)) + (define parent-types (map parse-type parent-stxs)) (define given-inits (attribute clause.inits)) (define given-fields (attribute clause.fields)) (define given-methods (attribute clause.methods)) @@ -683,31 +704,68 @@ (and (attribute clause.init-rest) (parse-type (attribute clause.init-rest)))) - (check-function-types given-methods) - (check-function-types given-augments) + ;; Only proceed to create a class type when the parsing + ;; process isn't looking for recursive type alias references. + ;; (otherwise the merging process will error) + (cond [(or (null? parent-stxs) + (not (current-referenced-aliases))) - ;; merge with all given parent types, erroring if needed - (define-values (row-var fields methods augments) - (for/fold ([row-var given-row-var] - [fields given-fields] - [methods given-methods] - [augments given-augments]) - ([parent-type parent-types]) - (merge-with-parent-type row-var parent-type fields - methods augments))) + (check-function-types given-methods) + (check-function-types given-augments) - ;; check constraints on row var for consistency with class - (when (and row-var (has-row-constraints? (F-n row-var))) - (define constraints (lookup-row-constraints (F-n row-var))) - (check-constraints given-inits (car constraints)) - (check-constraints fields (cadr constraints)) - (check-constraints methods (caddr constraints)) - (check-constraints augments (cadddr constraints))) + ;; merge with all given parent types, erroring if needed + (define-values (row-var fields methods augments) + (for/fold ([row-var given-row-var] + [fields given-fields] + [methods given-methods] + [augments given-augments]) + ([parent-type parent-types] + [parent-stx parent-stxs]) + (merge-with-parent-type row-var parent-type parent-stx + fields methods augments))) - (define class-type - (make-Class row-var given-inits fields methods augments given-init-rest)) + ;; check constraints on row var for consistency with class + (when (and row-var (has-row-constraints? (F-n row-var))) + (define constraints (lookup-row-constraints (F-n row-var))) + (check-constraints given-inits (car constraints)) + (check-constraints fields (cadr constraints)) + (check-constraints methods (caddr constraints)) + (check-constraints augments (cadddr constraints))) - class-type])) + (define class-type + (make-Class row-var given-inits fields methods augments given-init-rest)) + + class-type] + [else + ;; Conservatively assume that if there *are* #:implements + ;; clauses, then the current type alias will be recursive + ;; through one of the type aliases in the #:implements clauses. + ;; + ;; This is needed because it's hard to determine if a type + ;; in the #:implements clauses depends on the current + ;; type alias at this point. Otherwise, we would have to + ;; parse all type aliases again. + ;; + ;; An example type that is a problem without this assumption is + ;; alias = (Class #:implements Foo%) where Foo% + ;; has a class clause referring to alias + ;; since "alias" will be a non-recursive alias + ;; + ;; Without the approximation, we may miss recursive references + ;; which can cause infinite looping elsewhere in TR. + ;; + ;; With the approximation, we have spurious recursive references + ;; which may cause more indirection through the Name environment + ;; or generate worse contracts. + (define alias-box (current-referenced-aliases)) + (set-box! alias-box (cons (current-type-alias-name) + (unbox alias-box))) + (define class-box (current-referenced-class-parents)) + (set-box! class-box (append parent-stxs (unbox class-box))) + ;; Ok to return Error here, since this type will + ;; get reparsed in another pass + (make-Error) + ])])) ;; check-function-types : Dict -> Void ;; ensure all types recorded in the dictionary are function types diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt index 7744c526..557ab05e 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt @@ -7,7 +7,7 @@ syntax/parse (rep type-rep filter-rep object-rep) (utils tc-utils) - (env type-name-env) + (env type-name-env type-alias-env) (rep rep-utils) (types resolve union utils kw-types) (prefix-in t: (types abbrev numeric-tower)) @@ -194,7 +194,94 @@ (define (t->sc/method t) (t->sc/function t fail typed-side recursive-values loop #t)) (define (t->sc/fun t) (t->sc/function t fail typed-side recursive-values loop #f)) (match type - [(or (App: _ _ _) (Name: _)) (t->sc (resolve-once type))] + ;; Applications of implicit recursive type aliases + ;; + ;; We special case this rather than just resorting to standard + ;; App resolution (see case below) because the resolution process + ;; will make type->static-contract infinite loop. + [(App: (Name: name _ _ #f) rands _) + ;; Key with (cons name 'app) instead of just name because the + ;; application of the Name is not necessarily the same as the + ;; Name type alone + (cond [(hash-ref recursive-values (cons name 'app) #f)] + [else + (define name* (generate-temporary name)) + (recursive-sc (list name*) + (list + (t->sc (resolve-once type) + #:recursive-values + (hash-set recursive-values + (cons name 'app) + (recursive-sc-use name*)))) + (recursive-sc-use name*))])] + ;; Implicit recursive aliases + [(Name: name-id dep-ids args #f) + ;; FIXME: this may not be correct for different aliases that have + ;; the same name that are somehow used together, if that's + ;; possible + (define name (syntax-e name-id)) + (define deps (map syntax-e dep-ids)) + (cond [;; recursive references are looked up, see F case + (hash-ref recursive-values name #f) => + (λ (rv) (triple-lookup rv typed-side))] + [else + ;; see Mu case, which uses similar machinery + (match-define (and n*s (list untyped-n* typed-n* both-n*)) + (generate-temporaries (list name name name))) + (define-values (untyped-deps typed-deps both-deps) + (values (generate-temporaries deps) + (generate-temporaries deps) + (generate-temporaries deps))) + ;; Set recursive references for the `name` itself + (define *rv + (hash-set recursive-values name + (triple (recursive-sc-use untyped-n*) + (recursive-sc-use typed-n*) + (recursive-sc-use both-n*)))) + ;; Add in references for the dependency aliases + (define rv + (for/fold ([rv *rv]) + ([dep (in-list deps)] + [untyped-dep (in-list untyped-deps)] + [typed-dep (in-list typed-deps)] + [both-dep (in-list both-deps)]) + (hash-set rv dep + (triple (recursive-sc-use untyped-dep) + (recursive-sc-use typed-dep) + (recursive-sc-use both-dep))))) + (define resolved-name (resolve-once type)) + (define resolved-deps + (map (λ (dep) (lookup-type-alias dep values)) dep-ids)) + + ;; resolved-deps->scs : (U 'untyped 'typed 'both) + ;; -> (Listof Static-Contract) + (define (resolved-deps->scs typed-side) + (for/list ([resolved-dep resolved-deps]) + (loop resolved-dep typed-side rv))) + + ;; Now actually generate the static contracts + (case typed-side + [(both) (recursive-sc + (append (list both-n*) both-deps) + (cons (loop resolved-name 'both rv) + (resolved-deps->scs 'both)) + (recursive-sc-use both-n*))] + [(typed untyped) + (define untyped (loop resolved-name 'untyped rv)) + (define typed (loop resolved-name 'typed rv)) + (define both (loop resolved-name 'both rv)) + (define-values (untyped-dep-scs typed-dep-scs both-dep-scs) + (values + (resolved-deps->scs 'untyped) + (resolved-deps->scs 'typed) + (resolved-deps->scs 'both))) + (recursive-sc + (append n*s untyped-deps typed-deps both-deps) + (append (list untyped typed both) + untyped-dep-scs typed-dep-scs both-dep-scs) + (recursive-sc-use (if (from-typed? typed-side) typed-n* untyped-n*)))])])] + ;; Ordinary type applications or struct type names, just resolve + [(or (App: _ _ _) (Name: _ _ _ #t)) (t->sc (resolve-once type))] [(Univ:) (if (from-typed? typed-side) any-wrap/sc any/sc)] [(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var))))) (listof/sc (t->sc elem-ty))] diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt index caeca650..5b9fe1fd 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt @@ -111,10 +111,20 @@ (def-type F ([n symbol?]) [#:frees (single-free-var n) empty-free-vars] [#:fold-rhs #:base]) -;; id is an Identifier -;; This will always resolve to a struct -(def-type Name ([id identifier?]) [#:intern (hash-id id)] [#:frees #f] - [#:fold-rhs #:base]) +;; Name, an indirection of a type through the environment +;; +;; interp. +;; A type name, potentially recursive or mutually recursive or pointing +;; to a type for a struct type +;; id is the name stored in the environment +;; deps are the other aliases this depends on, if any +;; args are the type parameters for this type (or #f if none) +;; struct? indicates if this maps to a struct type +(def-type Name ([id identifier?] + [deps (listof identifier?)] + [args (or/c #f (listof identifier?))] + [struct? boolean?]) + [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base]) ;; rator is a type ;; rands is a list of types @@ -123,7 +133,7 @@ [#:intern (cons (Rep-seq rator) (map Rep-seq rands))] [#:frees (λ (f) (match rator - ((Name: n) + ((Name: n _ _ _) (instantiate-frees n (map f rands))) (else (f (resolve-app rator rands stx)))))] diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt index eb0eed06..f445d9d0 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt @@ -324,17 +324,20 @@ (define-values (super-row super-inits super-fields super-methods super-augments super-init-rest) (match super-type - [(tc-result1: (Class: super-row super-inits super-fields - super-methods super-augments super-init-rest)) - (values super-row super-inits super-fields - super-methods super-augments super-init-rest)] [(tc-result1: t) - (tc-error/expr/fields "type mismatch" - #:more "superclass expression should produce a class" - #:stx (hash-ref parse-info 'superclass-expr) - "expected" "a class" - "given" t) - (values #f null null null null #f)])) + (match (resolve t) + [(Class: super-row super-inits super-fields + super-methods super-augments super-init-rest) + (values super-row super-inits super-fields + super-methods super-augments super-init-rest)] + [t + (tc-error/expr/fields "type mismatch" + #:more "superclass expression should produce a class" + #:stx (hash-ref parse-info 'superclass-expr) + "expected" "a class" + "given" t) + (values #f null null null null #f)])] + [_ (int-err "Unhandled result")])) (define super-init-names (dict-keys super-inits)) (define super-field-names (dict-keys super-fields)) (define super-method-names (dict-keys super-methods)) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/internal-forms.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/internal-forms.rkt index b7ae7172..80461e4e 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/internal-forms.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/internal-forms.rkt @@ -99,7 +99,7 @@ (define-internal-classes [type-alias - (define-type-alias-internal name type)] + (define-type-alias-internal name type args)] [type-refinement (declare-refinement-internal predicate)] [typed-struct diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt index 00a9fc76..d34f39b2 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt @@ -143,10 +143,11 @@ ;; row var wasn't in the same position in some cases (fail)) (define idx (car row-var-idxs)) - (cond [(Class? (list-ref argtys-t idx)) + (define resolved-argty (resolve (list-ref argtys-t idx))) + (cond [(Class? resolved-argty) (define substitution (hash row-var - (t-subst (infer-row constraints (list-ref argtys-t idx))))) + (t-subst (infer-row constraints resolved-argty)))) (tc/funapp f-stx args-stx (ret (subst-all substitution f-ty)) argtys expected)] [else (fail)])] diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt index 515340eb..cf595fe9 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt @@ -4,7 +4,8 @@ (except-in (types utils abbrev union filter-ops) -> ->* one-of/c) (only-in (types abbrev) (-> t:->)) (private type-annotation parse-type syntax-properties) - (env lexical-env type-alias-env global-env type-env-structs scoped-tvar-env) + (env lexical-env type-alias-env type-alias-helper + global-env type-env-structs scoped-tvar-env) (rep type-rep filter-rep) syntax/free-vars (typecheck signatures tc-metafunctions tc-subst internal-forms) @@ -101,14 +102,24 @@ [clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])]) ;; Collect the declarations, which are represented as expression. ;; We put them back into definitions to reuse the existing machinery - (for ([body (in-list exprs)]) - (syntax-parse #`(define-values () #,body) - [t:type-alias - (register-resolved-type-alias #'t.name (parse-type #'t.type))] - [t:type-declaration - (register-type-if-undefined #'t.id (parse-type #'t.type)) - (register-scoped-tvars #'t.id (parse-literal-alls #'t.type))] - [_ (void)])) + (define-values (type-aliases declarations) + (for/fold ([aliases '()] [declarations '()]) + ([body (in-list exprs)]) + (syntax-parse #`(define-values () #,body) + [t:type-alias + (values (cons #'t aliases) declarations)] + [t:type-declaration + (values aliases (cons (list #'t.id #'t.type) declarations))] + [_ (values aliases declarations)]))) + + (define-values (alias-names alias-map) (get-type-alias-info type-aliases)) + (register-all-type-aliases alias-names alias-map) + + (for ([declaration declarations]) + (match-define (list id type) declaration) + (register-type-if-undefined id (parse-type type)) + (register-scoped-tvars id (parse-literal-alls type))) + ;; add scoped type variables, before we get to typechecking ;; FIXME: can this pass be fused with the one immediately above? (for ([n (in-list names)] [b (in-list exprs)]) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-send.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-send.rkt index e9d5573f..f4cee81a 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-send.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-send.rkt @@ -4,7 +4,7 @@ (require "../utils/utils.rkt" racket/match syntax/stx (typecheck signatures tc-funapp) - (types base-abbrev utils type-table) + (types base-abbrev resolve utils type-table) (rep type-rep) (utils tc-utils)) @@ -14,8 +14,8 @@ (define (tc/send form rcvr method args [expected #f]) (define (do-check rcvr-type) (match rcvr-type - [(tc-result1: (Instance: (? Mu? type))) - (do-check (ret (make-Instance (unfold type))))] + [(tc-result1: (Instance: (? needs-resolving? type))) + (do-check (ret (make-Instance (resolve type))))] [(tc-result1: (Instance: (and c (Class: _ _ _ methods _ _)))) (match (tc-expr method) [(tc-result1: (Value: (? symbol? s))) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt index 8b210618..d1d9c2de 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt @@ -8,7 +8,7 @@ (rep type-rep object-rep free-variance) (private parse-type syntax-properties) (types abbrev utils resolve substitute type-table struct-table) - (env global-env type-name-env tvar-env) + (env global-env type-name-env type-alias-env tvar-env) (utils tc-utils) (typecheck def-binding internal-forms) (for-syntax syntax/parse racket/base)) @@ -120,7 +120,13 @@ (define/cond-contract (register-sty! sty names desc) (c:-> Struct? struct-names? struct-desc? void?) - (register-type-name (struct-names-type-name names) + ;; a type alias needs to be registered here too, to ensure + ;; that parse-type will map the identifier to this Name type + (define type-name (struct-names-type-name names)) + (register-resolved-type-alias + type-name + (make-Name type-name null #f #t)) + (register-type-name type-name (make-Poly (struct-desc-tvars desc) sty))) @@ -139,10 +145,13 @@ ;; the base-type, with free type variables + (define name-type + (make-Name (struct-names-type-name names) + null #f #t)) (define poly-base (if (null? tvars) - (make-Name (struct-names-type-name names)) - (make-App (make-Name (struct-names-type-name names)) (map make-F tvars) #f))) + name-type + (make-App name-type (map make-F tvars) #f))) ;; is this structure covariant in *all* arguments? (define covariant? @@ -210,25 +219,13 @@ null (register-struct-bindings! sty names desc si))))) +;; Listof -> Void +;; Refines the variance of struct types in the name environment (define (refine-struct-variance! parsed-structs) (define stys (map parsed-struct-sty parsed-structs)) (define tvarss (map (compose struct-desc-tvars parsed-struct-desc) parsed-structs)) - (let loop () - (define sames - (for/list ((sty (in-list stys)) (tvars (in-list tvarss))) - (cond - ((null? tvars) #t) - (else - (define name (Struct-name sty)) - (define free-vars (free-vars-hash (free-vars* sty))) - (define variance (map (λ (v) (hash-ref free-vars v Constant)) tvars)) - (define old-variance (lookup-type-variance name)) - - (register-type-variance! name variance) - (equal? variance old-variance))))) - (unless (andmap values sames) - (loop)))) - + (define names (map Struct-name stys)) + (refine-variance! names stys tvarss)) ;; check and register types for a define struct ;; tc/struct : Listof[identifier] (U identifier (list identifier identifier)) @@ -285,7 +282,8 @@ (c:-> identifier? (c:or/c #f identifier?) (c:listof identifier?) (c:listof Type/c) (c:or/c #f identifier?) c:any/c) - (define parent-type (and parent (resolve-name (make-Name parent)))) + (define parent-type + (and parent (resolve-name (make-Name parent null #f #t)))) (define parent-tys (map fld-t (get-flds parent-type))) (define names (get-struct-names nm fld-names #f)) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt index dc4b657a..e91e264c 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt @@ -8,7 +8,8 @@ (types utils abbrev type-table struct-table) (private parse-type type-annotation type-contract syntax-properties) (env global-env init-envs type-name-env type-alias-env - lexical-env env-req mvar-env scoped-tvar-env) + lexical-env env-req mvar-env scoped-tvar-env + type-alias-helper) (utils tc-utils) (typecheck provide-handling def-binding tc-structs typechecker internal-forms) @@ -41,13 +42,6 @@ [t:typed-struct (attribute t.tvars)] [t:typed-struct/exec null])) -(define (add-constant-variance! name vars) - (unless (null? vars) - (register-type-variance! name (map (lambda (_) Constant) vars)))) - - - - ;; syntax? -> (listof def-binding?) (define (tc-toplevel/pass1 form) (parameterize ([current-orig-stx form]) @@ -249,10 +243,6 @@ [(define-syntaxes (nm ...) . rest) (syntax->list #'(nm ...))] [_ #f])) -(define (parse-type-alias form) - (syntax-parse form - [t:type-alias (values #'t.name #'t.type)])) - ;; actually do the work on a module ;; produces prelude and post-lude syntax objects ;; syntax-list -> (values syntax syntax) @@ -269,16 +259,23 @@ define/fixup-contract?)) (do-time "Form splitting done") ;(printf "before parsing type aliases~n") - (for-each (compose register-type-alias parse-type-alias) type-aliases) + + (define-values (type-alias-names type-alias-map) + (get-type-alias-info type-aliases)) + ;; Add the struct names to the type table, but not with a type ;(printf "before adding type names~n") (let ((names (map name-of-struct struct-defs)) (type-vars (map type-vars-of-struct struct-defs))) + (for ([name names]) + (register-resolved-type-alias + name (make-Name name null #f #t))) (for-each register-type-name names) (for-each add-constant-variance! names type-vars)) ;(printf "after adding type names~n") - ;; resolve all the type aliases, and error if there are cycles - (resolve-type-aliases parse-type) + + (register-all-type-aliases type-alias-names type-alias-map) + ;; Parse and register the structure types (define parsed-structs (for/list ((def (in-list struct-defs))) @@ -405,7 +402,9 @@ [_ ;; Handle type aliases (when (type-alias? form) - ((compose register-type-alias parse-type-alias) form)) + (define-values (alias-names alias-map) + (get-type-alias-info (list form))) + (register-all-type-aliases alias-names alias-map)) ;; Handle struct definitions (when (typed-struct? form) (define name (name-of-struct form)) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt index 95d49378..e154a7df 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt @@ -13,7 +13,8 @@ "types/kw-types.rkt" "types/utils.rkt" "utils/utils.rkt" - "utils/tc-utils.rkt") + "utils/tc-utils.rkt" + "env/type-name-env.rkt") (for-syntax racket/base syntax/parse)) ;; printer-type: (one-of/c 'custom 'debug) @@ -386,7 +387,7 @@ [(? Rep-stx a) (syntax->datum (Rep-stx a))] [(Univ:) 'Any] ;; names are just the printed as the original syntax - [(Name: stx) (syntax-e stx)] + [(Name: id _ _ _) (syntax-e id)] ;; If a type has a name, then print it with that name. ;; However, we expand the alias in some cases ;; (i.e., the fuel is > 0) for the :type form. diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/remove-intersect.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/remove-intersect.rkt index 4547ce3b..078f544b 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/remove-intersect.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/remove-intersect.rkt @@ -35,12 +35,12 @@ [(list _ (F: _)) #t] [(list (Opaque: _) _) #t] [(list _ (Opaque: _)) #t] - [(list (Name: n) (Name: n*)) + [(list (Name: n _ _ _) (Name: n* _ _ _)) (or (free-identifier=? n n*) (overlap (resolve-once t1) (resolve-once t2)))] - [(list _ (Name: _)) + [(list _ (Name: _ _ _ _)) (overlap t1 (resolve-once t2))] - [(list (Name: _) _) + [(list (Name: _ _ _ _) _) (overlap (resolve-once t1) t2)] [(list (? Mu?) _) (overlap (unfold t1) t2)] [(list _ (? Mu?)) (overlap t1 (unfold t2))] @@ -118,7 +118,7 @@ (if (subtype old rem) (Un) ;; the empty type (match (list old rem) - [(list (or (App: _ _ _) (Name: _)) t) + [(list (or (App: _ _ _) (Name: _ _ _ _)) t) ;; must be different, since they're not subtypes ;; and n must refer to a distinct struct type old] diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/resolve.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/resolve.rkt index 452f1a9f..5fccb2e4 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/resolve.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/resolve.rkt @@ -10,15 +10,34 @@ racket/format) (provide resolve-name resolve-app needs-resolving? - resolve resolve-app-check-error) + resolve resolve-app-check-error + current-cache-resolve? + current-check-polymorphic-recursion) (provide/cond-contract [resolve-once (Type/c . -> . (or/c Type/c #f))]) (define-struct poly (name vars) #:prefab) +;; This parameter allows other parts of the typechecker to +;; request that the resolve cache isn't updated. This is needed +;; by the setup for recursive type aliases, since certain Name +;; types should not be cached while their mapping is still being +;; computed. +(define current-cache-resolve? (make-parameter #f)) + +;; Parameter>> +;; This parameter controls whether or not the resolving process +;; should check for polymorphic recursion in implicit recursive +;; type names. This should only need to be enabled at type alias +;; definition time. +;; +;; If not #f, it should be a list of symbols that correspond +;; to the type parameters of the type being parsed. +(define current-check-polymorphic-recursion (make-parameter #f)) + (define (resolve-name t) (match t - [(Name: n) (let ([t (lookup-type-name n)]) - (if (Type/c? t) t #f))] + [(Name: n _ _ _) (let ([t (lookup-type-name n)]) + (if (Type/c? t) t #f))] [_ (int-err "resolve-name: not a name ~a" t)])) (define already-resolving? (make-parameter #f)) @@ -31,7 +50,7 @@ (unless (= n (length rands)) (tc-error "wrong number of arguments to polymorphic type: expected ~a and got ~a" n (length rands)))] - [(Name: n) + [(Name: n _ _ #t) (when (and (current-poly-struct) (free-identifier=? n (poly-name (current-poly-struct)))) (define num-rands (length rands)) @@ -48,6 +67,50 @@ " does not match the given number:" " expected " num-poly ", given " num-rands))))] + [(Name: _ _ args #f) + (cond [args + (define num-rands (length rands)) + (define num-args (length args)) + (unless (= num-rands num-args) + (tc-error (~a "The expected number of arguments for " + rator " does not match the given number:" + " expected " num-args + ", given " num-rands))) + ;; Does not allow polymorphic recursion since both type + ;; inference and equirecursive subtyping for polymorphic + ;; recursion are difficult. + ;; + ;; Type inference is known to be undecidable in general, but + ;; practical algorithms do exist[1] that do not diverge in + ;; practice. + ;; + ;; It is possible that equirecursive subtyping with polymorphic + ;; recursion is as difficult as equivalence of DPDAs[2], which is + ;; known to be decidable[3], but good algorithms may not exist. + ;; + ;; [1] Fritz Henglein. "Type inference with polymorphic recursion" + ;; TOPLAS 1993 + ;; [2] Marvin Solomon. "Type definitions with parameters" + ;; POPL 1978 + ;; [3] Geraud Senizergues. + ;; "L(A)=L(B)? decidability results from complete formal systems" + ;; TCS 2001. + ;; + ;; check-argument : Type Id -> Void + ;; Check argument to make sure there's no polymorphic recursion + (define (check-argument given-type arg-name) + (define ok? + (if (F? given-type) + (type-equal? given-type (make-F (syntax-e arg-name))) + (not (member (syntax-e arg-name) (fv given-type))))) + (unless ok? + (tc-error (~a "Recursive type " rator " cannot be applied at" + " a different type in its recursive invocation")))) + (define current-vars (current-check-polymorphic-recursion)) + (when current-vars + (for-each check-argument rands current-vars))] + [else + (tc-error "Type ~a cannot be applied, arguments were: ~a" rator rands)])] [(Mu: _ _) (void)] [(App: _ _ _) (void)] [(Error:) (void)] @@ -59,7 +122,7 @@ [already-resolving? #t]) (resolve-app-check-error rator rands stx) (match rator - [(Name: _) + [(Name: _ _ _ _) (let ([r (resolve-name rator)]) (and r (resolve-app r rands stx)))] [(Poly: _ _) (instantiate-poly rator rands)] @@ -81,8 +144,10 @@ [(Mu: _ _) (unfold t)] [(App: r r* s) (resolve-app r r* s)] - [(Name: _) (resolve-name t)])]) - (when (and r* (not (currently-subtyping?))) + [(Name: _ _ _ _) (resolve-name t)])]) + (when (and r* + (not (currently-subtyping?)) + (current-cache-resolve?)) (hash-set! resolver-cache seq r*)) r*))) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt index d4eea8d9..6a64a91c 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt @@ -181,8 +181,11 @@ (lambda (stx) (syntax-case stx () [(_ i) - #'(or (and (Name: _) (app resolve-once (? Struct? i))) - (App: (and (Name: _) (app resolve-once (Poly: _ (? Struct? i)))) _ _))]))) + #'(or (and (Name: _ _ _ #t) + (app resolve-once (? Struct? i))) + (App: (and (Name: _ _ _ #t) + (app resolve-once (Poly: _ (? Struct? i)))) + _ _))]))) (define (subtype/flds* A flds flds*) (for/fold ([A A]) ([f (in-list flds)] [f* (in-list flds*)] #:break (not A)) @@ -210,7 +213,8 @@ (or (free-identifier=? s-name p-name) (match s [(Poly: _ (? Struct? s*)) (in-hierarchy? s* par)] - [(Struct: _ (and (Name: _) p) _ _ _ _) (in-hierarchy? (resolve-once p) par)] + [(Struct: _ (and (Name: _ _ _ #t) p) _ _ _ _) + (in-hierarchy? (resolve-once p) par)] [(Struct: _ (? Struct? p) _ _ _ _) (in-hierarchy? p par)] [(Struct: _ (Poly: _ p) _ _ _ _) (in-hierarchy? p par)] [(Struct: _ #f _ _ _ _) #f] @@ -582,6 +586,16 @@ (subtype* s-out t-out))] [((Param: in out) t) (subtype* A0 (cl->* (-> out) (-> in -Void)) t)] + [((Instance: (? needs-resolving? s)) other) + (let ([s* (resolve-once s)]) + (if (Type/c? s*) + (subtype* A0 (make-Instance s*) other) + #f))] + [(other (Instance: (? needs-resolving? t))) + (let ([t* (resolve-once t)]) + (if (Type/c? t*) + (subtype* A0 other (make-Instance t*)) + #f))] [((Instance: (Class: _ _ field-map method-map augment-map _)) (Instance: (Class: _ _ field-map* method-map* augment-map* _))) (define (subtype-clause? map map*) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-error.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-error.rkt index ac91635d..756d4004 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-error.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-error.rkt @@ -14,7 +14,8 @@ #:rest (c:listof c:any/c) . c:->* . c:any/c)] [lookup-fail (identifier? . c:-> . Type/c)] - [lookup-type-fail (identifier? . c:-> . Type/c)]) + [lookup-type-fail (identifier? . c:-> . Type/c)] + [lookup-variance-fail (identifier? . c:-> . void?)]) ;; produce a type-checking error, and also return a result (e.g., a type) (define (tc-error/expr msg @@ -66,3 +67,6 @@ (define (lookup-type-fail i) (tc-error/expr "~a is not bound as a type" (syntax-e i))) + +(define (lookup-variance-fail i) + (int-err "~a is bound but missing a variance" (syntax-e i))) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/union.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/union.rkt index f17b81c5..7a0b7f60 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/union.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/union.rkt @@ -27,7 +27,7 @@ ;; If a union element is a Name application, then it should not ;; be checked for subtyping since that can cause infinite ;; loops if this is called during type instantiation. - [((App: (and (Name: _) rator) rands stx) _) + [((App: (? Name? rator) rands stx) _) ;; However, we should check if it's a well-formed application ;; so that bad applications are rejected early. (resolve-app-check-error rator rands stx) diff --git a/pkgs/typed-racket-pkgs/typed-racket-more/typed/pict.rkt b/pkgs/typed-racket-pkgs/typed-racket-more/typed/pict.rkt index f280a480..4150696a 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-more/typed/pict.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-more/typed/pict.rkt @@ -6,10 +6,10 @@ make-Union))) (begin-for-syntax - (define -pict (make-Name #'pict)) + (define -pict (make-Name #'pict null #f #t)) (define -pict-path (make-Union (list (-val #f) -pict (-lst -pict)))) - (define -child (make-Name #'child)) + (define -child (make-Name #'child null #f #t)) (define -pin-arrow-line (->key -Real -pict diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/even-odd-recursive-contract.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/even-odd-recursive-contract.rkt new file mode 100644 index 00000000..00c23708 --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/even-odd-recursive-contract.rkt @@ -0,0 +1,28 @@ +#; +(exn-pred #rx"blaming: \\(interface for even->odd\\)") +#lang racket/load + +;; Test mutually recursive type alias contract generation +;; with polymorphism + +(module untyped racket + (define (even->odd elem lst) (cons 3 lst)) + (provide even->odd)) + +(module poly-even/odd typed/racket + (define-type (Even A) (U Null (Pairof A (Odd A)))) + (define-type (Odd A) (Pairof A (Even A))) + + (: even-lst (Even Integer)) + (define even-lst '(1 2 3 4)) + + (: odd-lst (Odd Integer)) + (define odd-lst '(1 2 3)) + + (require/typed 'untyped + [even->odd (All (A) (A (Even A) -> (Odd A)))]) + + (even->odd 3 even-lst) ) + +(require 'poly-even/odd) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/polymorphic-recursion-2.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/polymorphic-recursion-2.rkt new file mode 100644 index 00000000..29f808fc --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/polymorphic-recursion-2.rkt @@ -0,0 +1,8 @@ +#; +(exn-pred #rx"cannot be applied at a different type") +#lang typed/racket + +;; Polymorphic recursion should fail + +(define-type (Foo A) (Listof (Foo (Listof A)))) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/polymorphic-recursion-3.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/polymorphic-recursion-3.rkt new file mode 100644 index 00000000..13b80b0f --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/polymorphic-recursion-3.rkt @@ -0,0 +1,12 @@ +#; +(exn-pred #rx"cannot be applied at a different type") +#lang typed/racket + +;; Polymorphic recursion should fail through mutual recursion + +(define-type (Foo A) (Listof (Bar (Listof A)))) +(define-type (Bar B) (Listof (Foo (Listof B)))) + +(define-type (Foo2 A) (Listof (Bar2 (Listof A)))) +(define-type (Bar2 B) (Listof (Foo2 B))) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/polymorphic-recursion.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/polymorphic-recursion.rkt new file mode 100644 index 00000000..997571a1 --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/polymorphic-recursion.rkt @@ -0,0 +1,39 @@ +#; +(exn-pred #rx"cannot be applied at a different type") +#lang typed/racket + +;; Example from Wikipedia +;; http://en.wikipedia.org/w/index.php?title=Polymorphic_recursion&oldid=543854337 + +;; Note that the following code does not work, but some +;; of it could work if polymorphic recursion were implemented +;; in the future. +;; +;; Right now the type definition of Nested should throw a static error + +(struct: (A B) :<: ([left : A] [right : B]) + #:transparent) +(struct: ε ()) + +;; Note that this type uses polymorphic recursion +(define-type (Nested A) + (U (:<: A (Nested (Listof A))) ε)) + +(: nested (Nested Integer)) +(define nested + (:<: 1 (:<: (list 2 3 4) (:<: (list (list 4 5) (list 7) (list 8 9)) (ε))))) + +;; inference loops forever for this one... +(: nested-length (All (A) ((Nested A) -> Integer))) +(define (nested-length n) + (if (ε? n) + 0 + ;; explicit instantiation needed + (add1 ((inst nested-length (Listof A)) (:<:-right n))))) + +;; Test subtyping with polymorphic recursion +(: nested2 (Nested Number)) +(define nested2 nested) + +(provide nested nested-length :<: Nested ε) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/recursive-type-application.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/recursive-type-application.rkt new file mode 100644 index 00000000..4e211002 --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/recursive-type-application.rkt @@ -0,0 +1,8 @@ +#; +(exn-pred #rx"does not match the given number:") +#lang typed/racket + +;; Check bad arity for recursive invocation of Foo + +(define-type (Foo A) (Listof (Foo A A))) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/both-recursive-types.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/both-recursive-types.rkt new file mode 100644 index 00000000..29283af8 --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/both-recursive-types.rkt @@ -0,0 +1,31 @@ +#lang typed/racket + +;; Make sure that recursive types defined using +;; different recursion methods are compatible with +;; each other + +(define-type (L1 A) (U Null (Pairof A (L1 A)))) +(define-type (L2 A) (Rec X (U Null (Pairof A X)))) +(define-type (L3 A) (Rec X (U Null (Pairof A (L3 A))))) + +(: x (L1 Integer)) +(define x '(1 2 3)) + +(: y (L2 Number)) +(define y x) + +(: z (L3 Number)) +(define z x) + +(: a (Listof Number)) +(define a x) + +(: b (L1 Number)) +(define b a) + +(: c (L1 Number)) +(define c y) + +(: d (L1 Number)) +(define d z) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/even-odd-recursive-type.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/even-odd-recursive-type.rkt new file mode 100644 index 00000000..0902cb8b --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/even-odd-recursive-type.rkt @@ -0,0 +1,75 @@ +#lang racket + +(require rackunit) + +(module num-even/odd typed/racket + (define-type Even (U Null (Pairof Number Odd))) + (define-type Odd (Pairof Number Even)) + + (: even-lst Even) + (define even-lst '(1 2 3 4)) + + (: odd-lst Odd) + (define odd-lst '(1 2 3))) + +(module poly-even/odd typed/racket + (define-type (Even A) (U Null (Pairof A (Odd A)))) + (define-type (Odd A) (Pairof A (Even A))) + + (: even-lst (Even Integer)) + (define even-lst '(1 2 3 4)) + + (: odd-lst (Odd Integer)) + (define odd-lst '(1 2 3)) + + (: even->odd (All (A) (A (Even A) -> (Odd A)))) + (define (even->odd elem lst) + (cons elem lst)) + + (provide even->odd Even Odd even-lst odd-lst)) + +;; make sure it works in a let +(module let-even/odd typed/racket + (let () + (define-type (Even A) (U Null (Pairof A (Odd A)))) + (define-type (Odd B) (Pairof B (Even B))) + + (: even-lst (Even Integer)) + (define even-lst '(1 2 3 4)) + + (: odd-lst (Odd Integer)) + (define odd-lst '(1 2 3)) + + (cons 3 even-lst))) + +(module even/odd* typed/racket + ;; weird variant that alternates types between + ;; Even and Odd + (define-type (Even A B) (U Null (Pairof A (Odd A B)))) + (define-type (Odd A B) (Pairof B (Even A B))) + + (: even-lst (Even Integer String)) + (define even-lst '(1 "b" 3 "a")) + + (: odd-lst (Odd Integer String)) + (define odd-lst '("b" 2 "a")) + + ;; specialized for more interesting contract + (: even->odd (String (Even Integer String) -> (Odd Integer String))) + (define (even->odd elem lst) (cons elem lst)) + + (provide even-lst odd-lst even->odd)) + +(require (prefix-in a: 'num-even/odd)) +(require (prefix-in b: 'poly-even/odd)) +(require (prefix-in c: 'let-even/odd)) +(require (prefix-in d: 'even/odd*)) + +;; make sure contract generation on even/odd* worked +(cons 3 d:odd-lst) +(check-equal? (d:even->odd "c" d:even-lst) '("c" 1 "b" 3 "a")) +(check-exn exn:fail:contract? (λ () (d:even->odd 1 d:even-lst))) + +(b:even->odd "c" b:even-lst) +(check-exn exn:fail:contract? (λ () (b:even->odd "c" b:odd-lst))) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/non-recursive-and-recursive-type-aliases.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/non-recursive-and-recursive-type-aliases.rkt new file mode 100644 index 00000000..20be1e4d --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/non-recursive-and-recursive-type-aliases.rkt @@ -0,0 +1,26 @@ +#lang typed/racket + +;; This test used to fail when the non-recursive type +;; aliases were registered *after* the recursive ones. +;; +;; Thanks to Havvy from IRC for the test + +(define-type magic/int Integer) +(define-type magic/float Flonum) +(define-type magic/str String) +(define-type magic/symbol Symbol) +(define-type magic/map HashTable) +(define-type magic/invokable (magic/any * -> magic/any)) +(define-type magic/any (U magic/int + magic/float + magic/str + magic/symbol + magic/map + magic/invokable)) + +(: x magic/any) +(define x "magic/str") + +(: f magic/invokable) +(define f (lambda: (rst : magic/any *) (car rst))) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/rec-type-alias-variance.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/rec-type-alias-variance.rkt new file mode 100644 index 00000000..a27df240 --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/rec-type-alias-variance.rkt @@ -0,0 +1,38 @@ +#lang typed/racket + +;; Test subtyping and variance for recursive type aliases + +(define-type (B X) + (U (Listof X) (Setof (B X)))) + +(: b1 (B String)) +(define b1 (list "foo")) + +(: b2 (B (U String Symbol))) +(define b2 b1) + +(: f (All (Y) (Y -> (B Y)))) +(define (f x) (list x)) + +(: g (All (X) (X -> (B X)))) +(define g f) + +;; Adapted from struct variance test +(define-type (Boxer D) (List (Boxer2 D))) +(define-type (Boxer2 D) (List (D -> Void) (Boxer D))) + +(: f-Boxer (All (D) ((Boxer D) D -> Void))) +(define (f-Boxer boxer v) + ((car (car boxer)) v)) + +;; The last line in this example would error without +;; registering the variance +(define-type (Even A) (U Null (Pairof A (Odd A)))) +(define-type (Odd A) (Pairof A (Even A))) + +(: even->odd (All (A) (A (Even A) -> (Odd A)))) +(define (even->odd elem lst) + (cons elem lst)) + +(even->odd 3 '(1 2)) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/recursive-type-alias-top-level.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/recursive-type-alias-top-level.rkt new file mode 100644 index 00000000..33131e22 --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/recursive-type-alias-top-level.rkt @@ -0,0 +1,20 @@ +#lang racket + +;; Make sure type aliases are registered from a module +;; to another context appropriately + +(require racket/sandbox) + +(define evaluator + (call-with-trusted-sandbox-configuration + (λ () (make-evaluator 'typed/racket)))) + +(evaluator '(require typed/racket)) +(evaluator '(module a typed/racket + (define-type (Foo A) (Option (Listof (Foo A)))) + (: x (Foo Integer)) + (define x #f) + (provide x))) +(evaluator '(require 'a)) +(evaluator 'x) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/all-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/all-tests.rkt index bbaf0b53..8eb18ff1 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/all-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/all-tests.rkt @@ -34,6 +34,7 @@ "contract-tests.rkt" "interactive-tests.rkt" "type-printer-tests.rkt" + "type-alias-helper.rkt" "class-tests.rkt" "class-util-tests.rkt" "check-below-tests.rkt" diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/type-alias-helper.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/type-alias-helper.rkt new file mode 100644 index 00000000..d0452a5b --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/type-alias-helper.rkt @@ -0,0 +1,78 @@ +#lang racket/base + +;; Unit tests for the type-alias-helper.rkt module + +(require "test-utils.rkt" + racket/set + rackunit + syntax/id-table + typed-racket/env/type-alias-helper) + +(provide tests) +(gen-test-main) + +;; two aliases in their own components +(define example-1 + (list (cons #'x (list #'x)) + (cons #'y (list #'y)))) +;; all one component +(define example-2 + (list (cons #'x (list #'x #'y)) + (cons #'y (list #'x)))) +;; two components, one with two nodes +(define example-3 + (list (cons #'x (list #'y)) + (cons #'y (list #'x)) + (cons #'z (list)))) +;; one with cycles, two that form a line +(define example-4 + (list (cons #'x (list #'y)) + (cons #'y (list #'x)) + (cons #'a (list #'b)) + (cons #'b (list)))) +;; two large cycles +(define example-5 + (list (cons #'x (list #'y #'z)) + (cons #'y (list #'x)) + (cons #'z (list #'x #'y)) + (cons #'a (list #'b)) + (cons #'b (list #'c)) + (cons #'c (list #'a)))) +;; check topological order +(define example-6 + (list (cons #'a (list #'b)) + (cons #'d (list)) + (cons #'c (list #'d #'e)) + (cons #'b (list #'c)) + (cons #'e (list #'f)) + (cons #'f (list)))) + +;; helper function for the tests below +;; ignores order of ids in the components and the +;; order of the components (because neither are stable +;; except for topological ordering). +(define (equal-id-sets? x y) + (define (id-lsts->id-sets id-lsts) + (for/set ([id-lst id-lsts]) + (for/set ([id id-lst]) (syntax-e id)))) + (equal? (id-lsts->id-sets x) + (id-lsts->id-sets y))) + +(define-binary-check (check-equal?/id equal-id-sets? actual expected)) + +(define tests + (test-suite + "Tests for type-alias-helper" + (check-equal?/id (find-strongly-connected-type-aliases example-1) + (list (list #'x) (list #'y))) + (check-equal?/id (find-strongly-connected-type-aliases example-2) + (list (list #'x #'y))) + (check-equal?/id (find-strongly-connected-type-aliases example-3) + (list (list #'z) (list #'x #'y))) + (check-equal?/id (find-strongly-connected-type-aliases example-4) + (list (list #'a) (list #'b) (list #'y #'x))) + (check-equal?/id (find-strongly-connected-type-aliases example-5) + (list (list #'b #'a #'c) (list #'z #'x #'y))) + (check-equal?/id (find-strongly-connected-type-aliases example-6) + (list (list #'a) (list #'b) (list #'c) + (list #'e) (list #'f) (list #'d))))) diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt index 54941843..c569b85d 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt @@ -2398,6 +2398,23 @@ void)) (display "hello" accumulator/not-thread-safe)) -Void] + + ;; Additional tests for recursive type aliases + [tc-e ;; The types here are valid, but uninhabitable. + (let () (define-type-alias A (Listof B)) + (define-type-alias B (Listof A)) + "dummy") + #:ret (ret -String -true-filter)] + [tc-e (let () (define-type-alias A (Listof B)) + (define-type-alias B (U #f (Listof A))) + (: a A) + (define a (list #f (list (list #f)))) + (void)) + -Void] + [tc-err (let () (define-type-alias A (Class #:implements A)) "dummy") + #:msg "Recursive #:implements clause not allowed"] + [tc-err (let () (define-type-alias X (U X #f)) "dummy") + #:msg "Recursive types are not allowed directly inside"] ) (test-suite "tc-literal tests"