  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. GRIP features an impure (gradual) sort of types
inhabited by errors and unknown terms, and a pure (non-gradual) sort of strict
propositions for consistent reasoning about gradual terms. 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.
