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

don't make new foralls for under-constrained function applications

Browse Source 
Fixes the unsoundness mentioned in
https://bitbucket.org/stchang/macrotypes/issues/16/allow-under-constrained-function#comment-27692493
by disallowing under-constrained function calls entirely.
This re-opens issue #16, which will have to be solved in a sound way later.
This commit is contained in:
AlexKnauth 2016-05-10 14:05:20 -04:00
parent 1e68e32ecc
commit c9110ccf73
2 changed files with 20 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
tapl/mlish.rkt
View File

@ -756,11 +756,7 @@
#'(τ_in ...)))
#:with τ_out* (if (stx-null? #'(unsolved-X ...))
#'τ_out
(syntax-parse #'τ_out
[(~?∀ (Y ...) τ_out)
(unless (→? #'τ_out)
(raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))
#'(∀ (unsolved-X ... Y ...) τ_out)]))
(raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))
(⊢ (#%app e_fn- e_arg- ...) : τ_out*)])])]
[(_ e_fn . e_args) ; err case; e_fn is not a function
#:with [e_fn- τ_fn] (infer+erase #'e_fn)

38
tapl/tests/mlish-tests.rkt
View File

@ -365,18 +365,20 @@
(define (nn [x : X] -> (→ (× X (→ Y Y))))
(λ () (tup x (λ ([x : Y]) x))))
(define nn-1 (nn 1))
(check-type (nn-1) : (× Int (→ String String)))
(check-type (nn-1) : (× Int (→ (List Int) (List Int))))
(typecheck-fail (nn 1) #:with-msg "Could not infer instantiation of polymorphic function nn.")
(check-type (nn 1) : (→ (× Int (→ String String))))
(check-type (nn 1) : (→ (× Int (→ (List Int) (List Int)))))
(define (nn2 [x : X] -> (→ (× X (→ Y Y) (List Z))))
(λ () (tup x (λ ([x : Y]) x) Nil)))
(define nn2-1 (nn2 1))
(check-type (nn2-1) : (× Int (→ String String) (List (List Int))))
(check-type (nn2-1) : (× Int (→ (List Int) (List Int)) (List String)))
(typecheck-fail (nn2 1) #:with-msg "Could not infer instantiation of polymorphic function nn2.")
(check-type (nn2 1) : (→ (× Int (→ String String) (List (List Int)))))
(check-type (nn2 1) : (→ (× Int (→ (List Int) (List Int)) (List String))))
;; test inst order
(check-type ((inst nn2-1 String (List Int))) : (× Int (→ String String) (List (List Int))))
(check-type ((inst nn2-1 (List Int) String)) : (× Int (→ (List Int) (List Int)) (List String)))
(check-type ((inst nn2 Int String (List Int)) 1)
: (→ (× Int (→ String String) (List (List Int)))))
(check-type ((inst nn2 Int (List Int) String) 1)
: (→ (× Int (→ (List Int) (List Int)) (List String))))
(define-type (Result A B)
(Ok A)
@ -409,20 +411,20 @@
(check-type result-if-1
: (→/test (Result A1 B1) (→ (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2))
(Result A2 B2))))
(check-type (inst (result-if-1 (Ok {Int String} 1)) (List Int) (List String))
(check-type ((inst result-if-1 Int String (List Int) (List String)) (Ok 1))
: (→ (→ Int (Result (List Int) (List String)))
(→ String (Result (List Int) (List String)))
(Result (List Int) (List String))))
(check-type (inst (result-if-1 (Error {Int String} "bad")) (List Int) (List String))
(check-type ((inst result-if-1 Int String (List Int) (List String)) (Error "bad"))
: (→ (→ Int (Result (List Int) (List String)))
(→ String (Result (List Int) (List String)))
(Result (List Int) (List String))))
(check-type ((result-if-1 (Ok {Int String} 1))
(check-type (((inst result-if-1 Int String (List Int) (List String)) (Ok 1))
(λ ([a : Int]) (ok (Cons a Nil)))
(λ ([b : String]) (error (Cons b Nil))))
: (Result (List Int) (List String)))
;; same thing, but without the lambda annotations:
(check-type ((result-if-1 (Ok {Int String} 1))
(check-type (((inst result-if-1 Int String (List Int) (List String)) (Ok 1))
(λ (a) (ok (Cons a Nil)))
(λ (b) (error (Cons b Nil))))
: (Result (List Int) (List String)))
@ -438,18 +440,16 @@
: (→/test (Result A1 B1) (→ (→ A1 (Result A2 B2))
(→ (→ B1 (Result A2 B2))
(Result A2 B2)))))
(check-type (inst (result-if-2 (Ok {Int String} 1)) (List Int) (List String))
(check-type ((inst result-if-2 Int String (List Int) (List String)) (Ok 1))
: (→/test (→ Int (Result (List Int) (List String)))
(→ (→ String (Result (List Int) (List String)))
(Result (List Int) (List String)))))
(check-type ((result-if-2 (Ok {Int String} 1))
(λ ([a : Int]) (Ok {(List Int) (List String)} (Cons a Nil))))
(check-type (((inst result-if-2 Int String (List Int) (List String)) (Ok 1))
(λ (a) (Ok (Cons a Nil))))
: (→/test (→ String (Result (List Int) (List String)))
(Result (List Int) (List String))))
(check-type (((result-if-2 (Ok {Int String} 1))
; type annotations are necessary here:
(λ ([a : Int]) (Ok {(List Int) (List String)} (Cons a Nil))))
; but not here:
(check-type ((((inst result-if-2 Int String (List Int) (List String)) (Ok 1))
(λ (a) (Ok (Cons a Nil))))
(λ (b) (Error (Cons b Nil))))
: (Result (List Int) (List String)))