In prior work we introduced a pure type assignment system
that encompasses
a rich set of property types, including intersections, unions,
and universally and existentially quantified dependent types.
This system was shown sound with
respect to a call-by-value operational semantics with effects,
yet is inherently undecidable.
In this paper we provide a decidable formulation for this
system based on bidirectional checking, combining type
synthesis and analysis following logical principles.
The presence of unions and existential quantification
requires the additional ability to visit subterms
in evaluation position before the context in which they
occur, leading to a tridirectional
type system. While soundness with respect to the
type assignment system is immediate, completeness requires
the novel concept of contextual type annotations,
introducing a notion from the study of principal typings into
the source program.
