From 08e8a6eeb1b6080747f2109a3f569ba9d8749348 Mon Sep 17 00:00:00 2001
From: Asumu Takikawa <asumu@ccs.neu.edu>
Date: Fri, 14 Feb 2014 23:24:46 -0500
Subject: [PATCH] Fix TR regression and use abstraction recipe

A function like (lambda (x) (lambda (y) y)) would cause TR
to fail in an internal metafunction. The fault was triggered
when the object y is abstracted to (0 0) and then the outer
lambda tries to abstract (0 0) and fails.

The problem was triggered by the new path index changes in
v6.0 because TR did not previously try to abstract objects
that occurs in the target type (now necessary for scope
lifting of path indices), which may contain non-identifier
objects.

This error didn't occur in another nearly identical (except
for one crucial identifier? check) code path, so this commit
also eliminates the duplication by abstracting.

original commit: bf47523ac92f2d3b32e6c97aa83d9d256b449a6f
---
 .../typecheck/tc-metafunctions.rkt            | 35 ++++++++++++-------
 .../unit-tests/typecheck-tests.rkt            | 13 ++++++-
 2 files changed, 35 insertions(+), 13 deletions(-)

diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
index 40a3dd28..95bce261 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
@@ -118,11 +118,7 @@
 ;; the given object
 (define/cond-contract (abstract-object ids keys o)
   (-> (listof identifier?) (listof name-ref/c) Object? Object?)
-  (define (lookup y)
-    (for/first ([x (in-list ids)] [i (in-list keys)] #:when (free-identifier=? x y)) i))
-  (define-match-expander lookup:
-    (syntax-rules ()
-      [(_ i) (app lookup (? values i))]))
+  (define-lookup: lookup: ids keys)
   (match o
     [(Path: p (lookup: idx)) (make-Path p idx)]
     [_ -no-obj]))
@@ -138,15 +134,9 @@
 
 (define/cond-contract (abo xs idxs f)
   ((listof identifier?) (listof name-ref/c) Filter/c . -> . Filter/c)
-  (define/cond-contract (lookup y)
-    (identifier? . -> . (or/c #f (list/c integer? integer?)))
-    (for/first ([x (in-list xs)] [i (in-list idxs)] #:when (free-identifier=? x y)) i))
-  (define-match-expander lookup:
-    (syntax-rules ()
-      [(_ i) (or (? identifier? (app lookup (? values i)))
-                 i)]))
   (define (rec f) (abo xs idxs f))
   (define (sb-t t) t)
+  (define-lookup: lookup: xs idxs)
   (filter-case (#:Type sb-t #:Filter rec) f
                [#:TypeFilter
                 t p (lookup: idx)
@@ -155,6 +145,27 @@
                 t p (lookup: idx)
                 (-not-filter t idx p)]))
 
+;; Look up the identifier in a mapping of a list of identifiers
+;; to a list of path indices
+(define/cond-contract (lookup-index target ids keys)
+  (-> identifier? (listof identifier?) (listof (list/c integer? integer?))
+      (or/c #f (list/c integer? integer?)))
+  (for/first ([id (in-list ids)] [index (in-list keys)]
+              #:when (free-identifier=? id target))
+    index))
+
+;; Generates a match expander to make `lookup-index` convenient
+(define-syntax-rule (define-lookup: lookup: ids keys)
+  (define-match-expander lookup:
+    (syntax-rules ()
+      [(_ i)
+       (or ;; No need to look up if it's not an identifier,
+           ;; since that means it was already abstracted
+           ;; into an index.
+           (? identifier? (app (λ (id) (lookup-index id ids keys))
+                               (? values i)))
+           i)])))
+
 (define (merge-filter-sets fs)
   (match fs
     [(list (FilterSet: f+ f-) ...)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
index a69b3c35..89b9dc2d 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
@@ -857,7 +857,8 @@
               (-polydots (z x y) (t:-> (cl->*
                                         ((t:-> x z) (-pair x (-lst x)) . t:-> . (-pair z (-lst z)))
                                         ((list ((list x) (y y) . ->... . z) (-lst x)) ((-lst y) y) . ->... . (-lst z)))
-                                       : (-FS (-not-filter (-val #f) #'map) (-filter (-val #f) #'map))))]
+                                       : (-FS (-not-filter (-val #f) #'map) (-filter (-val #f) #'map))
+                                       : (make-Path null #'map)))]
 
         ;; error tests
         [tc-err (+ 3 #f)]
@@ -1779,6 +1780,16 @@
          ;; type doesn't really matter, just make sure it typechecks
          -Void]
 
+        ;; Tests the absence of a regression with curried functions
+        ;; (should not trigger an error with free-identifier=?)
+        [tc-e (lambda (x) (lambda (y) y))
+              #:ret
+              (ret (t:-> Univ (t:-> Univ Univ : (-FS (-not-filter (-val #f) (list 0 0))
+                                                     (-filter (-val #f) (list 0 0)))
+                                              : (make-Path null (list 0 0)))
+                              : (-FS -top -bot))
+                   (-FS -top -bot))]
+
        ;; The following ensures that the correct filter can be
        ;; written by the user
        [tc-e