From 7a3c096a83ac26e5970c097588abc1d94d8dbaa0 Mon Sep 17 00:00:00 2001
From: AlexKnauth <alexander@knauth.org>
Date: Tue, 10 May 2016 19:03:27 -0400
Subject: [PATCH] allow some under-constrained function applications

in cases where the unsolved type variables only appear in covariant
positions.
---
 tapl/mlish.rkt             |  9 ++++++++-
 tapl/tests/mlish-tests.rkt | 10 ++++++++++
 2 files changed, 18 insertions(+), 1 deletion(-)

diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
index 751f829..e5584eb 100644
--- a/tapl/mlish.rkt
+++ b/tapl/mlish.rkt
@@ -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)
diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt
index 0223f61..521975a 100644
--- a/tapl/tests/mlish-tests.rkt
+++ b/tapl/tests/mlish-tests.rkt
@@ -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))