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

allow some under-constrained function applications

Browse Source 
in cases where the unsolved type variables only appear in covariant
positions.
This commit is contained in:
AlexKnauth 2016-05-10 19:03:27 -04:00
parent 4af0f4e2b4
commit 7a3c096a83
2 changed files with 18 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
tapl/mlish.rkt
View File

@ -916,7 +916,14 @@
#'(τ_in ...)))
#:with τ_out* (if (stx-null? #'(unsolved-X ...))
#'τ_out
(raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))
(syntax-parse #'τ_out
[(~?∀ (Y ...) τ_out)
(unless (→? #'τ_out)
(raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))
(for ([X (in-list (syntax->list #'(unsolved-X ...)))])
(unless (covariant-X? X #'τ_out)
(raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)))
#'(∀ (unsolved-X ... Y ...) τ_out)]))
(⊢ (#%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)

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

@ -397,6 +397,16 @@
(check-type ((inst nn2 Int (List Int) String) 1)
: (→ (× Int (→ (List Int) (List Int)) (List String))))
(define (nn3 [x : X] -> (→ (× X (Option Y) (Option Z))))
(λ () (tup x None None)))
(check-type (nn3 1) : (→/test (× Int (Option Y) (Option Z))))
(check-type (nn3 1) : (→ (× Int (Option String) (Option (List Int)))))
(check-type ((nn3 1)) : (× Int (Option String) (Option (List Int))))
(check-type ((nn3 1)) : (× Int (Option (List Int)) (Option String)))
;; test inst order
(check-type ((inst (nn3 1) String (List Int))) : (× Int (Option String) (Option (List Int))))
(check-type ((inst (nn3 1) (List Int) String)) : (× Int (Option (List Int)) (Option String)))
(define-type (Result A B)
(Ok A)
(Error B))