From b87ebbfe8f961a1d78827a5c5f0633630566befc Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Wed, 2 Apr 2014 07:26:14 -0500
Subject: [PATCH] adjust let poly bug #4 so that the check procedure catches
 errors and treats them as failing to satisfy the property
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This bug disables the occurs check and, thanks to the now
tighter contracts on the uh function, this can cause it to
signal an error. Here's the example:

  (term (unify (x → (list int)) ((list x) → x)))

found by in-order enumeration (so naturally it had ||
variables in it, not 'x's originally)

This leads to this trace in the uh function:

  (uh ((x → (list int)) ((list x) → x) ·) ·)
  (uh (x (list x) ((list int) x ·))       ·)
  (uh ((list int) (list x) ·)             (x (list x) ·))
  (uh (int x ·)                           (x (list x) ·))
  (uh (x int ·)                           (x (list x) ·))
  (uh ·                                   (x int (int (list int) ·)))

whereby the third step sets up a problem (that's where the
occurs check should have aborted the program) but instead, a
few steps later when we get a substitution for 'x', it
causes the second argument to not have the form of
variables-for-types substitution.

I don't think this can happen when the occurs check is in place
because the variable elimination step makes sure that we don't
set ourselves up to change the domain of anything in the second
argument to 'uh' (except possibly when the occurs check fails,
of course).

Here's an example that shows this:

 (unify (q → q) (y → int)))
 (uh ((q → q) (y → int) ·) ·)
 (uh (q y (q int ·))       ·)
 (uh (y int ·)             (q y ·))
 (uh ·                     (y int (q int ·)))

In the second to last step we don't have (q int ·), we have
(y int ·) because the variable elimination step changes the
q to a y.
---
 .../redex/examples/benchmark/let-poly/4.diff  | 28 ++++++++++++++++++-
 .../benchmark/let-poly/let-poly-4.rkt         | 25 +++++++++--------
 2 files changed, 40 insertions(+), 13 deletions(-)

diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff
index 61968e952e..575ee48a6f 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff
@@ -8,7 +8,33 @@
 <   [(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
 ---
 >   [(uh (x τ G) Gx) ⊥ (where #t (in-vars? x τ))]
-552a555,557
+541,552c543,558
+<       (let ([t-type (type-check M)])
+<         (implies
+<          t-type
+<          (let loop ([Σ+M `(· ,M)] [n 100])
+<            (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
+<            (and (consistent-with? t-type new-type)
+<                 (or (v? (list-ref Σ+M 1))
+<                     (let ([red-res (apply-reduction-relation red Σ+M)])
+<                       (and (= (length red-res) 1)
+<                            (let ([red-t (car red-res)])
+<                              (or (equal? red-t "error")
+<                                  (zero? n) (loop red-t (- n 1)))))))))))))
+---
+>       (with-handlers ([exn:fail? (λ (x) #f)])
+>         (let ([t-type (type-check M)])
+>           (implies
+>            t-type
+>            (let loop ([Σ+M `(· ,M)] [n 100])
+>              (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
+>              (and (consistent-with? t-type new-type)
+>                   (or (v? (list-ref Σ+M 1))
+>                       (let ([red-res (apply-reduction-relation red Σ+M)])
+>                         (and (= (length red-res) 1)
+>                              (let ([red-t (car red-res)])
+>                                (or (equal? red-t "error")
+>                                    (zero? n) (loop red-t (- n 1))))))))))))))
 > 
 > (define small-counter-example (term ((λ x (x x)) hd)))
 > (test-equal (check small-counter-example) #f)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt
index df0045c7e2..fbc6b945d1 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt
@@ -540,18 +540,19 @@ reachable from the given term.
 
 (define (check M)
   (or (not M)
-      (let ([t-type (type-check M)])
-        (implies
-         t-type
-         (let loop ([Σ+M `(· ,M)] [n 100])
-           (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
-           (and (consistent-with? t-type new-type)
-                (or (v? (list-ref Σ+M 1))
-                    (let ([red-res (apply-reduction-relation red Σ+M)])
-                      (and (= (length red-res) 1)
-                           (let ([red-t (car red-res)])
-                             (or (equal? red-t "error")
-                                 (zero? n) (loop red-t (- n 1)))))))))))))
+      (with-handlers ([exn:fail? (λ (x) #f)])
+        (let ([t-type (type-check M)])
+          (implies
+           t-type
+           (let loop ([Σ+M `(· ,M)] [n 100])
+             (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
+             (and (consistent-with? t-type new-type)
+                  (or (v? (list-ref Σ+M 1))
+                      (let ([red-res (apply-reduction-relation red Σ+M)])
+                        (and (= (length red-res) 1)
+                             (let ([red-t (car red-res)])
+                               (or (equal? red-t "error")
+                                   (zero? n) (loop red-t (- n 1))))))))))))))
 
 (define small-counter-example (term ((λ x (x x)) hd)))
 (test-equal (check small-counter-example) #f)