From c9110ccf73da86389b9e8fba98fb612aee9e4511 Mon Sep 17 00:00:00 2001
From: AlexKnauth <alexander@knauth.org>
Date: Tue, 10 May 2016 14:05:20 -0400
Subject: [PATCH] don't make new foralls for under-constrained function
 applications

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.
---
 tapl/mlish.rkt             |  6 +-----
 tapl/tests/mlish-tests.rkt | 38 +++++++++++++++++++-------------------
 2 files changed, 20 insertions(+), 24 deletions(-)

diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
index df970df..8056881 100644
--- a/tapl/mlish.rkt
+++ b/tapl/mlish.rkt
@@ -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)
diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt
index 2c00b77..a818110 100644
--- a/tapl/tests/mlish-tests.rkt
+++ b/tapl/tests/mlish-tests.rkt
@@ -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)))