Gradualizing the Calculus of Inductive Constructions (CIC) involves dealing
with subtle tensions between normalization, graduality, and conservativity with
respect to CIC. Recently, GCIC has been proposed as a parametrized gradual type
theory that admits three variants, each sacrificing one of these properties.
For devising a gradual proof assistant based on CIC, normalization and
conservativity with respect to CIC are key, but the tension with graduality
needs to be addressed. Additionally, several challenges remain: (1) The
presence of two wildcard terms at any type---the error and unknown
terms---enables trivial proofs of any theorem, jeopardizing the use of a
gradual type theory in a proof assistant; (2) Supporting general indexed
inductive families, most prominently equality, is an open problem; (3)
Theoretical accounts of gradual typing and graduality so far do not support
handling type mismatches detected during reduction; (4) Precision and
graduality are external notions not amenable to reasoning within a gradual type
theory. All these issues manifest primally in CastCIC, the cast calculus used
to define GCIC. In this work, we present an extension of CastCIC called GRIP.
GRIP is a reasonably gradual type theory that addresses the issues above,
featuring internal precision and general exception handling. By adopting a
novel interpretation of the unknown term that carefully accounts for universe
levels, GRIP satisfies graduality for a large and well-defined class of terms,
in addition to being normalizing and a conservative extension of CIC. Internal
precision supports reasoning about graduality within GRIP itself, for instance
to characterize gradual exception-handling terms, and supports gradual subset
types. We develop the metatheory of GRIP using a model formalized in Coq, and
provide a prototype implementation of GRIP in Agda.