From 18adcb5b041be12994eb65d86bde5dc1f164cca7 Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Sun, 16 Feb 2014 11:18:40 -0500 Subject: [PATCH] Improve type inference for ListDots 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`. --- .../typed-racket/infer/infer-unit.rkt | 11 +++++++++++ .../tests/typed-racket/unit-tests/typecheck-tests.rkt | 9 +++++++++ 2 files changed, 20 insertions(+) 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 b2302f0668..7b1b66f258 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 @@ -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' 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 89b9dc2d6a..86a3645cad 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 @@ -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]