suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

More progress on refactoring infer

Browse Source
This commit is contained in:
Sam Tobin-Hochstadt 2010-06-02 19:09:34 -04:00
parent 18f45c4138
commit 82e7d281cb
8 changed files with 287 additions and 302 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
collects/typed-scheme/infer/constraint-structs.rkt
View File

@ -4,22 +4,23 @@
;; S, T types ;; S, T types
;; X a var ;; X a var
(define-struct c (S X T) #:prefab) ;; represents S <: X <: T
(d-s/c c ([S Type/c] [X symbol?] [T Type/c]) #:transparent)
;; fixed : Listof[c] ;; fixed : Listof[c]
;; rest : option[c] ;; rest : option[c]
(define-struct dcon (fixed rest) #:prefab) (d-s/c dcon ([fixed (listof c?)] [rest (or/c c? #f)]) #:transparent)
;; fixed : Listof[c] ;; fixed : Listof[c]
;; rest : c ;; rest : c
(define-struct dcon-exact (fixed rest) #:prefab) (d-s/c dcon-exact ([fixed (listof c?)] [rest c?]) #:transparent)
;; type : c ;; type : c
;; bound : var ;; bound : var
(define-struct dcon-dotted (type bound) #:prefab) (d-s/c dcon-dotted ([type c?] [bound symbol?]) #:transparent)
;; map : hash mapping variable to dcon or dcon-dotted ;; map : hash mapping variable to dcon or dcon-dotted
(define-struct dmap (map) #:prefab) (d-s/c dmap ([map (hash/c symbol? (or/c dcon? dcon-exact? dcon-dotted?))]) #:transparent)
;; maps is a list of pairs of ;; maps is a list of pairs of
;; - functional maps from vars to c's ;; - functional maps from vars to c's
@ -27,17 +28,13 @@
;; we need a bunch of mappings for each cset to handle case-lambda ;; we need a bunch of mappings for each cset to handle case-lambda
;; because case-lambda can generate multiple possible solutions, and we ;; because case-lambda can generate multiple possible solutions, and we
;; don't want to rule them out too early ;; don't want to rule them out too early
(define-struct cset (maps) #:prefab) (d-s/c cset ([maps (listof (cons/c (hash/c symbol? c?) dmap?))]) #:transparent)
(define-match-expander c: (define-match-expander c:
(lambda (stx) (lambda (stx)
(syntax-parse stx (syntax-parse stx
[(_ s x t) [(_ s x t)
#'(struct c ((app (lambda (v) (if (Type? v) v (Un))) s) x (app (lambda (v) (if (Type? v) v Univ)) t)))]))) #'(struct c (s x t))])))
(p/c (struct c ([S (or/c boolean? Type?)] [X symbol?] [T (or/c boolean? Type?)])) (provide (struct-out cset) (struct-out dmap) (struct-out dcon) (struct-out dcon-dotted) (struct-out dcon-exact) (struct-out c)
(struct dcon ([fixed (listof c?)] [rest (or/c c? false/c)])) c:)
(struct dcon-exact ([fixed (listof c?)] [rest c?]))
(struct dcon-dotted ([type c?] [bound symbol?]))
(struct dmap ([map (hash/c symbol? (or/c dcon? dcon-exact? dcon-dotted?))]))
(struct cset ([maps (listof (cons/c (hash/c symbol? c?) dmap?))])))

6
collects/typed-scheme/infer/dmap.rkt
View File

@ -2,14 +2,15 @@
(require "../utils/utils.rkt" (require "../utils/utils.rkt"
"signatures.rkt" "constraint-structs.rkt" "signatures.rkt" "constraint-structs.rkt"
(utils tc-utils) (utils tc-utils) racket/contract
unstable/sequence unstable/hash scheme/match) unstable/sequence unstable/hash scheme/match)
(import constraints^) (import constraints^)
(export dmap^) (export dmap^)
;; dcon-meet : dcon dcon -> dcon ;; dcon-meet : dcon dcon -> dcon
(define (dcon-meet dc1 dc2) (d/c (dcon-meet dc1 dc2)
(dcon? dcon? . -> . dcon?)
(match* (dc1 dc2) (match* (dc1 dc2)
[((struct dcon-exact (fixed1 rest1)) (or (struct dcon (fixed2 rest2)) [((struct dcon-exact (fixed1 rest1)) (or (struct dcon (fixed2 rest2))
(struct dcon-exact (fixed2 rest2)))) (struct dcon-exact (fixed2 rest2))))
@ -20,6 +21,7 @@
[c2 fixed2]) [c2 fixed2])
(c-meet c1 c2 (c-X c1))) (c-meet c1 c2 (c-X c1)))
(c-meet rest1 rest2 (c-X rest1)))] (c-meet rest1 rest2 (c-X rest1)))]
;; redo in the other order to call the first case
[((struct dcon (fixed1 rest1)) (struct dcon-exact (fixed2 rest2))) [((struct dcon (fixed1 rest1)) (struct dcon-exact (fixed2 rest2)))
(dcon-meet dc2 dc1)] (dcon-meet dc2 dc1)]
[((struct dcon (fixed1 #f)) (struct dcon (fixed2 #f))) [((struct dcon (fixed1 #f)) (struct dcon (fixed2 #f)))

2
collects/typed-scheme/infer/infer-dummy.rkt
View File

@ -4,6 +4,6 @@
(require (rep type-rep) (utils tc-utils) mzlib/trace) (require (rep type-rep) (utils tc-utils) mzlib/trace)
(define infer-param (make-parameter (lambda e (int-err "infer not initialized")))) (define infer-param (make-parameter (lambda e (int-err "infer not initialized"))))
(define (unify X S T) ((infer-param) X null S T (make-Univ) null null)) (define (unify X S T) ((infer-param) X null S T (make-Univ)))
;(trace unify) ;(trace unify)
(provide unify infer-param) (provide unify infer-param)

486
collects/typed-scheme/infer/infer-unit.rkt
View File

@ -7,12 +7,12 @@
"rep/free-variance.rkt" "rep/type-rep.rkt" "rep/filter-rep.rkt" "rep/rep-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" "types/convenience.rkt" "types/union.rkt" "types/subtype.rkt" "types/remove-intersect.rkt" "types/resolve.rkt"
"env/type-name-env.rkt" "env/index-env.rkt" "env/tvar-env.rkt") "env/type-name-env.rkt" "env/index-env.rkt" "env/tvar-env.rkt")
make-env) make-env -> ->* one-of/c)
"constraint-structs.rkt" "constraint-structs.rkt"
"signatures.rkt" "signatures.rkt"
scheme/match scheme/match
mzlib/etc mzlib/etc
mzlib/trace mzlib/trace racket/contract
unstable/sequence unstable/list unstable/debug unstable/sequence unstable/list unstable/debug
scheme/list) scheme/list)
@ -68,275 +68,253 @@
(define (move-vars-to-dmap cset dbound vars) (define (move-vars-to-dmap cset dbound vars)
(mover cset dbound vars (mover cset dbound vars
(lambda (cmap) (λ (cmap)
(make-dcon (for/list ([v vars]) (make-dcon (for/list ([v vars])
(hash-ref cmap v (hash-ref cmap v
(lambda () (int-err "No constraint for new var ~a" v)))) (λ () (int-err "No constraint for new var ~a" v))))
#f)))) #f))))
(define (move-rest-to-dmap cset dbound #:exact [exact? #f]) (define (move-rest-to-dmap cset dbound #:exact [exact? #f])
(mover cset dbound (list dbound) (mover cset dbound (list dbound)
(lambda (cmap) (λ (cmap)
((if exact? make-dcon-exact make-dcon) ((if exact? make-dcon-exact make-dcon)
null null
(hash-ref cmap dbound (hash-ref cmap dbound
(lambda () (int-err "No constraint for bound ~a" dbound))))))) (λ () (int-err "No constraint for bound ~a" dbound)))))))
(define (move-vars+rest-to-dmap cset dbound vars #:exact [exact? #f]) (define (move-vars+rest-to-dmap cset dbound vars #:exact [exact? #f])
(map/cset (mover cset dbound vars
(lambda (cmap dmap) (λ (cmap)
(cons (hash-remove* cmap vars)
(dmap-meet
(singleton-dmap
dbound
((if exact? make-dcon-exact make-dcon) ((if exact? make-dcon-exact make-dcon)
(for/list ([v vars]) (for/list ([v vars])
(hash-ref cmap v (hash-ref cmap v (λ () (int-err "No constraint for new var ~a" v))))
(lambda () (int-err "No constraint for new var ~a" v))))
(hash-ref cmap dbound (hash-ref cmap dbound
(lambda () (int-err "No constraint for bound ~a" dbound))))) (λ () (int-err "No constraint for bound ~a" dbound)))))))
dmap)))
cset))
;; t and s must be *latent* filters ;; s and t must be *latent* filters
(define (cgen/filter V X t s) (define (cgen/filter V X s t)
(match* (t s) (match* (s t)
[(e e) (empty-cset X)] [(e e) (empty-cset X)]
[(e (Top:)) (empty-cset X)] [(e (Top:)) (empty-cset X)]
;; FIXME - is there something to be said about the logical ones? ;; FIXME - is there something to be said about the logical ones?
[((TypeFilter: t p i) (TypeFilter: s p i)) (cset-meet (cgen V X t s) (cgen V X s t))] [((TypeFilter: s p i) (TypeFilter: t p i)) (cset-meet (cgen V X s t) (cgen V X t s))]
[((NotTypeFilter: t p i) (NotTypeFilter: s p i)) (cset-meet (cgen V X t s) (cgen V X s t))] [((NotTypeFilter: s p i) (NotTypeFilter: t p i)) (cset-meet (cgen V X s t) (cgen V X t s))]
[(_ _) (fail! t s)])) [(_ _) (fail! s t)]))
#; ;; s and t must be *latent* filter sets
(define (cgen/filters V X ts ss) (define (cgen/filter-set V X s t)
(cond (match* (s t)
[(null? ss) (empty-cset X)]
;; FIXME - this can be less conservative
[(= (length ts) (length ss))
(cset-meet* (for/list ([t ts] [s ss]) (cgen/filter V X t s)))]
[else (fail! ts ss)]))
;; t and s must be *latent* filter sets
(define (cgen/filter-set V X t s)
(match* (t s)
[(e e) (empty-cset X)] [(e e) (empty-cset X)]
[((FilterSet: t+ t-) (FilterSet: s+ s-)) [((FilterSet: s+ s-) (FilterSet: t+ t-))
(cset-meet (cgen/filter V X t+ s+) (cgen/filter V X t- s-))] (cset-meet (cgen/filter V X s+ t+) (cgen/filter V X s- t-))]
[(_ _) (fail! t s)])) [(_ _) (fail! s t)]))
(define (cgen/object V X t s) (define (cgen/object V X s t)
(match* (t s) (match* (s t)
[(e e) (empty-cset X)] [(e e) (empty-cset X)]
[(e (Empty:)) (empty-cset X)] [(e (Empty:)) (empty-cset X)]
;; FIXME - do something here ;; FIXME - do something here
[(_ _) (fail! t s)])) [(_ _) (fail! s t)]))
(define (cgen/arr V X t-arr s-arr) (define (cgen/arr V X s-arr t-arr)
(define (cg S T) (cgen V X S T)) (define (cg S T) (cgen V X S T))
(match* (t-arr s-arr) (match* (s-arr t-arr)
[((arr: ts t #f #f '()) ;; the simplest case - no rests, drests, keywords
(arr: ss s #f #f '())) [((arr: ss s #f #f '())
(cset-meet* (arr: ts t #f #f '()))
(list (cgen/list V X ss ts) (cset-meet* (list
(cg t s)))] ;; contravariant
[((arr: ts t t-rest #f '()) (cgen/list V X ts ss)
(arr: ss s s-rest #f '())) ;; covariant
(cg s t)))]
;; just a rest arg, no drest, no keywords
[((arr: ss s s-rest #f '())
(arr: ts t t-rest #f '()))
(let ([arg-mapping (let ([arg-mapping
(cond [(and t-rest s-rest (<= (length ts) (length ss))) (cond
(cgen/list V X (cons s-rest ss) (cons t-rest (extend ss ts t-rest)))] ;; both rest args are present, so make them the same length
[(and t-rest s-rest (>= (length ts) (length ss))) [(and s-rest t-rest)
(cgen/list V X (cons s-rest (extend ts ss s-rest)) (cons t-rest ts))] (cgen/list V X (cons t-rest (extend ss ts t-rest)) (cons s-rest (extend ts ss s-rest)))]
[(and t-rest (not s-rest) (<= (length ts) (length ss))) ;; no rest arg on the right, so just pad the left and forget the rest arg
(cgen/list V X ss (extend ss ts t-rest))] [(and s-rest (not t-rest) (<= (length ss) (length ts)))
[(and s-rest (not t-rest) (>= (length ts) (length ss))) (cgen/list V X ts (extend ts ss s-rest))]
(cgen/list V X (extend ts ss s-rest) ts)] ;; no rest arg on the left, or wrong number = fail
[else (fail! S T)])] [else (fail! S T)])]
[ret-mapping (cg t s)]) [ret-mapping (cg s t)])
(cset-meet* (cset-meet* (list arg-mapping ret-mapping)))]
(list arg-mapping ret-mapping)))] ;; dotted on the left, nothing on the right
[((arr: ts t #f (cons dty dbound) '()) [((arr: ss s #f (cons dty dbound) '())
(arr: ss s #f #f '())) (arr: ts t #f #f '()))
(unless (memq dbound X)
(fail! S T))
(unless (<= (length ts) (length ss))
(fail! S T))
(let* ([num-vars (- (length ss) (length ts))]
[vars (for/list ([n (in-range num-vars)])
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound dty))]
[new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f null) s-arr)])
(move-vars-to-dmap new-cset dbound vars))]
[((arr: ts t #f #f '())
(arr: ss s #f (cons dty dbound) '()))
(unless (memq dbound X) (unless (memq dbound X)
(fail! S T)) (fail! S T))
(unless (<= (length ss) (length ts)) (unless (<= (length ss) (length ts))
(fail! S T)) (fail! S T))
(let* ([num-vars (- (length ts) (length ss))] (let* ([vars (for/list ([n (in-range (- (length ts) (length ss)))])
[vars (for/list ([n (in-range num-vars)])
(gensym dbound))] (gensym dbound))]
[new-tys (for/list ([var vars]) [new-tys (for/list ([var vars])
(substitute (make-F var) dbound dty))] (substitute (make-F var) dbound dty))]
[new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f null))]) [new-s-arr (make-arr (append ss new-tys) s #f #f null)]
[new-cset (cgen/arr V (append vars X) new-s-arr t-arr)])
(move-vars-to-dmap new-cset dbound vars))] (move-vars-to-dmap new-cset dbound vars))]
[((arr: ts t #f (cons t-dty dbound) '()) ;; dotted on the right, nothing on the left
(arr: ss s #f (cons s-dty dbound) '())) [((arr: ss s #f #f '())
(unless (= (length ts) (length ss)) (arr: ts t #f (cons dty dbound) '()))
(unless (memq dbound X)
(fail! S T))
(unless (<= (length ts) (length ss))
(fail! S T))
(let* ([vars (for/list ([n (in-range (- (length ss) (length ts)))])
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound dty))]
[new-t-arr (make-arr (append ts new-tys) t #f #f null)]
[new-cset (cgen/arr V (append vars X) s-arr new-t-arr)])
(move-vars-to-dmap new-cset dbound vars))]
;; this case is just for constrainting other variables, not dbound
[((arr: ss s #f (cons s-dty dbound) '())
(arr: ts t #f (cons t-dty dbound) '()))
(unless (= (length ss) (length ts))
(fail! S T)) (fail! S T))
;; If we want to infer the dotted bound, then why is it in both types? ;; If we want to infer the dotted bound, then why is it in both types?
(when (memq dbound X) (when (memq dbound X)
(fail! S T)) (fail! S T))
(let* ([arg-mapping (cgen/list V X ss ts)] (let* ([arg-mapping (cgen/list V X ts ss)]
[darg-mapping (cgen V X s-dty t-dty)] [darg-mapping (cgen V X t-dty s-dty)]
[ret-mapping (cg t s)]) [ret-mapping (cg s t)])
(cset-meet* (cset-meet*
(list arg-mapping darg-mapping ret-mapping)))] (list arg-mapping darg-mapping ret-mapping)))]
[((arr: ts t #f (cons t-dty dbound) '()) ;; bounds are different
(arr: ss s #f (cons s-dty dbound*) '())) [((arr: ss s #f (cons s-dty dbound) '())
(unless (= (length ts) (length ss)) (arr: ts t #f (cons t-dty dbound*) '()))
(unless (= (length ss) (length ts))
(fail! S T)) (fail! S T))
(let* ([arg-mapping (cgen/list V X ss ts)] (let* ([arg-mapping (cgen/list V X ts ss)]
[darg-mapping (cgen V (cons dbound* X) s-dty t-dty)] ;; just add dbound as something that can be constrained
[ret-mapping (cg t s)]) [darg-mapping (cgen V (cons dbound X) t-dty s-dty)]
[ret-mapping (cg s t)])
(cset-meet* (cset-meet*
(list arg-mapping darg-mapping ret-mapping)))] (list arg-mapping darg-mapping ret-mapping)))]
[((arr: ts t t-rest #f '()) [((arr: ss s s-rest #f '())
(arr: ss s #f (cons s-dty dbound) '())) (arr: ts t #f (cons t-dty dbound) '()))
(unless (memq dbound X) (unless (memq dbound X)
(fail! S T)) (fail! S T))
(if (<= (length ts) (length ss)) (if (<= (length ss) (length ts))
;; the simple case ;; the simple case
(let* ([arg-mapping (cgen/list V X ss (extend ss ts t-rest))] (let* ([arg-mapping (cgen/list V X ts (extend ts ss s-rest))]
[darg-mapping (move-rest-to-dmap (cgen V X s-dty t-rest) dbound)] [darg-mapping (move-rest-to-dmap (cgen V X t-dty s-rest) dbound)]
[ret-mapping (cg t s)]) [ret-mapping (cg s t)])
(cset-meet* (list arg-mapping darg-mapping ret-mapping))) (cset-meet* (list arg-mapping darg-mapping ret-mapping)))
;; the hard case ;; the hard case
(let* ([num-vars (- (length ts) (length ss))] (let* ([vars (for/list ([n (in-range (- (length ss) (length ts)))])
[vars (for/list ([n (in-range num-vars)])
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound s-dty))]
[new-cset (cgen/arr V (append vars X) t-arr
(make-arr (append ss new-tys) s #f (cons s-dty dbound) null))])
(move-vars+rest-to-dmap new-cset dbound vars)))]
;; If dotted <: starred is correct, add it below. Not sure it is.
[((arr: ts t #f (cons t-dty dbound) '())
(arr: ss s s-rest #f '()))
(unless (memq dbound X)
(fail! S T))
(cond [(< (length ts) (length ss))
;; the hard case
(let* ([num-vars (- (length ss) (length ts))]
[vars (for/list ([n (in-range num-vars)])
(gensym dbound))] (gensym dbound))]
[new-tys (for/list ([var vars]) [new-tys (for/list ([var vars])
(substitute (make-F var) dbound t-dty))] (substitute (make-F var) dbound t-dty))]
[arg-mapping (cgen/list V (append vars X) ss (append ts new-tys))] [new-t-arr (make-arr (append ts new-tys) t #f (cons t-dty dbound) null)]
[darg-mapping (cgen V X s-rest t-dty)] [new-cset (cgen/arr V (append vars X) s-arr new-t-arr)])
[ret-mapping (cg t s)] (move-vars+rest-to-dmap new-cset dbound vars)))]
[new-cset ;; If dotted <: starred is correct, add it below. Not sure it is.
(cset-meet* (list arg-mapping darg-mapping ret-mapping))]) [((arr: ss s #f (cons s-dty dbound) '())
(arr: ts t t-rest #f '()))
(unless (memq dbound X)
(fail! S T))
(cond [(< (length ss) (length ts))
;; the hard case
(let* ([vars (for/list ([n (in-range (- (length ts) (length ss)))])
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound s-dty))]
[new-s-arr (make-arr (append ss new-tys) s #f (cons s-dty dbound) null)]
[new-cset (cgen/arr V (append vars X) new-s-arr t-arr)])
(move-vars+rest-to-dmap new-cset dbound vars #:exact #t))] (move-vars+rest-to-dmap new-cset dbound vars #:exact #t))]
[else [else
;; the simple case ;; the simple case
(let* ([arg-mapping (cgen/list V X (extend ts ss s-rest) ts)] (let* ([arg-mapping (cgen/list V X (extend ss ts t-rest) ss)]
[darg-mapping (move-rest-to-dmap (cgen V X s-rest t-dty) dbound #:exact #t)] [darg-mapping (move-rest-to-dmap (cgen V X t-rest s-dty) dbound #:exact #t)]
[ret-mapping (cg t s)]) [ret-mapping (cg s t)])
(cset-meet* (list arg-mapping darg-mapping ret-mapping)))])] (cset-meet* (list arg-mapping darg-mapping ret-mapping)))])]
[(_ _) (fail! S T)])) [(_ _) (fail! S T)]))
;; determine constraints on the variables in X that would make S a subtype of T ;; V : a set of variables not to mention in the constraints
;; the resulting constraints will not mention V ;; X : the set of variables to be constrained
(define (cgen V X S T) ;; S : a type to be the subtype of T
;; T : a type
;; produces a cset which determines a substitution that makes S a subtype of T
;; implements the V |-_X S <: T => C judgment from Pierce+Turner
(d/c (cgen V X S T)
((listof symbol?) (listof symbol?) Type? Type? . -> . cset?)
;; useful quick loop
(define (cg S T) (cgen V X S T)) (define (cg S T) (cgen V X S T))
;; this places no constraints on any variables in X
(define empty (empty-cset X)) (define empty (empty-cset X))
(define (singleton S X T) ;; this constrains just x (which is a single var)
(insert empty X S T)) (define (singleton S x T)
(insert empty x S T))
;; if we've been around this loop before, we're done (for rec types)
(if (seen? S T) (if (seen? S T)
empty empty
(parameterize ([match-equality-test (lambda (a b) (if (and (Rep? a) (Rep? b)) (type-equal? a b) (equal? a b)))] (parameterize ([match-equality-test (lambda (a b) (if (and (Rep? a) (Rep? b)) (type-equal? a b) (equal? a b)))]
;; remember S and T, and obtain everything we've seen from the context
;; we can't make this an argument since we may call back and forth with subtyping, for example
[current-seen (remember S T (current-seen))]) [current-seen (remember S T (current-seen))])
(match* (match* (S T)
(S T) ;; if they're equal, no constraints are necessary (CG-Refl)
[(a a) empty] [(a a) empty]
;; CG-Top
[(_ (Univ:)) empty] [(_ (Univ:)) empty]
;; refinements are erased to their bound
[((Refinement: S _ _) T) [((Refinement: S _ _) T)
(cg S T)] (cg S T)]
[((F: (? (lambda (e) (memq e X)) v)) S) ;; variables that are in X and should be constrained
(when (match S ;; all other variables are compatible only with themselves
[(F: v*) [((F: (? (λ (e) (memq e X)) v)) T)
(and (bound-index? v*) (not (bound-tvar? v*)))] (match T
[_ #f]) ;; only possible when v* is an index
(fail! S T)) [(F: v*) (when (and (bound-index? v*) (not (bound-tvar? v*)))
(singleton (Un) v (var-demote S V))] (fail! S T))]
[_ (void)])
;; constrain v to be below T (but don't mention V)
(singleton (Un) v (var-demote T V))]
[(S (F: (? (lambda (e) (memq e X)) v))) [(S (F: (? (lambda (e) (memq e X)) v)))
(when (match S (match S
[(F: v*) [(F: v*) (when (and (bound-index? v*) (not (bound-tvar? v*)))
(and (bound-index? v*) (not (bound-tvar? v*)))] (fail! S T))]
[_ #f]) [_ (void)])
(fail! S T)) ;; constrain v to be above S (but don't mention V)
(singleton (var-promote S V) v Univ)] (singleton (var-promote S V) v Univ)]
;; two unions with the same number of elements, so we just try to unify them pairwise ;; constrain b1 to be below T, but don't mention the new vars
#;[((Union: l1) (Union: l2)) [((Poly: v1 b1) T) (cgen (append v1 V) X b1 T)]
(=> unmatch)
(unless (= (length l1) (length l2))
(unmatch))
(cgen-union V X l1 l2)]
#;[((Poly: v1 b1) (Poly: v2 b2)) ;; constrain *each* element of es to be below T, and then combine the constraints
(unless (= (length v1) (length v2)) [((Union: es) T) (cset-meet* (cons empty (for/list ([e es]) (cg e T))))]
(fail! S T))
(let ([b2* (subst-all (map list v2 v1) b2)])
(cg b1 b2*))]
#;[((PolyDots: (list v1 ... r1) b1) (PolyDots: (list v2 ... r2) b2)) ;; find *an* element of es which can be made to be a supertype of S
(unless (= (length v1) (length v2)) ;; FIXME: we're using multiple csets here, but I don't think it makes a difference
(fail! S T)) ;; not using multiple csets will break for: ???
(let ([b2* (substitute-dotted v1 v1 v2 (subst-all (map list v2 v1) b2))]) [(S (Union: es))
(cg b1 b2*))] (cset-combine
(filter values
[((Poly: v1 b1) T) (for/list ([e es])
(cgen (append v1 V) X b1 T)] (with-handlers ([exn:infer? (λ _ #f)]) (cg S e)))))]
#;[((PolyDots: (list v1 ... r1) b1) T)
(let ([b1* (var-demote b1 (cons r1 v1))])
(cg b1* T))]
#;
[((Poly-unsafe: n b) (Poly-unsafe: n* b*))
(unless (= n n*)
(fail! S T))
(cg b b*)]
[((Union: es) S) (cset-meet* (cons empty (for/list ([e es]) (cg e S))))]
;; we might want to use multiple csets here, but I don't think it makes a difference
[(S (Union: es)) (or
(for/or
([e es])
(with-handlers
([exn:infer? (lambda _ #f)])
(cg S e)))
(fail! S T))]
;; two structs with the same name and parent
;; just check pairwise on the fields
;; FIXME - wrong for mutable structs!
[((Struct: nm p flds proc _ _ _ _ _) (Struct: nm p flds* proc* _ _ _ _ _)) [((Struct: nm p flds proc _ _ _ _ _) (Struct: nm p flds* proc* _ _ _ _ _))
(let-values ([(flds flds*) (let-values ([(flds flds*)
(cond [(and proc proc*) (cond [(and proc proc*)
(values (cons proc flds) (cons proc* flds*))] (values (cons proc flds) (cons proc* flds*))]
[(or proc proc*)
(fail! S T)]
[else (values flds flds*)])]) [else (values flds flds*)])])
(cgen/list V X flds flds*))] (cgen/list V X flds flds*))]
;; two struct names, need to resolve b/c one could be a parent
[((Name: n) (Name: n*)) [((Name: n) (Name: n*))
(if (free-identifier=? n n*) (if (free-identifier=? n n*)
null null
(fail! S T))] (cg (resolve-once S) (resolve-once T)))]
;; pairs are pointwise
[((Pair: a b) (Pair: a* b*)) [((Pair: a b) (Pair: a* b*))
(cset-meet (cg a a*) (cg b b*))] (cset-meet (cg a a*) (cg b b*))]
;; sequences are covariant ;; sequences are covariant
@ -362,108 +340,126 @@
(cg t t*)] (cg t t*)]
[((Hashtable: k v) (Sequence: (list k* v*))) [((Hashtable: k v) (Sequence: (list k* v*)))
(cgen/list V X (list k v) (list k* v*))] (cgen/list V X (list k v) (list k* v*))]
;; ListDots can be below a Listof
;; must be above mu unfolding ;; must be above mu unfolding
[((ListDots: s-dty dbound) (Listof: t-elem)) [((ListDots: s-dty dbound) (Listof: t-elem))
(when (memq dbound X) (fail! S T)) (when (memq dbound X) (fail! S T))
(cgen V X (substitute Univ dbound s-dty) t-elem)] (cgen V X (substitute Univ dbound s-dty) t-elem)]
;; two ListDots with the same bound, just check the element type
[((ListDots: s-dty dbound) (ListDots: t-dty dbound)) [((ListDots: s-dty dbound) (ListDots: t-dty dbound))
(when (memq dbound X) (fail! S T)) (when (memq dbound X) (fail! S T))
(cgen V X s-dty t-dty)] (cgen V X s-dty t-dty)]
;; this constrains `dbound' to be |ts| - |ss|
[((ListDots: s-dty dbound) (List: ts))
(unless (memq dbound X) (fail! S T))
(let* ([vars (for/list ([n (in-range (length ts))])
(gensym dbound))]
;; new-tys are dummy plain type variables, standing in for the elements of dbound that need to be generated
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound s-dty))]
;; generate constraints on the prefixes, and on the dummy types
[new-cset (cgen/list V (append vars X) new-tys ts)])
;; now take all the dummy types, and use them to constrain dbound appropriately
(move-vars-to-dmap new-cset dbound vars))]
;; if we have two mu's, we rename them to have the same variable ;; if we have two mu's, we rename them to have the same variable
;; and then compare the bodies ;; and then compare the bodies
;; This relies on (B 0) only unifying with itself, and thus only hitting the first case of this `match'
[((Mu-unsafe: s) (Mu-unsafe: t)) [((Mu-unsafe: s) (Mu-unsafe: t))
(cg s t)] (cg s t)]
;; other mu's just get unfolded ;; other mu's just get unfolded
[(s (? Mu? t)) (cg s (unfold t))] [(s (? Mu? t)) (cg s (unfold t))]
[((? Mu? s) t) (cg (unfold s) t)] [((? Mu? s) t) (cg (unfold s) t)]
;; type application
[((App: (Name: n) args _) ;; resolve applications
(App: (Name: n*) args* _))
(unless (free-identifier=? n n*)
(fail! S T))
(cg (resolve-once S) (resolve-once T))]
[((App: _ _ _) _) (cg (resolve-once S) T)] [((App: _ _ _) _) (cg (resolve-once S) T)]
[(_ (App: _ _ _)) (cg S (resolve-once T))] [(_ (App: _ _ _)) (cg S (resolve-once T))]
;; values are covariant
[((Values: ss) (Values: ts)) [((Values: ss) (Values: ts))
(unless (= (length ss) (length ts)) (unless (= (length ss) (length ts))
(fail! ss ts)) (fail! ss ts))
(cgen/list V X ss ts)] (cgen/list V X ss ts)]
[((Values: ss) (ValuesDots: ts t-dty dbound))
(unless (>= (length ss) (length ts)) ;; this constrains `dbound' to be |ts| - |ss|
(fail! ss ts))
(unless (memq dbound X)
(fail! S T))
(let* ([num-vars (- (length ss) (length ts))]
[vars (for/list ([n (in-range num-vars)])
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound t-dty))]
[new-cset (cgen/list V (append vars X) ss (append ts new-tys))])
(move-vars-to-dmap new-cset dbound vars))]
[((ValuesDots: ss s-dty dbound) (Values: ts)) [((ValuesDots: ss s-dty dbound) (Values: ts))
(unless (>= (length ts) (length ss)) (unless (>= (length ts) (length ss)) (fail! ss ts))
(fail! ss ts)) (unless (memq dbound X) (fail! S T))
(unless (memq dbound X)
(fail! S T)) (let* ([vars (for/list ([n (in-range (- (length ts) (length ss)))])
(let* ([num-vars (- (length ts) (length ss))]
[vars (for/list ([n (in-range num-vars)])
(gensym dbound))] (gensym dbound))]
;; new-tys are dummy plain type variables, standing in for the elements of dbound that need to be generated
[new-tys (for/list ([var vars]) [new-tys (for/list ([var vars])
(substitute (make-F var) dbound s-dty))] (substitute (make-F var) dbound s-dty))]
;; generate constraints on the prefixes, and on the dummy types
[new-cset (cgen/list V (append vars X) (append ss new-tys) ts)]) [new-cset (cgen/list V (append vars X) (append ss new-tys) ts)])
;; now take all the dummy types, and use them to constrain dbound appropriately
(move-vars-to-dmap new-cset dbound vars))] (move-vars-to-dmap new-cset dbound vars))]
;; identical bounds - just unify pairwise
[((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound)) [((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound))
(when (memq dbound X) (fail! ss ts)) (when (memq dbound X) (fail! ss ts))
(cgen/list V X (cons s-dty ss) (cons t-dty ts))] (cgen/list V X (cons s-dty ss) (cons t-dty ts))]
;; vectors are invariant - generate constraints *both* ways
[((Vector: e) (Vector: e*)) [((Vector: e) (Vector: e*))
(cset-meet (cg e e*) (cg e* e))] (cset-meet (cg e e*) (cg e* e))]
;; boxes are invariant - generate constraints *both* ways
[((Box: e) (Box: e*)) [((Box: e) (Box: e*))
(cset-meet (cg e e*) (cg e* e))] (cset-meet (cg e e*) (cg e* e))]
[((MPair: s t) (MPair: s* t*)) [((MPair: s t) (MPair: s* t*))
(cset-meet* (list (cg s s*) (cg s* s) (cg t t*) (cg t* t)))] (cset-meet* (list (cg s s*) (cg s* s) (cg t t*) (cg t* t)))]
[((Channel: e) (Channel: e*)) [((Channel: e) (Channel: e*))
(cset-meet (cg e e*) (cg e* e))] (cset-meet (cg e e*) (cg e* e))]
;; we assume all HTs are mutable at the moment
[((Hashtable: s1 s2) (Hashtable: t1 t2)) [((Hashtable: s1 s2) (Hashtable: t1 t2))
;; for mutable hash tables, both are invariant ;; for mutable hash tables, both are invariant
(cset-meet* (list (cg t1 s1) (cg s1 t1) (cg t2 s2) (cg s2 t2)))] (cset-meet* (list (cg t1 s1) (cg s1 t1) (cg t2 s2) (cg s2 t2)))]
;; syntax is covariant
[((Syntax: s1) (Syntax: s2)) [((Syntax: s1) (Syntax: s2))
(cg s1 s2)] (cg s1 s2)]
;; parameters are just like one-arg functions ;; parameters are just like one-arg functions
[((Param: in1 out1) (Param: in2 out2)) [((Param: in1 out1) (Param: in2 out2))
(cset-meet (cg in2 in1) (cg out1 out2))] (cset-meet (cg in2 in1) (cg out1 out2))]
;; every function is trivially below top-arr
[((Function: _) [((Function: _)
(Function: (list (top-arr:)))) (Function: (list (top-arr:))))
empty] empty]
[((Function: (list t-arr ...)) [((Function: (list s-arr ...))
(Function: (list s-arr ...))) (Function: (list t-arr ...)))
(=> unmatch) (cset-meet*
(cset-combine (for/list ([t-arr t-arr])
(filter ;; for each element of t-arr, we need to get at least one element of s-arr that works
values ;; only generate the successful csets (let ([results (filter values
(for*/list (for/list ([s-arr s-arr])
([t-arr t-arr] [s-arr s-arr])
(with-handlers ([exn:infer? (lambda (_) #f)]) (with-handlers ([exn:infer? (lambda (_) #f)])
(cgen/arr V X t-arr s-arr)))))] (cgen/arr V X s-arr t-arr))))])
;; this is overly conservative ;; ensure that something produces a constraint set
(when (null? results) (fail! S T))
(cset-combine results))))]
;; check each element
[((Result: s f-s o-s) [((Result: s f-s o-s)
(Result: t f-t o-t)) (Result: t f-t o-t))
(cset-meet* (list (cg s t) (cset-meet* (list (cg s t)
(cgen/filter-set V X f-s f-t) (cgen/filter-set V X f-s f-t)
(cgen/object V X o-s o-t)))] (cgen/object V X o-s o-t)))]
[(_ _) [(_ _)
(cond [(subtype S T) empty] (cond
;; subtypes are easy - should this go earlier?
[(subtype S T) empty]
;; or, nothing worked, and we fail ;; or, nothing worked, and we fail
[else (fail! S T)])])))) [else (fail! S T)])]))))
(define (check-vars must-vars subst) (d/c (subst-gen C R)
(and (for/and ([v must-vars]) (cset? Type? . -> . (or/c #f list?))
(assq v subst)) ;; fixme - should handle these separately
subst)) (define must-vars (append (fv R) (fi R)))
(define (subst-gen C R must-vars)
(define (constraint->type v #:variable [variable #f]) (define (constraint->type v #:variable [variable #f])
(match v (match v
[(struct c (S X T)) [(struct c (S X T))
;; fixme - handle free indexes, remove Dotted
(let ([var (hash-ref (free-vars* R) (or variable X) Constant)]) (let ([var (hash-ref (free-vars* R) (or variable X) Constant)])
;(printf "variance was: ~a~nR was ~a~nX was ~a~nS T ~a ~a~n" var R (or variable X) S T) ;(printf "variance was: ~a~nR was ~a~nX was ~a~nS T ~a ~a~n" var R (or variable X) S T)
(evcase var (evcase var
@ -473,26 +469,34 @@
[Invariant S] [Invariant S]
[Dotted T]))])) [Dotted T]))]))
(match (car (cset-maps C)) (match (car (cset-maps C))
[(cons cmap (struct dmap (dm))) [(cons cmap (dmap dm))
(check-vars (let ([subst (append
must-vars
(append
(for/list ([(k dc) (in-hash dm)]) (for/list ([(k dc) (in-hash dm)])
(match dc (match dc
[(struct dcon (fixed rest)) [(dcon fixed rest)
(list k (list k
(for/list ([f fixed]) (for/list ([f fixed])
(constraint->type f #:variable k)) (constraint->type f #:variable k))
(and rest (constraint->type rest)))] (and rest (constraint->type rest)))]
[(struct dcon-exact (fixed rest)) [(dcon-exact fixed rest)
(list k (list k
(for/list ([f fixed]) (for/list ([f fixed])
(constraint->type f #:variable k)) (constraint->type f #:variable k))
(constraint->type rest))])) (constraint->type rest))]))
(for/list ([(k v) (in-hash cmap)]) (for/list ([(k v) (in-hash cmap)])
(list k (constraint->type v)))))])) (list k (constraint->type v))))])
;; verify that we got all the important variables
(and (for/and ([v must-vars])
(assq v subst))
subst))]))
(define (cgen/list V X S T) ;; V : a set of variables not to mention in the constraints
;; X : the set of variables to be constrained
;; S : a list of types to be the subtypes of T
;; T : a list of types
;; produces a cset which determines a substitution that makes the Ss subtypes of the Ts
(d/c (cgen/list V X S T)
((listof symbol?) (listof symbol?) (listof Type?) (listof Type?) . -> . cset?)
(unless (= (length S) (length T)) (unless (= (length S) (length T))
(fail! S T)) (fail! S T))
(cset-meet* (for/list ([s S] [t T]) (cgen V X s t)))) (cset-meet* (for/list ([s S] [t T]) (cgen V X s t))))
@ -502,25 +506,23 @@
;; S : actual argument types ;; S : actual argument types
;; T : formal argument types ;; T : formal argument types
;; R : result type ;; R : result type
;; must-vars : variables that must be in the substitution
;; must-idxs : index variables that must be in the substitution
;; expected : boolean ;; expected : boolean
;; returns a substitution ;; returns a substitution
;; if R is #f, we don't care about the substituion ;; if R is #f, we don't care about the substituion
;; just return a boolean result ;; just return a boolean result
(define (infer X Y S T R must-vars must-idxs [expected #f]) (define (infer X Y S T R [expected #f])
(with-handlers ([exn:infer? (lambda _ #f)]) (with-handlers ([exn:infer? (lambda _ #f)])
(let* ([cs (cgen/list null (append X Y) S T)] (let* ([cs (cgen/list null (append X Y) S T)]
[cs* (if expected [cs* (if expected
(cset-meet cs (cgen null (append X Y) R expected)) (cset-meet cs (cgen null (append X Y) R expected))
cs)]) cs)])
(subst-gen cs* R (append must-vars must-idxs))))) (if R (subst-gen cs* R) #t))))
;; like infer, but T-var is the vararg type: ;; like infer, but T-var is the vararg type:
(define (infer/vararg X Y S T T-var R must-vars must-idxs [expected #f]) (define (infer/vararg X Y S T T-var R [expected #f])
(define new-T (if T-var (extend S T T-var) T)) (define new-T (if T-var (extend S T T-var) T))
(and ((length S) . >= . (length T)) (and ((length S) . >= . (length T))
(infer X Y S new-T R must-vars must-idxs expected))) (infer X Y S new-T R expected)))
;; like infer, but dotted-var is the bound on the ... ;; like infer, but dotted-var is the bound on the ...
;; and T-dotted is the repeated type ;; and T-dotted is the repeated type
@ -537,7 +539,7 @@
[cs-dotted* (move-vars-to-dmap cs-dotted dotted-var new-vars)] [cs-dotted* (move-vars-to-dmap cs-dotted dotted-var new-vars)]
[cs (cset-meet cs-short cs-dotted*)]) [cs (cset-meet cs-short cs-dotted*)])
(if (not expected) (if (not expected)
(subst-gen cs R must-vars) (subst-gen cs R)
(subst-gen (cset-meet cs (cgen null X R expected)) R must-vars))))) (subst-gen (cset-meet cs (cgen null X R expected)) R)))))
;(trace cgen) ;(trace cgen)

2
collects/typed-scheme/infer/restrict.rkt
View File

@ -23,7 +23,7 @@
[(subtype t1 t2) t1] ;; already a subtype [(subtype t1 t2) t1] ;; already a subtype
[(match t2 [(match t2
[(Poly: vars t) [(Poly: vars t)
(let ([subst (infer vars null (list t1) (list t) t1 (fv t1) (fi t1))]) (let ([subst (infer vars null (list t1) (list t) t1)])
(and subst (restrict* t1 (subst-all subst t1))))] (and subst (restrict* t1 (subst-all subst t1))))]
[_ #f])] [_ #f])]
[(Union? t1) (union-map (lambda (e) (restrict* e t2)) t1)] [(Union? t1) (union-map (lambda (e) (restrict* e t2)) t1)]

12
collects/typed-scheme/infer/signatures.rkt
View File

@ -39,11 +39,7 @@
;; domain ;; domain
(listof Type?) (listof Type?)
;; range ;; range
Type? (or/c #f Type?))
;; free variables
(listof symbol?)
;; free indexes
(listof symbol?))
;; optional expected type ;; optional expected type
((or/c #f Type?)) ((or/c #f Type?))
. ->* . any)] . ->* . any)]
@ -58,11 +54,7 @@
;; rest ;; rest
(or/c #f Type?) (or/c #f Type?)
;; range ;; range
Type? (or/c #f Type?))
;; free variables
(listof symbol?)
;; free indexes
(listof symbol?))
;; [optional] expected type ;; [optional] expected type
((or/c #f Type?)) . ->* . any)] ((or/c #f Type?)) . ->* . any)]
[cnt infer/dots (((listof symbol?) [cnt infer/dots (((listof symbol?)

2
collects/typed-scheme/rep/type-rep.rkt
View File

@ -227,7 +227,7 @@
;; name : symbol ;; name : symbol
;; parent : Struct ;; parent : Struct
;; flds : Listof[Cons[Type,Bool]] type and mutability ;; flds : Listof[Type]
;; proc : Function Type ;; proc : Function Type
;; poly? : is this a polymorphic type? ;; poly? : is this a polymorphic type?
;; pred-id : identifier for the predicate of the struct ;; pred-id : identifier for the predicate of the struct

28
collects/typed-scheme/typecheck/tc-app.rkt
View File

@ -324,9 +324,7 @@
(cons (make-Listof (car rests*)) (cons (make-Listof (car rests*))
(car doms*)) (car doms*))
(car rests*) (car rests*)
(car rngs*) (car rngs*)))
(fv (car rngs*))
(fi (car rngs*))))
=> (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))] => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
;; actual work, when we have a * function and ... final arg ;; actual work, when we have a * function and ... final arg
[(and (car rests*) [(and (car rests*)
@ -338,9 +336,7 @@
(cons (make-Listof (car rests*)) (cons (make-Listof (car rests*))
(car doms*)) (car doms*))
(car rests*) (car rests*)
(car rngs*) (car rngs*)))
(fv (car rngs*))
(fi (car rngs*))))
=> (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))] => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg ;; ... function, ... arg
[(and (car drests*) [(and (car drests*)
@ -349,7 +345,7 @@
(= (length (car doms*)) (= (length (car doms*))
(length arg-tys)) (length arg-tys))
(infer vars null (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (infer vars null (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*))
(car rngs*) (fv (car rngs*)) (fi (car rngs*)))) (car rngs*)))
=> (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))] => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
;; if nothing matches, around the loop again ;; if nothing matches, around the loop again
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
@ -381,8 +377,7 @@
(cons (make-Listof (car rests*)) (cons (make-Listof (car rests*))
(car doms*)) (car doms*))
(car rests*) (car rests*)
(car rngs*) (car rngs*)))
(fv (car rngs*)) (fi (car rngs*))))
=> (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))] => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
;; actual work, when we have a * function and ... final arg ;; actual work, when we have a * function and ... final arg
[(and (car rests*) [(and (car rests*)
@ -394,8 +389,7 @@
(cons (make-Listof (car rests*)) (cons (make-Listof (car rests*))
(car doms*)) (car doms*))
(car rests*) (car rests*)
(car rngs*) (car rngs*)))
(fv (car rngs*)) (fi (car rngs*))))
=> (lambda (substitution) => (lambda (substitution)
(do-ret (subst-all substitution (car rngs*))))] (do-ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg, same bound on ... ;; ... function, ... arg, same bound on ...
@ -407,8 +401,7 @@
(infer fixed-vars (list dotted-var) (infer fixed-vars (list dotted-var)
(cons tail-ty arg-tys) (cons tail-ty arg-tys)
(cons (car (car drests*)) (car doms*)) (cons (car (car drests*)) (car doms*))
(car rngs*) (car rngs*)))
(fv (car rngs*)) (fi (car rngs*))))
=> (lambda (substitution) => (lambda (substitution)
(do-ret (subst-all substitution (car rngs*))))] (do-ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg, different bound on ... ;; ... function, ... arg, different bound on ...
@ -423,8 +416,7 @@
(infer fixed-vars (list dotted-var) (infer fixed-vars (list dotted-var)
(cons tail-ty arg-tys) (cons tail-ty arg-tys)
(cons (car (car drests*)) (car doms*)) (cons (car (car drests*)) (car doms*))
(car rngs*) (car rngs*)))))
(fv (car rngs*)) (fi (car rngs*))))))
=> (lambda (substitution) => (lambda (substitution)
(define drest-bound (cdr (car drests*))) (define drest-bound (cdr (car drests*)))
(do-ret (substitute-dotted (cadr (assq drest-bound substitution)) (do-ret (substitute-dotted (cadr (assq drest-bound substitution))
@ -621,7 +613,7 @@
(fail)) (fail))
(match (map single-value (syntax->list #'pos-args)) (match (map single-value (syntax->list #'pos-args))
[(list (tc-result1: argtys-t) ...) [(list (tc-result1: argtys-t) ...)
(let* ([subst (infer vars null argtys-t dom rng (fv rng) (fi rng) (and expected (tc-results->values expected)))]) (let* ([subst (infer vars null argtys-t dom rng (and expected (tc-results->values expected)))])
(tc-keywords form (list (subst-all subst ar)) (tc-keywords form (list (subst-all subst ar))
(type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected))])] (type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected))])]
[(tc-result1: (Function: arities)) [(tc-result1: (Function: arities))
@ -839,7 +831,7 @@
(if drest (if drest
(infer/dots fixed-vars dotted-var argtys-t dom (car drest) rng (fv rng) (infer/dots fixed-vars dotted-var argtys-t dom (car drest) rng (fv rng)
#:expected (and expected (tc-results->values expected))) #:expected (and expected (tc-results->values expected)))
(infer/vararg fixed-vars (list dotted-var) argtys-t dom rest rng (fv rng) (fi rng) (infer/vararg fixed-vars (list dotted-var) argtys-t dom rest rng
(and expected (tc-results->values expected))))) (and expected (tc-results->values expected)))))
t argtys expected)] t argtys expected)]
;; regular polymorphic functions without dotted rest, and without mandatory keyword args ;; regular polymorphic functions without dotted rest, and without mandatory keyword args
@ -854,7 +846,7 @@
(lambda (dom _ rest a) ((if rest <= =) (length dom) (length argtys))) (lambda (dom _ rest a) ((if rest <= =) (length dom) (length argtys)))
;; only try to infer the free vars of the rng (which includes the vars in filters/objects) ;; only try to infer the free vars of the rng (which includes the vars in filters/objects)
;; note that we have to use argtys-t here, since argtys is a list of tc-results ;; note that we have to use argtys-t here, since argtys is a list of tc-results
(lambda (dom rng rest a) (infer/vararg vars null argtys-t dom rest rng (fv rng) (fi rng) (and expected (tc-results->values expected)))) (lambda (dom rng rest a) (infer/vararg vars null argtys-t dom rest rng (and expected (tc-results->values expected))))
t argtys expected)] t argtys expected)]
;; procedural structs ;; procedural structs
[((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _ _ _))) _) [((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _ _ _))) _)