  Graded type theories are an emerging paradigm for augmenting the reasoning
power of types with parameterizable, fine-grained analyses of program
properties. There have been many such theories in recent years which equip a
type theory with quantitative dataflow tracking, usually via a semiring-like
structure which provides analysis on variables (often called `quantitative' or
`coeffect' theories). We present Graded Modal Dependent Type Theory (GrTT for
short), which equips a dependent type theory with a general, parameterizable
analysis of the flow of data, both in and between computational terms and
types. In this theory, it is possible to study, restrict, and reason about data
use in programs and types, enabling, for example, parametric quantifiers and
linearity to be captured in a dependent setting. We propose GrTT, study its
metatheory, and explore various case studies of its use in reasoning about
programs and studying other type theories. We have implemented the theory and
highlight the interesting details, including showing an application of grading
to optimising the type checking procedure itself.
