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

Improve type inference for ListDots

Browse Source 
This provides better inference for the case when trying
to infer a ListDots in a negative position against a List
type. For example, when trying to apply `time-apply`.
This commit is contained in:
Asumu Takikawa 2014-02-16 11:18:40 -05:00
parent 5ada90bfd2
commit 18adcb5b04
2 changed files with 20 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
View File

@ -577,6 +577,17 @@
;; now take all the dummy types, and use them to constrain dbound appropriately
(move-vars-to-dmap new-cset dbound vars))]
;; same as above, constrains `dbound' to be |ss| - |ts|
[((List: ss) (ListDots: t-dty dbound))
(unless (memq dbound Y) (fail! S T))
;; see comments for last case, we flip s and t though
(let* ([vars (var-store-take dbound t-dty (length ss))]
[new-tys (for/list ([var (in-list vars)])
(substitute (make-F var) dbound t-dty))]
[new-cset (cgen/list V (append vars X) Y ss new-tys)])
(move-vars-to-dmap new-cset dbound vars))]
;; if we have two mu's, we rename them to have the same variable
;; and then compare the bodies
;; This relies on (B 0) only unifying with itself, and thus only hitting the first case of this `match'

9
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
View File

@ -2019,6 +2019,15 @@
#:ret (ret (t:-> (t:Un (-Param -Symbol -Symbol) -Symbol) -Symbol))
#:expected (ret (t:-> (t:Un (-Param -Symbol -Symbol) -Symbol) -Symbol))]
;; time-apply and similar functions (test improved inference)
[tc-e (let ()
(: f (All (b a ...) (-> (List a ... a) b b)))
(define (f lst x) x)
(f '(a b) "foo"))
-String]
[tc-e (time-apply (lambda: ([x : Symbol] [y : Symbol]) "foo") '(a b))
#:ret (ret (list (-lst* -String) -Nat -Nat -Nat))]
;; test kw function without type annotation
[tc-e (let () (tr:define (f x #:y y) y) (f 'a #:y 'b)) Univ]
[tc-e (let () (tr:define (f x [a "a"] #:y y) y) (f 'a #:y 'b)) Univ]