www

commit 57885d86459b26a0d988fa303b32f5a024a1fc08
parent 6e2f9a4a167f7a4f71f441a194aef557f759404c
Author: AlexKnauth <alexander@knauth.org>
Date:   Mon, 27 Jun 2016 10:23:37 -0400

infer instantiations for function positions

Diffstat:
M
turnstile/examples/infer.rkt
 | 
4
++--
M
turnstile/examples/tests/tlb-infer-tests.rkt
 | 
2
++

2 files changed, 4 insertions(+), 2 deletions(-)
diff --git a/turnstile/examples/infer.rkt b/turnstile/examples/infer.rkt
@@ -162,13 +162,13 @@
    [#:with [A ...] (generate-temporaries #'[e_arg ...])]
    [#:with B (generate-temporary 'result)]
    [⊢ [[e_fn ≫ e_fn-] ⇒ : τ_fn*]]
-   [#:with (~?Some [V1 ...] τ_fn (~Cs [τ_3 τ_4] ...))
+   [#:with (~?Some [V1 ...] (~?∀ (V2 ...) τ_fn) (~Cs [τ_3 τ_4] ...))
     (syntax-local-introduce #'τ_fn*)]
    [#:with τ_fn-expected (tycons #'→ #'[A ... B])]
    [⊢ [[e_arg ≫ e_arg-] ⇒ : τ_arg*] ...]
    [#:with [(~?Some [V3 ...] τ_arg (~Cs [τ_5 τ_6] ...)) ...]
     (syntax-local-introduce #'[τ_arg* ...])]
-   [#:with τ_out (some/inst/generalize #'[A ... B V1 ... V3 ... ...]
+   [#:with τ_out (some/inst/generalize #'[A ... B V1 ... V2 ... V3 ... ...]
                                        #'B
                                        #'([τ_fn-expected τ_fn]
                                           [τ_3 τ_4] ...
diff --git a/turnstile/examples/tests/tlb-infer-tests.rkt b/turnstile/examples/tests/tlb-infer-tests.rkt
@@ -3,6 +3,8 @@
 
 (check-type (λ (x) 5) : (∀ (X) (→ X Int)))
 (check-type (λ (x) x) : (∀ (X) (→ X X)))
+(check-type ((λ (x) x) 5) : Int)
+(check-type ((λ (x) x) (λ (y) y)) : (∀ (Y) (→ Y Y)))
 
 (check-type (λ (x) (λ (y) 6)) : (∀ (X) (→ X (∀ (Y) (→ Y Int)))))
 (check-type (λ (x) (λ (y) x)) : (∀ (X) (→ X (∀ (Y) (→ Y X)))))