Reasoning about programs in the presence of mutation and aliasing is
notoriously difficult.
Rust has popularized lifetime-based ownership tracking in systems programming,
but its ``shared XOR mutable'' model is fundamentally at odds with
higher-level functional programming.
Reachability types offer an alternative: they enable safe sharing and
escape of mutable data by tracking which resources each expression can reach.

To track internal reachability within complex object graphs,
reachability types adopt \emph{self-references} that let
components refer to enclosing resources from inside,
just like \texttt{this} pointers in OO languages.
While natural for \emph{declaratively} typing escaping data,
self-references complicate subtyping and furthermore type inference:
variance restricts where self-references may appear, yet useful type
conversions must allow them to vary in controlled ways, which in turn imposes
constraints on inference.
As an undesirable result, prior works require programmers to insert term-level
coercions for even just \emph{avoidance}—avoiding ill-scoped names in types.

With all prior works being declarative,
we investigate \emph{algorithmic} reachability types in this work.
We introduce a refined subtyping relation that permits more flexible usages
of self-references.
We further develop a sound and decidable bidirectional typing algorithm,
implemented and verified in Lean.
The algorithm automatically avoids ill-scoped names in types,
and infers qualifiers via a lightweight unification mechanism.
As a step towards practical reachability programming,
we show that the system is capable of tracking diverse reachability patterns
without explicit coercions in complex Church-encoded datatypes.