From 95d960267a79ce2544a930721150fb623c4764eb Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Tue, 10 May 2016 14:35:05 -0400 Subject: [PATCH] test the example that would have been unsound --- .../mlish/value-restriction-example.mlish | 25 +++++++++++++++++++ tapl/tests/run-mlish-tests1.rkt | 1 + 2 files changed, 26 insertions(+) create mode 100644 tapl/tests/mlish/value-restriction-example.mlish diff --git a/tapl/tests/mlish/value-restriction-example.mlish b/tapl/tests/mlish/value-restriction-example.mlish new file mode 100644 index 0000000..dd00d5c --- /dev/null +++ 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 index e59e76f..250d7d1 100644 --- 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")