www

commit 95d960267a79ce2544a930721150fb623c4764eb
parent c9110ccf73da86389b9e8fba98fb612aee9e4511
Author: AlexKnauth <alexander@knauth.org>
Date:   Tue, 10 May 2016 14:35:05 -0400

test the example that would have been unsound

Diffstat:
A
tapl/tests/mlish/value-restriction-example.mlish
 | 
25
+++++++++++++++++++++++++
M
tapl/tests/run-mlish-tests1.rkt
 | 
1
+

2 files changed, 26 insertions(+), 0 deletions(-)
diff --git a/tapl/tests/mlish/value-restriction-example.mlish b/tapl/tests/mlish/value-restriction-example.mlish
@@ -0,0 +1,25 @@
+#lang s-exp "../../mlish.rkt"
+(require "../rackunit-typechecking.rkt")
+
+(define-type (Option X)
+  None
+  (Some X))
+
+(define (make-f → (→ A A))
+  (let ([r (ref (None {A}))])
+    (λ (x)
+      (let ([y (deref r)])
+        (begin
+          (:= r (Some x))
+          (match y with
+            [None -> x]
+            [Some y -> y]))))))
+;; This has to fail, because if could succeed with the type (→ A A),
+;; then it could cause unsoundness.
+(typecheck-fail (make-f) #:with-msg "Could not infer instantiation of polymorphic function make-f.")
+; ;; If f were defined as the result of (make-f), then it would result
+; ;; in unsoundess if these two expressions were also accepted:
+; (f 13)
+; ;; Because this would typecheck as a String even though it returns 13, an Int:
+; (f "foo")
+
diff --git a/tapl/tests/run-mlish-tests1.rkt b/tapl/tests/run-mlish-tests1.rkt
@@ -5,6 +5,7 @@
 (require "mlish/match2.mlish")
 (require "mlish/polyrecur.mlish")
 (require "mlish/loop.mlish")
+(require "mlish/value-restriction-example.mlish")
 
 ;; (require "mlish/trees.mlish")
 ;; (require "mlish/chameneos.mlish")