diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt
index 1659f22b7e..ae4c486344 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt
@@ -98,16 +98,16 @@
     [(TypeFilter: t p i)
      `(make-TypeFilter ,(sub t) ,(sub p) ,(if (identifier? i)
                                               `(quote-syntax ,i)
-                                              i))]
+                                              `(list ,(car i) ,(cadr i))))]
     [(NotTypeFilter: t p i)
      `(make-NotTypeFilter ,(sub t) ,(sub p)
                           ,(if (identifier? i)
                                `(quote-syntax ,i)
-                               i))]
+                               `(list ,(car i) ,(cadr i))))]
     [(Path: p i)
      `(make-Path ,(sub p) ,(if (identifier? i)
                                `(quote-syntax ,i)
-                               i))]
+                               `(list ,(car i) ,(cadr i))))]
     [(? Rep? rep)
      `(,(gen-constructor (car (vector->list (struct->vector rep))))
        ,@(map sub (Rep-values rep)))]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/filter-rep.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/filter-rep.rkt
index 8d10cdfbc1..0fb4e2296e 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/filter-rep.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/filter-rep.rkt
@@ -14,8 +14,10 @@
    'FilterSet
    (λ (e) (or (FilterSet? e) (NoFilter? e)))))
 
-
-(define name-ref/c (or/c identifier? integer?))
+;; A Name-Ref is any value that represents an object.
+;; As an identifier, it represents a free variable in the environment
+;; As a list, it represents a De Bruijn indexed bound variable
+(define name-ref/c (or/c identifier? (list/c integer? integer?)))
 (define (hash-name v) (if (identifier? v) (hash-id v) (list v)))
 
 (def-filter Bot () [#:fold-rhs #:base])
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 a9ef659c63..40a3dd2882 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
@@ -11,21 +11,111 @@
          combine-props
          tc-results->values)
 
+;; abstract-results
+;;
+;; Given results from the range of a lambda, abstract any
+;; identifier objects into index (numeric) objects. This is effectively
+;; doing a kind of De Bruijn indexing for objects.
+;;
+;; When the body of a lambda is type-checked, its filters and object
+;; may refer to variables that are in scope in that body. Since these
+;; names are not in scope outside of the lambda, the type of the function
+;; will instead store their De Bruijn indices.
+;;
+;; For example, given the function
+;;
+;;   (λ (x) (number? x))
+;;
+;; the typechecker will check the body and return
+;;
+;;   Boolean ; N_x | !N_x ; ∅
+;;
+;; but the `x`s have to be converted to indices to get the type
+;;
+;;      N_(0,0) | !N_(0,0)
+;; Any -------------------> Boolean
+;;              ∅
+;;
+;; where the index (0,0) indicates the first argument of
+;; the current function
+;;
+;; Comparatively, a curried predicate like
+;;
+;;   (λ (x) (λ (y)(number? x)))
+;;
+;; gets the type
+;;
+;;             N_(1,0) | !N_(1,0)
+;; Any -> Any -------------------> Boolean
+;;                     ∅
+;;
+;; (ignoring filters on the first arrow)
+;; where the index (1,0) indicates the first argument of
+;; the enclosing lambda.
+;;
+;; The paper "Logical Types for Untyped Languages" takes a different
+;; approach where all function types carry their names, so that the first
+;; example would have the type:
+;;
+;;        N_x | !N_x
+;; x:Any ------------> Boolean
+;;            ∅
+;;
+;; See tc-subst.rkt for the functions that take an abstracted function
+;; type and substitute in a concrete object.
+;;
 (define/cond-contract (abstract-results results arg-names)
   (tc-results/c (listof identifier?) . -> . SomeValues/c)
-  (define keys (for/list ([(nm k) (in-indexed arg-names)]) k))
+  (define keys (for/list ([(nm k) (in-indexed arg-names)]) (list 0 k)))
   (match results
     [(tc-any-results:) (make-AnyValues)]
     [(tc-results: ts fs os dty dbound)
      (make-ValuesDots
       (for/list ([t (in-list ts)] [f (in-list fs)] [o (in-list os)])
-        (make-Result t (abstract-filter arg-names keys f) (abstract-object arg-names keys o)))
+        (make-Result (abstract-type arg-names keys t)
+                     (abstract-filter arg-names keys f)
+                     (abstract-object arg-names keys o)))
       dty dbound)]
     [(tc-results: ts fs os)
      (make-Values
       (for/list ([t (in-list ts)] [f (in-list fs)] [o (in-list os)])
-        (make-Result t (abstract-filter arg-names keys f) (abstract-object arg-names keys o))))]))
+        (make-Result (abstract-type arg-names keys t)
+                     (abstract-filter arg-names keys f)
+                     (abstract-object arg-names keys o))))]))
 
+;; Abstract all given id objects into index objects (keys) in
+;; the given type
+(define/cond-contract (abstract-type ids keys type)
+  (-> (listof identifier?) (listof name-ref/c) Type/c Type/c)
+  (define (at type) (abstract-type ids keys type))
+  (define (af filter) (abstract-filter ids keys filter))
+  (define (ao obj) (abstract-object ids keys obj))
+  (type-case
+   (#:Type at #:Filter af #:Object ao)
+   type
+   [#:arr
+    dom rng rest drest kws
+    (let ([at*
+           ;; when a new function type is encountered, increase
+           ;; the scope count in the keys so that names are
+           ;; substituted with the correct level of nesting
+           (λ (type)
+             (abstract-type ids (add-scope keys) type))])
+      (make-arr (map at dom)
+                (at* rng) ; only increase scope in range
+                (and rest (at rest))
+                (and drest (cons (at (car drest)) (cdr drest)))
+                (map at kws)))]))
+
+;; add-scope : Listof<name-ref/c> -> Listof<name-ref/c>
+;; Add a scope to the index object
+(define (add-scope keys)
+  (for/list ([depth+arg keys])
+    (match-define (list depth arg) depth+arg)
+    (list (+ 1 depth) arg)))
+
+;; Abstract all given id objects into index objects (keys) in
+;; the given object
 (define/cond-contract (abstract-object ids keys o)
   (-> (listof identifier?) (listof name-ref/c) Object? Object?)
   (define (lookup y)
@@ -37,6 +127,8 @@
     [(Path: p (lookup: idx)) (make-Path p idx)]
     [_ -no-obj]))
 
+;; Abstract all given id objects into index objects (keys) in
+;; the given filter set
 (define/cond-contract (abstract-filter ids keys fs)
   (-> (listof identifier?) (listof name-ref/c) FilterSet/c FilterSet/c)
   (match fs
@@ -47,8 +139,8 @@
 (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 integer?))
-       (for/first ([x (in-list xs)] [i (in-list idxs)] #:when (free-identifier=? x y)) i))
+    (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)))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
index b744c2053c..a7775dee9a 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
@@ -21,11 +21,12 @@
   (->* (Result? (listof Object?)) ((listof Type/c)) (values Type/c FilterSet? Object?))
   (match-define (Result: t fs old-obj) r)
   (for/fold ([t t] [fs fs] [old-obj old-obj])
-            ([(o k) (in-indexed (in-list objs))]
+            ([(o arg) (in-indexed (in-list objs))]
              [arg-ty (if ts (in-list ts) (in-cycle (in-value #f)))])
-    (values (subst-type t k o #t)
-            (subst-filter-set fs k o #t arg-ty)
-            (subst-object old-obj k o #t))))
+    (define key (list 0 arg))
+    (values (subst-type t key o #t)
+            (subst-filter-set fs key o #t arg-ty)
+            (subst-object old-obj key o #t))))
 
 ;; Substitution of objects into a filter set
 ;; This is essentially ψ+|ψ- [o/x] from the paper
@@ -54,10 +55,10 @@
               #:Object (lambda (f) (subst-object f k o polarity)))
               t
               [#:arr dom rng rest drest kws
-                     ;; here we have to increment the count for the domain, where the new bindings are in scope
-                     (let* ([arg-count (+ (length dom) (if rest 1 0) (if drest 1 0) (length kws))]
-                            [st* (if (integer? k)
-                                     (λ (t) (subst-type t (if (number? k) (+ arg-count k) k) o polarity))
+                     (let* ([st* (if (pair? k)
+                                     ;; Add a scope if we are substituting an index and
+                                     ;; not a free variable by name
+                                     (λ (t) (subst-type t (add-scope k) o polarity))
                                      st)])
                        (make-arr (map st dom)
                                  (st* rng)
@@ -65,6 +66,11 @@
                                  (and drest (cons (st (car drest)) (cdr drest)))
                                  (map st kws)))]))
 
+;; add-scope : name-ref/c -> name-ref/c
+;; Add a scope from an index object
+(define (add-scope key)
+  (list (+ (car key) 1) (cadr key)))
+
 ;; Substitution of objects into objects
 ;; This is o [o'/x] from the paper
 (define/cond-contract (subst-object t k o polarity)
@@ -142,9 +148,9 @@
                  #:Object for-object)
                 t
                 [#:arr dom rng rest drest kws
-                       ;; here we have to increment the count for the domain, where the new bindings are in scope
-                       (let* ([arg-count (+ (length dom) (if rest 1 0) (if drest 1 0) (length kws))]
-                              [st* (lambda (t) (index-free-in? (if (number? k) (+ arg-count k) k) t))])
+                       (let* ([st* (if (pair? k)
+                                       (lambda (t) (index-free-in? (add-scope k) t))
+                                       for-type)])
                          (for-each for-type dom)
                          (st* rng)
                          (and rest (for-type rest))
@@ -167,8 +173,9 @@
                          (open-Result r (map (lambda (i) (make-Path null i))
                                              formals)))])
            (ret ts fs os
-                (for/fold ([dty dty]) ([(o k) (in-indexed (in-list formals))])
-                  (subst-type dty k (make-Path null o) #t))
+                (for/fold ([dty dty]) ([(o idx) (in-indexed (in-list formals))])
+                  (define key (list 0 idx))
+                  (subst-type dty key (make-Path null o) #t))
                 dbound))
          (ret ts fs os dty dbound))]
     [(Values: (list (and rs (Result: ts fs os)) ...))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt
index 470625bdbe..dc69d8c6c4 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt
@@ -117,17 +117,23 @@
   (c:-> Filter/c Filter/c FilterSet?)
   (make-FilterSet + -))
 
+;; Abbreviation for filters
+;; `i` can be an integer for backwards compatibility
 (define/cond-contract (-filter t i [p null])
-     (c:->* (Type/c name-ref/c) ((c:listof PathElem?)) Filter/c)
-     (if (or (type-equal? Univ t) (and (identifier? i) (is-var-mutated? i)))
-         -top
-         (make-TypeFilter t p i)))
+  (c:->* (Type/c (c:or/c integer? name-ref/c)) ((c:listof PathElem?)) Filter/c)
+  (define i* (if (integer? i) (list 0 i) i))
+  (if (or (type-equal? Univ t) (and (identifier? i) (is-var-mutated? i)))
+      -top
+      (make-TypeFilter t p i*)))
 
+;; Abbreviation for not filters
+;; `i` can be an integer for backwards compatibility
 (define/cond-contract (-not-filter t i [p null])
-     (c:->* (Type/c name-ref/c) ((c:listof PathElem?)) Filter/c)
-     (if (or (type-equal? -Bottom t) (and (identifier? i) (is-var-mutated? i)))
-         -top
-         (make-NotTypeFilter t p i)))
+  (c:->* (Type/c (c:or/c integer? name-ref/c)) ((c:listof PathElem?)) Filter/c)
+  (define i* (if (integer? i) (list 0 i) i))
+  (if (or (type-equal? -Bottom t) (and (identifier? i) (is-var-mutated? i)))
+      -top
+      (make-NotTypeFilter t p i*)))
 
 (define (-filter-at t o)
   (match o
@@ -199,9 +205,9 @@
 
 (define (->acc dom rng path)
   (make-Function (list (make-arr* dom rng
-                                  #:filters (-FS (-not-filter (-val #f) 0 path)
-                                                 (-filter (-val #f) 0 path))
-                                  #:object (make-Path path 0)))))
+                                  #:filters (-FS (-not-filter (-val #f) (list 0 0) path)
+                                                 (-filter (-val #f) (list 0 0) path))
+                                  #:object (make-Path path (list 0 0))))))
 
 (define (cl->* . args)
   (define (funty-arities f)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt
index 055b9dbb2f..35f4b60f3b 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt
@@ -29,7 +29,7 @@
 
 
 (define (name-ref=? a b)
-  (or (eq? a b)
+  (or (equal? a b)
       (and (identifier? a)
            (identifier? b)
            (free-identifier=? a b))))
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 6aa80d44fd..61acfdefc2 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
@@ -838,9 +838,9 @@
         ;; instantiating non-dotted terms
         [tc-e/t (inst (plambda: (a) ([x : a]) x) Integer)
                 (make-Function (list (make-arr* (list -Integer) -Integer
-                                                #:filters (-FS (-not-filter (-val #f) 0)
-                                                               (-filter (-val #f) 0))
-                                                #:object (make-Path null 0))))]
+                                                #:filters (-FS (-not-filter (-val #f) (list 0 0))
+                                                               (-filter (-val #f) (list 0 0)))
+                                                #:object (make-Path null (list 0 0)))))]
         [tc-e/t (inst (plambda: (a) [x : a *] (apply list x)) Integer)
                 ((list) -Integer . ->* . (-lst -Integer))]
 
@@ -1765,6 +1765,21 @@
                   (Any -> Boolean : #:+ (Integer @ x) #:- (! Integer @ x))))
            (if (f 'dummy) (add1 x) 2))
          (t:-> Univ -Integer : (-FS -top (-filter -Integer 0)))]
+
+        ;; This test ensures that curried predicates have
+        ;; the correct filters so that they can be used for
+        ;; occurrence typing.
+        [tc-e
+         (let ()
+           (define f (λ (x) (λ (y) (number? x))))
+           (: b (U Number String))
+           (define b 5)
+           (define g (f b))
+           ;; this doesn't type-check unless OT is working
+           (if (g "foo") (add1 b) 3)
+           (void))
+         ;; type doesn't really matter, just make sure it typechecks
+         -Void]
         )
   (test-suite
    "tc-literal tests"