Gradualizing the Calculus of Inductive Constructions

Meven Lennon-Bertrand

Gallinette Project-Team, Inria

Kenji Maillard

Gallinette Project-Team, Inria

Nicolas Tabareau

Gallinette Project-Team, Inria

Éric Tanter

PLEIAD Lab, Computer Science Department (DCC), University of Chile

This work is partially funded by ANID FONDECYT Regular
Project 1190058, and Inria Équipe Associée GECO.
[width=, sharp corners=all, colback=white!95!black]
To appear in ACM Transactions in Programming Languages and Systems, 2022,

We investigate gradual variations on the Calculus of Inductive Construction (CIC) for swifter prototyping with imprecise types and terms. We observe, with a no-go theorem, a crucial tradeoff between graduality and the key properties of normalization and closure of universes under dependent product that CIC enjoys. Beyond this Fire Triangle of Graduality, we explore the gradualization of CIC with three different compromises, each relaxing one edge of the Fire Triangle. We develop a parametrized presentation of Gradual CIC (GCIC) that encompasses all three variations, and develop their metatheory. We first present a bidirectional elaboration of GCIC to a dependently-typed cast calculus, CastCIC, which elucidates the interrelation between typing, conversion, and the gradual guarantees. We use a syntactic model of CastCIC to inform the design of a safe, confluent reduction, and establish, when applicable, normalization. We study the static and dynamic gradual guarantees as well as the stronger notion of graduality with embedding-projection pairs formulated by New and Ahmed, using appropriate semantic model constructions. This work informs and paves the way towards the development of malleable proof assistants and dependently-typed programming languages.

§ INTRODUCTION

Gradual typing arose as an approach to selectively and soundly relax static type
checking by endowing programmers with imprecise
types <cit.>. Optimistically well-typed
programs are safeguarded by runtime checks that detect violations of
statically-expressed assumptions. A gradual version of the simply-typed lambda
calculus () enjoys such expressiveness that it can embed the untyped lambda
calculus. This means that gradually-typed languages tend to accommodate at least
two kinds of effects, non-termination and runtime errors.
The smoothness of the static-to-dynamic checking spectrum afforded by gradual languages
is usually captured by (static and dynamic) gradual
which stipulate that typing and reduction are monotone with respect
to precision <cit.>.

Originally formulated in terms of simple types, the extension of gradual typing
to a wide variety of typing disciplines has been an extremely active topic of
research, both in theory and in practice. As part of this quest towards more
sophisticated type disciplines, gradual typing was bound to meet with full-blown
dependent types. This encounter saw various premises in a variety of approaches
to integrate (some form of) dynamic checking with (some form of) dependent
types <cit.>.
Naturally, the highly-expressive setting of dependent types, in which terms and
types are not distinct and computation happens as part of typing, raises a lot
of subtle challenges for gradualization. In the most elaborate effort to date,
<cit.> present a gradual dependently-typed programming
language, GDTL, which can be seen as an effort to gradualize a two-phase
programming language such as  <cit.>. A key idea of GDTL is to adopt an
approximate form of computation at compile-time, called approximate
normalization, which ensures termination and totality of typing, while adopting
a standard gradual reduction semantics with errors and non-termination at runtime.
The metatheory of GDTL however still needs to be extended to account for inductive types.

This paper addresses the open challenge of gradualizing a full-blown dependent type theory, namely the Calculus of Inductive Constructions (hereafter, ) <cit.>, identifying and addressing the corresponding metatheoretic challenges. In doing so, we build upon several threads of prior work in the type theory and gradual typing literature: syntactic models of type theories to justify extensions of  <cit.>, in particular the exceptional type theory of <cit.>, an effective re-characterization of the dynamic gradual guarantee as graduality with embedding-projection pairs <cit.>, as well as the work on GDTL <cit.>.

Motivation. We believe that studying the gradualization of a full-blown dependent type theory like is in and of itself an important scientific endeavor, which is very likely to inform the gradual typing research community in its drive towards supporting ever more challenging typing disciplines. In this light, the aim of this paper is not to put forth a unique design or solution, but to explore the space of possibilities. Nor is this paper about a concrete implementation of gradual and an evaluation of its applicability; these are challenging perspectives of their own, which first require the theoretical landscape to be unveiled.

This being said, as <cit.>, we can highlight a number of practical motivating scenarios for gradualizing , anticipating what could be achieved in a hypothetical gradual version of , for instance.

[Smoother development with indexed types]

, which underpins languages and proof assistants such as , Agda and , among others, is a very powerful system to program in, but at the same time extremely demanding. Mixing programs and their specifications is attractive but challenging.

Consider the classical example of length-indexed lists, of type vec A n as defined in :[We use the notation $\square_i$ for the predicative universe of types , and omit the universe level $i$ when not required.]

Inductive vec (A : Type) : nat -> Type :=
| nil  : vec A 0
| cons : A -> forall n : nat, vec A n -> vec A (S n).

Indexing the inductive type by its length allows us to define a total head function, which can only be applied to non-empty lists:

head : forall A n, vec A (S n) -> A

Developing functions over such structures can be tricky. For instance, what type should the filter function be given?

filter : forall A n (f : A -> bool), vec A n -> vec A

The size of the resulting list depends on how many elements in the list actually match the given predicate f!
Dealing with this level of intricate specification can (and does) scare programmers away from mixing programs and specifications. The truth is that many libraries, such as MathComp <cit.>, give up on mixing programs and specifications even for simple structures such as these, which are instead dealt with as ML-like lists with extrinsically-established properties. This
tells a lot about the current intricacies of dependently-typed programming.

Instead of avoiding the obstacle altogether, gradual dependent types provide a uniform and flexible mechanism to a tailored adoption of dependencies. For instance, one could give filter the following gradual type, which makes use of the unknown term $\?$ in an index position:

filter : forall A n (f : A -> bool), vec A n -> vec A ?

This imprecise type means that uses of filter will be optimistically accepted by the typechecker, although subject to associated checks during reduction. For instance:

head nat ? (filter nat 4 even [ 0 ; 1 ; 2 ; 3 ])

typechecks, and is successfully convertible to $0$, while:

head nat ? (filter nat 2 even [ 1 ; 3 ])

typechecks but fails upon reduction, when discovering that the assumption that the argument to head is non-empty is
in fact incorrect.

[Defining general recursive functions]

Another challenge of working in is to convince the type checker that recursive definitions are well founded. This can either require tight syntactic restrictions, or sophisticated arguments involving accessibility predicates. At any given stage of a development, one might not be in a position to follow any of these. In such cases, a workaround is to adopt the “fuel pattern”,  parametrizing a function with a clearly syntactically decreasing argument in order to please the typechecker, and to use an arbitrary initial fuel value. In practice, one sometimes requires a simpler way to unplug termination checking, and for that purpose, many proof assistants support external commands or parameters to deactivate termination checking.[such as  in , or  in .]

Because the use of the unknown type allows the definition of fix-point combinators <cit.>, one can use this added expressiveness to bypass termination checking locally.
This just means that the external facilities provided by specific proof assistant implementations now become internalized in the language.

[Large elimination, gradually]

One of the argued benefit of dynamically-typed languages, which is accommodated by gradual typing, is the ability to define functions that can return values of different types depending on their inputs, such as:

def foo(n)(m)  if (n > m) then m + 1 else m > 0

In a gradually-typed language, one can give this function the type $\?$, or even $\nat -> \nat -> \?$ in order to enforce proper argument types, and remain flexible in the treatment of the returned value.
Of course, one knows very well that in a dependently-typed language, with large elimination, we can simply give  the dependent type:

foo : forall (n m : nat), if (n > m) then nat else bool

Lifting the term-level comparison n > m to the type level is extremely expressive, but hard to work with as well, both for the implementer of the function and its clients.

In a gradual dependently-typed setting, one can explore the whole spectrum of type-level precision for such a function, starting from the least precise to the most precise, for instance:

foo : ?
foo : nat -> nat -> ?
foo : nat -> nat -> if ? then nat else ?
foo : forall (n m : nat), if (n > m) then nat else ?
foo : forall (n m : nat), if (n > m) then nat else bool

At each stage from top to bottom, there is less flexibility (but more guarantees!) for both the implementer of foo and its clients. The gradual guarantee ensures that if the function is actually faithful to the most precise type
then giving it any of the less precise types above does not introduce any new failure <cit.>.

[Gradually refining specifications]

Let us come back to the filter function from <ref>. Its fully-precise type requires appealing to a type-level function that counts the number of elements in the list that satisfy the predicate (notice the dependency to the input vector v):

filter : forall A n (f : A -> bool) (v : vec A n), vec A (count_if A n f v)

Anticipating the need for this function, a gradual specification could adopt the above signature for
filter but leave count_if unspecified:

Definition count_if A n (f : A -> bool) (v: vec A n) : nat := ?.

This situation does not affect the behavior of the program compared to leaving the return type index unknown. More interestingly, one could immediately define the base case, which trivially specifies that there are no matching elements in an empty vector:

Definition count_if A n (f : A -> bool) (v : vec A n) : nat :=
match v with
| nil _ _ => 0
| cons _ _ _ => ?

This slight increment in precision provides a little more static checking, for instance:

head nat ? (filter nat 4 even [])

does not typecheck, instead of failing during reduction.

Again, the gradual guarantee ensures that such incremental refinements in precision towards the proper fully-precise version do not introduce spurious errors.
Note that this is in stark contrast with the use of axioms (which will be discussed in more depth in <ref>). Indeed, replacing correct code with an axiom can simply break typing! For instance, with the following definitions:

Axiom to_be_done : nat.
Definition count_if A n (f : A -> bool) (v: vec A n) : nat := to_be_done.

the definition of filter does not typecheck anymore, as the axiom at the type-level is not convertible to any given value.

Note: Gradual programs or proofs?

When adapting the ideas of gradual typing to a dependent type theory, one might
expect to deal with programs rather than proofs.
This observation is however misleading: from the point of view of the Curry-Howard correspondence, proofs and programs are intrinsically related, so that gradualizing the latter begs for a gradualization of the former. The examples above illustrate mixed programs and specifications, which naturally also appeal to proofs: dealing with indexed types typically requires exhibiting equality proofs to rewrite terms.
Moreover, there are settings in which one must consider computationally-relevant proofs, such as constructive algebra and analysis, homotopy type theory, etc. In such settings, using axioms to bypass unwanted proofs breaks reduction, and because typing requires reduction, the use of axioms can simply prevent typing, as illustrated in <ref>.

This article reports on the following contributions:

* We analyze, from a type theoretic point of view, the fundamental tradeoffs
involved in gradualizing a dependent type theory such as (<ref>), and establish a no-go theorem,
the Fire Triangle of Graduality, which does apply to . In essence, this result tells us that a gradual type theory[Note that we sometimes use “dependent type theory” in order to differentiate from the Gradual Type Theory of
<cit.>, which is simply typed. But by default, in
this article, the expression "type theory" is used to refer to a
type theory with full dependent types, such as .]  cannot satisfy at the same time normalization, graduality, and conservativity with respect to . We explain each property and carefully analyze what it means in the type theoretic setting.

* We present an approach to gradualizing (<ref>),
parametrized by two knobs for controlling universe constraints on the
dependent function space, resulting in
three meaningful variants of Gradual (), that reflect distinct resolutions of the
Fire Triangle of Graduality. Each variant sacrifices one key property.

* We give a bidirectional and mutually-recursive elaboration of
to a dependently-typed cast calculus (<ref>). This elaboration is based on a
bidirectional presentation of , which has been recently studied
in details by <cit.>, and of which we give a comprehensive
summary in <ref>.
Like , is parametrized, and encompasses three variants. We develop the metatheory of , and elaboration. In particular, we prove type safety for all variants, as well as the gradual guarantees and normalization, each for two of the three variants.

* To further develop the metatheory of , we appeal to various
models (<ref>). First, to prove strong normalization of two variants, we provide a syntactic  model of with a translation to extended with induction-recursion <cit.>. Second, to prove the stronger notion of graduality with embedding-projection pairs <cit.> for a normalizing variant, we provide a model of that captures the notion of monotonicity with
respect to precision. Finally, we present an extension of Scott's model
based on $\omega$-complete partial orders <cit.> to prove
graduality for the variant with divergence.

* We describe how to handle indexed inductive types in , either directly or via different encodings, under some constraints on indices (<ref>).

We then elucidate the current limitations of this work regarding three important features of —impredicativity, $\eta$-equality and propositional equality (<ref>).
We finally discuss related work (<ref>) and conclude (<ref>). Some detailed proofs are omitted from the main text and can be found in appendix.

§ FUNDAMENTAL TRADEOFFS IN GRADUAL DEPENDENT TYPE THEORY

Before exposing a specific approach to gradualizing , we present a general analysis of the main properties at stake and tensions that arise when gradualizing a dependent type theory.

We start by recalling two cornerstones of type theory, namely progress and normalization, and allude to the need to reconsider them carefully in a gradual setting (<ref>). We explain why the obvious approach based on axioms is unsatisfying (<ref>), as well as why simply using a type theory with exceptions <cit.> is not enough either (<ref>). We then turn to the gradual approach, recalling its essential properties in the simply-typed setting (<ref>), and revisiting them in the context of a dependent type theory (<ref>). This finally leads us to establish a fundamental impossibility in the gradualization of , which means that at least one of the desired properties has to be sacrificed (<ref>).

§.§ Safety and Normalization, Endangered

As a well-behaved typed programming language, enjoys
(type) Safety (), meaning that well-typed closed terms cannot get
stuck, the normal forms of closed terms of a given type are
exactly the canonical forms of that type.

In , a closed canonical form is a term whose typing derivation ends
with an introduction rule, a $\lambda$-abstraction for a function
type, and a constructor for an inductive type.

For instance, any closed term of type bool is convertible (and
reduces) to either true or false.
Note that an open term can reduce to an open canonical form called a neutral term,
such as not x.

As a logically consistent type theory, enjoys (strong) Normalization
(), meaning that any term is convertible to its (unique) normal form.
together with imply canonicity: any closed term of a given
type must reduce to a canonical form of that type.

When applied to the empty type False, canonicity ensures logical consistency:
because there is no canonical form for False, there is no
closed proof of False.

Note that also has an important consequence in . Indeed, in
this system, conversion—which coarsely means syntactic equality
up-to reduction—is used in the type-checking algorithm.

ensures that one can devise a sound and complete decision
procedure (a reduction strategy) in order to decide conversion, and hence, typing.

In the gradual setting, the two cornerstones and must be considered with care.

First, any closed term can be ascribed the unknown type ?
first and then any other type: for instance, 0::?::bool is a
well-typed closed term of type bool.
[We write $a :: A$ for a type ascription, which is syntactic sugar
for $(\lambda x:A.x)\;a$ <cit.>; in
other systems, it can be taken as a primitive notion <cit.>.]
However, such a term
cannot possibly reduce to either true or false, so some
concessions must be made with respect to safety—at least, the notion
of canonical forms must be extended.

Second, is endangered. The quintessential example of non-termination in the untyped lambda calculus is the
term  where . In the simply-typed lambda calculus (hereafter ), as in ,
self-applications like $\delta~\delta$ and $x~x$ are ill-typed. However,
when introducing gradual types, one usually expects to accommodate such idioms,
and therefore in a standard gradually-typed calculus such as
<cit.>, a variant of $\Omega$ that uses $(\lambda~ x :
\?.~x~x)$ for $\delta$ is well-typed and diverges, that is, admits no normal form.
The reason is that the argument type of $\delta$, the unknown type $\?$, is consistent with the type of $\delta$ itself, $\? \to \?$, and at runtime, nothing prevents reduction from going on forever.
Therefore, if one aims at ensuring in a gradual setting, some care must be taken to restrict expressiveness.

§.§ The Axiomatic Approach

Let us first address the elephant in the room: why would one want to gradualize instead of simply postulating
an axiom for any term (be it a program or a proof) that one does not feel like providing (yet)?

Indeed, we can augment with a general-purpose wildcard axiom $\axiom$:

Axiom _st : forall A, A.

The resulting theory, called , has an obvious practical benefit: we can use
(_st A), hereafter noted _st_A, as a wildcard whenever we are
asked to exhibit an inhabitant of some type A and we do not (yet) want to.
This is exactly what admitted definitions are in , for instance, and they do play an
important practical role at some stages of any development.

However, we cannot use the axiom _st_A in any meaningful way as a value at the
type level.

For instance, going back to <ref>, one might be tempted to give to the filter function on
vectors the type

forall A n (f : A -> bool), vec A n -> vec A _st_nat

, in order to avoid the complications related to specifying the
size of the vector produced by filter.

The problem is that the term:

head nat _st_nat (filter nat 4 even [ 0 ; 1 ; 2 ; 3 ])

does not typecheck because the type of the filtering expression, vec A _st_nat,
is not convertible to vec A (S _st_nat),
as required by the domain type of head nat _st_nat.

So the axiomatic approach is not useful for making dependently-typed programming
any more pleasing.

That is, using axioms goes in total opposition to the gradual typing
criteria <cit.> when it comes to the smoothness of
the static-to-dynamic checking spectrum: given a well-typed term,
making it “less precise” by using axioms for some subterms actually
results in programs that do not typecheck or reduce anymore.

Because  amounts to working in with an initial context extended with $\axiom$, this theory
satisfies normalization () as much as , so conversion remains decidable. However,
lacks a satisfying notion of safety because
there is an infinite number of open canonical normal forms (more
adequately called stuck terms) that inhabit any type A.

For instance, in bool, we not only have the normal forms true,
false, and _st_bool, but an infinite number of terms stuck on
eliminations of $\axiom$, such as match _st_A with ...
or $\axiom_{\nat \rightarrow \bool}\;1$.

§.§ The Exceptional Approach

<cit.> present the exceptional type theory ,
demonstrating that it is possible to extend a
type theory with a wildcard term while enjoying a satisfying notion of safety,
which coincides with that of programming languages with exceptions.

is essentially , that is, it
extends with an indexed error term raise_A that can inhabit any type A. But instead
of being treated as a computational black box like _st_A, raise_A is endowed with computational content
emulating exceptions in programming languages, which propagate instead of being stuck.

For instance, in we have the following conversion:

match raise_bool return nat with | true -> O | false -> 1 end
$\equiv$  raise_nat

Notably, such exceptions are call-by-name exceptions, so one can only
discriminate exceptions on positive types ( inductive types), not on negative
types ( function types). In particular, in , raise_A_->_B  and
fun _ : A => raise_B are convertible, and the latter is considered to be
in normal form. So raise_A is a normal form of A only if A is a positive type.

has a number of interesting properties: it is
normalizing () and safe
(), taking raise_A into account as usual in programming languages where exceptions are possible outcomes of computation: the normal forms of
closed terms of a positive type ( bool) are either the
constructors of that type ( true and false) or
raise at that type ( err_bool).

As a consequence, does not satisfy full canonicity, but it
does satisfy a weaker form of it. In particular, enjoys
(weak) logical consistency: any closed proof of False is convertible to
raise_False, which is discriminable at False.

It has been shown that we can still reason soundly in an
exceptional type theory, either using a parametricity
requirement <cit.>, or more flexibly, using
different universe hierarchies <cit.>.

It is also important to highlight that this weak form of logical
consistency is the most one can expect in
a theory with effects. Indeed, <cit.> have
shown that it is not possible to define a type theory with full
dependent elimination that has observable effects (from which
exceptions are a particular case) and at the same time validates
traditional canonicity.

Settling for less, as explained in <ref> for the axiomatic
approach, leads to an infinite number of stuck terms, even in the
case of booleans, which is in opposition to the type safety criterion of gradual languages,
which only accounts for runtime type errors.

Unfortunately, while solves the safety issue of the axiomatic approach, it still suffers from the same limitation as the axiomatic approach regarding type-level computation. Indeed, even though we can use raise_A to inhabit any type, we cannot use it in any meaningful way as a value at the type level. The term:

head nat err_nat (filter nat 4 even [ 0 ; 1 ; 2 ; 3 ])

does not typecheck, because vec A raise_nat is still not convertible to vec A (S raise_nat). The reason is that raise_nat behaves like an extra constructor to nat, so
S raise_nat is itself a normal form, and normal forms with different head constructors (S and raise_nat) are not convertible.

§.§ The Gradual Approach: Simple Types

Before going on with our exploration of the fundamental challenges in gradual dependent type theory, we review some key concepts and expected properties in the context of simple types <cit.>.

Static semantics Gradually-typed languages introduce
the unknown type, written , which is used to indicate the lack of static typing information <cit.>.
One can understand such an unknown type in terms of an abstraction of the
set of possible types that it stands for <cit.>. This
interpretation provides a naive but natural understanding of the meaning of partially-specified types, for instance $\bool \to \?$ denotes the set of all function types with $\bool$ as domain. Given imprecise types, a gradual type system relaxes all type predicates and functions in order to optimistically account for occurrences of .  In a simple type system, the predicate on types is equality, whose relaxed counterpart is called consistency.[Not to be confused
with logical consistency!] For instance, given a function f of type $\bool \to \?$, the expression (f true) + 1 is well-typed because f could plausibly return a number, given that its codomain is , which is consistent with nat.

Note that there are other ways to consider imprecise types, for instance by restricting the unknown type to denote base types (in which case $\?$ would not be consistent with any function type), or to only allow imprecision in certain parts of the syntax of types, such as effects <cit.>, security labels <cit.>, annotations <cit.>, or only at the top-level <cit.>. Here, we do not consider these specialized approaches, which have benefits and challenges of their own, and stick to the mainstream setting of gradual typing in which the unknown type is consistent with any type and can occur anywhere in the syntax of types.

Dynamic semantics
Having optimistically relaxed typing based on consistency, a gradual language must detect inconsistencies at runtime if it is to satisfy safety (), which therefore has to be formulated in a way that encompasses runtime errors. For instance, if the function f above returns false, then an error must be raised to avoid reducing to false + 1—a closed stuck term, denoting a violation of safety. The traditional approach to do so is to avoid giving a direct reduction semantics to gradual programs, and instead, to elaborate them to an intermediate language with runtime casts, in which casts between inconsistent types raise errors <cit.>. Alternatively—and equivalently from a semantics point of view—one can define the reduction of gradual programs directly on gradual typing derivations augmented with evidence about consistency judgments, and report errors when transitivity of such judgments is unjustified <cit.>. There are many ways to realize each of these approaches, which vary in terms of efficiency and eagerness of checking <cit.>.

Conservativity A first important property of a gradual language is that it is a conservative extension of a related static typing discipline: the gradual and static systems should coincide on static terms. This property is hereafter called Conservativity (), and parametrized with the considered static system. For instance, we write that satisfies . Technically,
<cit.> prove that typing and reduction of and coincide on their common set of terms ( terms that are fully precise). An important aspect of is that the type formation rules and typing rules themselves are also preserved, modulo the presence of  as a new type and the adequate lifting of predicates and functions <cit.>. While this aspect is often left implicit, it ensures that the gradual type system does not behave in ad hoc ways on imprecise terms.

Note that, despite its many issues,  (<ref>) satisfies : all pure (axiom-free) terms behave as they would in . More precisely,
two terms are convertible in  iff they are convertible in .
Importantly, this does not mean that  is a conservative extension of
as a logic—which it clearly is not!

Gradual guarantees
The early accounts of gradual typing emphasized consistency as the central idea. However,
<cit.> observed that this characterization left too many possibilities for the impact of type information on program behavior, compared to what was originally intended <cit.>. Consequently, <cit.> brought forth type precision (denoted precise) as the key notion, from which consistency can be derived: two types A and B are consistent if and only if there exists T such that T precise A and T precise B. The unknown type  is the most imprecise type of all,  T precise ? for any T.

Precision is a preorder that can be used to capture the intended monotonicity of the static-to-dynamic spectrum afforded by gradual
The static and dynamic gradual guarantees specify that typing
and reduction should be monotone with respect to precision:
losing precision should not introduce new static or dynamic errors.
These properties require precision to be extended from types to terms. <cit.> present a natural extension that is purely syntactic: a term is more precise than another if they are syntactically equal except for their type annotations, which can be more precise in the former.

The static gradual guarantee (SGG) ensures that imprecision does not break typeability:

If t precise u and t : T, then u :
U for some U such that T precise U.

The SGG captures the intuition that “sprinkling  over a term” maintains its typeability. As such, the notion of precision precise used to formulate the SGG is inherently syntactic, over as-yet-untyped terms: typeability is the consequence of the SGG theorem.

The dynamic gradual guarantee (DGG) is the key result that
bridges the syntactic notion of precision to reduction: if t precise u
and t reduces to some value v, then
u reduces to some value v' such that v precise v'; and if t diverges, then so does u.
This property entails that t precise u means that t may error more than u, but otherwise they should behave the same.

Instead of the original formulation of the DGG by
<cit.>, <cit.> appeal to the
semantic notion of observational error-approximation to capture
the relation between two terms that are contextually equivalent except
that the left-hand side term may fail more:[Observational
error-approximation does not mention the case where $\mathcal{C}[t]$
reduces to $\mathtt{true}$ or $\mathtt{false}$ but the quantification
over all contexts ensures that, in that case, $\mathcal{C}[u]$ must
reduce to the same value.]

A term $\Gamma \vdash t : A$ observationally error-approximates
a term $\Gamma \vdash u : A$, noted $ t
\obsApprox u$, if for all boolean-valued observation contexts
$\mathcal{C} : (\Gamma \vdash A) \Rightarrow (\vdash \bool{})$ closing over all
free variables, either

* $\mathcal{C}[t]$ and $\mathcal{C}[u]$ both diverge.

* Otherwise if $\mathcal{C}[u] \rtred \err_{\bool}$, then $\mathcal{C}[t] \rtred \err_{\bool}$.

Using this semantic notion, the DGG simply states that term
precision implies observational error-approximation:

If t precise u then t obsApprox u.

While often implicit, it is important to highlight that the DGG is relative to both the notion of precision precise and the notion of observations obsApprox. Indeed, it is possible to study alternative notions of precisions beyond the natural definition stated by <cit.>. For instance, following the Abstracting Gradual Typing methodology <cit.>, precision follows from the definition of gradual types as a concretization to sets of static types. This opens the door to justifying alternative precisions,  by considering that the unknown type only stands for specific static types, such as base types. Additionally, variants of precision have been studied in more challenging typing disciplines where the natural definition seems incompatible with the DGG, see  <cit.>. As we will soon see below, it can also be necessary in certain situations to consider another notion of observations.

Graduality As we have seen, the DGG is relative to a notion of precision, but what should this relation be? To go beyond a syntactic axiomatic definition of precision, <cit.>
characterize the good dynamic behavior of precision: the runtime checking mechanism used to define a gradual language, such as casting, should only perform typechecking, and not otherwise affect behavior.

Specifically, they mandate that precision gives rise
to embedding-projection pairs (ep-pairs):
the cast induced by two types related by precision forms an adjunction,
which induces a retraction.
In particular, going to a less precise type and back is the identity:
for any term a of type A, and given A precise B, then
a::B::A should be observationally equivalent to a (recall from <ref>
that :: is a type ascription).
For instance, 1::?::nat should be equivalent to 1.
Dually, when gaining precision, there is the potential for errors:
given a term b of type B, b::A::B may fail.
By considering error as the least precise term, this can be stated as
b::A::B precise b.
For instance, with the imprecise successor function f := fun n:? => (S n)::? of type ?->?, we have f::nat->bool::?->? precise f, because the ascribed function will fail when applied.

Technically, the adjunction part states that if we have

A precise B, a term a of type A,
and a term b of type B, then
a precise b::A <=> a::B precise b.

The retraction part further states that t is not only more precise
than t::B::A (which is given by the unit of the adjunction) but
is equi-precise to it, noted

t equiprecise t::B::A.

Because the DGG dictates that precision implies observational error-approximation,
equi-precision implies observational equivalence,
and so losing and recovering precision
must produce a term that is observationally
equivalent to the original one.

A couple of additional observations need to be made here, as they will play a major role in the development of this article:

* These two approaches to characterizing gradual typing highlight the need to distinguish syntactic from semantic notions of precision. Indeed, with the usual syntactic precision from <cit.>, one cannot derive the ep-pair property, in particular the equi-precision stated above.
This is why <cit.> introduce a semantic
precision, defined on well-typed terms. This semantic precision serves
as a proxy between the syntactic precision and the desired
observational error-approximation.

* A type-based semantic precision cannot be used for the SGG. Indeed, this theorem (not addressed by <cit.>) requires a syntactic notion of precision that predates typing: well-typedness of the less precise term is the consequence of the theorem.
Therefore a full study of a gradual language that covers SGG, DGG, and embedding-projection pairs needs to consider both syntactic and semantic notions of precision.

* The embedding-projection property does not per se imply the DGG: one could pick precision to be the universal relation, which trivially induces ep-pairs, but does not imply observational error-approximation. It appears that, in the simply-typed setting considered in prior work, the DGG implies the embedding-projection property. In fact, <cit.> essentially advocate ep-pairs as an elegant and compositional proof technique to establish the DGG. But as we uncover later in this article, it turns out that in certain settings—and in particular dependent types—the embedding-projection property imposes more desirable constraints on the behavior of casts than the DGG alone.

In this paper, we use the term Graduality () for the DGG established with respect to a notion of precision that also induces embedding-projection pairs.

§.§ The Gradual Approach: Dependent Types

Extending the gradual approach to a setting with full dependent types requires reconsidering several aspects.

Newcomers: the unknown term and the error type

In the simply-typed setting, there is a clear stratification: $\?$ is at the type level, raise is at the term level. Likewise, type precision, with  as greatest element, is separate from term precision, with raise as least element.
In the absence of a type/term syntactic distinction as in , this stratification is untenable:

* Because types permeate terms,  is no longer only the unknown type, but it also acts as the “unknown term”. In particular, this makes it possible to consider unknown indices for types, as in <ref>. More precisely, there is a family of unknown terms ?_A, indexed by their type A. The traditional unknown type is just ?_Type, the unknown of the universe Type.

* Dually, because terms permeate types, we also have the “error type”, raise_Type.
We have to deal with errors in types.

* Precision must be unified as a single preorder, with $\?$ at the top and raise at the bottom. The most imprecise term of all is $\mathtt{\?_{\?_\square}}$ ($\?$ for short)—more exactly, there is one such term per type universe. At the bottom, raise_A is the most precise term of type A.

Revisiting safety

The notion of closed canonical forms used to characterize legitimate normal forms
via safety () needs to be extended not only with errors as in the
simply-typed setting, but also with unknown terms.
Indeed, as there is an unknown term ?_A inhabiting any type
A, we have one new canonical form for each type A. In particular,
?_bool cannot possibly reduce to either true or false
or raise_bool, because doing so would collapse the precision order.

Therefore, ?_A should propagate computationally,
like raise_A (<ref>).

The difference between errors and unknown terms is rather on their
static interpretation.

In essence, the unknown term ?_A is a dual form of exceptions: it
propagates, but is optimistically comparable, consistent
with, any other term of type A. Conversely, raise_A
should not be consistent with any term of type A.

Going back to the issues we identified with the axiomatic (<ref>) and exceptional
(<ref>) approaches when dealing with type-level computation, the term:

head nat ?_nat (filter nat 4 even [ 0 ; 1 ; 2 ; 3 ])

now typechecks: vec A ?_nat can be deemed consistent with
vec A (S ?_nat), because S ?_nat is consistent with ?_nat.
This newly-brought flexibility is the key to support the different scenarios from the introduction.

So let us now turn to the question of how to integrate consistency in
a dependently-typed setting.

Relaxing conversion
In the simply-typed setting, consistency is a relaxing of syntactic type equality to account for imprecision. In a dependent type theory, there is a more powerful notion than syntactic equality to compare types, namely conversion (<ref>): if t:T and T==U, then t:U.
For instance, a term of type T can be used as a function as soon as T
is convertible to the type forall (a:A),B for some types A and B.
The proper notion to relax in the gradual dependently-typed setting is therefore conversion, not syntactic equality.

<cit.> give a general framework for gradual typing that explains how to relax any static type predicate to account for imprecision: for a binary type predicate P, its consistent lifting Q(A,B) holds iff there exist static types A' and B' in the denotation (concretization in abstract interpretation parlance) of A and B, respectively, such that P(A',B'). As observed by <cit.>, when applied to equality, this defines consistency as a unification problem. Therefore, the consistent lifting of conversion ought to be that two terms t and u are consistently convertible iff they denote some static terms t' and u' such that t' == u'. This property is essentially higher-order unification, which is undecidable.

It is therefore necessary to adopt some approximation of consistent conversion (hereafter called consistency for short) in order to be able to implement a gradual dependent type theory.
And there lies a great challenge: because of the absence of stratification between typing and reduction, the static gradual guarantee (SGG) already demands monotonicity for conversion, a demand very close to that of the DGG.[In a dependently-typed programming language with separate typing and execution phases, this demand of the SGG is called the normalization gradual guarantee by <cit.>.]

Dealing with neutrals
Prior work on gradual typing usually only considers reduction on closed terms in order to establish results about the dynamics, such as the DGG.

But in dependent type theory,
conversion must operate on open terms, yielding neutral terms such as 1::X::nat where X is a type variable, or x+1 where x is of type nat or ?_Type.

Such neutral terms cannot reduce further, and can occur in both terms and types. Depending on the upcoming substitutions, neutrals can fail or not. For instance, in 1::X::nat, if ?_Type is substituted for X, the term reduces to 1, but fails if bool is substituted instead.

Importantly, less precise variants of neutrals can reduce more. For instance, both
1::?_Type::nat and ?_nat+1 are less precise than the neutrals above, but do evaluate further (typically, to 1 and to ?_nat, respectively). This interaction between neutrals, reduction, and precision spices up the goal of establishing DGG and . In particular, this re-enforces the need to consider semantic precision, because a syntactic precision is likely not to be stable by reduction: 1::X::nat precise 1::?::nat is obvious syntactically, but 1::X::nat precise 1 is not.

DGG vs Graduality In a dependently-typed setting, it is possible to satisfy the DGG while not satisfying the embedding-projection pairs requirement of .

To see why, consider a system in which any term of type A that is not fully-precise immediately reduces to ?_A. This system would satisfy , , , and …the DGG. Recall that the DGG only requires reduction to be monotone with respect to precision, so using the most imprecise term ?_A as a universal redux is surely valid. This collapse of the DGG is impossible in the simply-typed setting because there is no unknown term: it is only possible when ?_A exists as a term. It is therefore possible to satisfy the DGG while being useless when computing with imprecise terms.
Conversely, the degenerate system breaks the embedding-projection requirement of graduality stated by <cit.>.
For instance, 1::?_Type::nat would be convertible to ?_nat, which is
not observationally equivalent to 1.
Therefore, the embedding-projection requirement of graduality goes beyond the DGG in a way that is critical in a dependent type theory, where it captures both the smoothness of the static-to-dynamic checking spectrum, and the proper computational content of valid uses
of imprecision.

Observational refinement

Let us come back to the notion of observational
error-approximation used in the simply-typed setting to state the
<cit.> justify this notion because in
“gradual typing we are not particularly interested in
when one program diverges more than another, but rather when it
produces more type errors.”

This point of view is adequate in the simply-typed setting because
the addition of casts may only produce more type errors; in particular,
adding casts can never lead to divergence when the original term does not diverge

Therefore, in that setting, the definition of error-approximation
includes equi-divergence.

The situation in the dependent setting is however more
complicated, if the theory admits divergence.
There exist non-gradual dependently-typed programming languages that admit divergence ( Dependent Haskell <cit.>,  <cit.>); we will also present one such theory in this article.

In a gradual dependent type theory that admits divergence,

a diverging term is more precise than the
unknown term $\?$. Because the unknown term in itself does not diverge, this
breaks the left-to-right implication of
equi-divergence. Note that this argument does not rely on any specific definition of precision,
just on the fact that the unknown term is the most imprecise term (at its type).

Additionally, an error at a diverging type $X$ may be ascribed to $\?_{[]}$
then back to $X$. Evaluating this
roundtrip requires evaluating $X$ itself, which makes the less
precise term diverge. This breaks the right-to-left implication of

To summarize,
the way to understand these counterexamples is that
in a dependent and non-terminating setting,
the motto of graduality ought to be adjusted: more precise programs produce
more type errors or diverge more. This leads to the following definition
of observational refinement.

A term $\Gamma \vdash t : A$ observationally refines a term $\Gamma \vdash u : A$, noted $ t
\obsRef u$  if for all boolean-valued observation context
$\mathcal{C} : (\Gamma \vdash A) \Rightarrow (\vdash \bool{})$ closing over all
free variables, if $\mathcal{C}[u] \rtred \err_{\bool}$ or diverges, then either $\mathcal{C}[t] \rtred \err_{\bool}$ or $\mathcal{C}[t]$ diverges.

In this definition, errors and divergence are collapsed. Thus, in a gradual dependent theory that admits divergence, equi-refinement does not imply observational equivalence, because one term might diverge while the other reduces to an error. Of course, if the gradual dependent theory is strongly normalizing, then both notions $\obsApprox$ (<ref>) and  $\obsRef$ (<ref>)  coincide.

§.§ The Fire Triangle of Graduality

To sum up, we have seen four important properties that can be expected from a gradual type theory:
safety (), conservativity with respect to a theory $X$ (X), graduality (),
and normalization (). Any type theory ought to satisfy at least . Unfortunately, we now show that mixing the three other properties , and is impossible for , as well as for .

Preliminary: regular reduction.
To derive this general impossibility result, by relying only on the properties and without committing to a specific language or theory, we need to assume that the reduction system used to decide conversion is regular, in that it only looks at the weak head normal form of subterms for reduction rules, and does not magically shortcut reduction, for instance based on the specific syntax of inner terms. As an example, $\beta$-reduction is not allowed to look into the body of the lambda term to decide how to proceed.

This property is satisfied in all actual systems we know of, but formally stating it in full generality, in particular without devoting
to a particular syntax, is beyond the scope of this paper. Fortunately, in the following, we need only rely on a much weaker hypothesis,
which is a slight strengthening of the retraction hypothesis of .
Recall that retraction says that when A precise B, any term t of type A is equi-precise to t::B::A.

We additionally require that for any context C, if C[t]
reduces at least $k$ steps, then C[t::B::A] also reduces at
least $k$ steps.
Intuitively, this means that the reduction of C[t::B::A], while free to decide when to get rid of the embedding-to-B-projection-to-A, cannot use it to avoid reducing t. This property is true in all gradual languages, where type information at runtime is used only as a monitor.

Gradualizing .
Let us first consider the case of .

We show that $\Omega$ is necessarily a well-typed diverging term in any
gradualization of that satisfies the other properties.

Suppose a gradual type theory that satisfies properties
and .

Then cannot hold.

We pose $\Omega := \delta~(\asc{\delta}{\?})$ with
$\delta := \lambda~ x : \?.~(\asc{x}{\? \to
\?})~x$ and show that it must necessarily be a well-typed diverging

Because the unknown type  is consistent with any type (<ref>) and $\? \to \?$ is a valid type (by ), the self-applications in $\Omega$ are well-typed, $\delta$ has type $\? \to \?$, and $\Omega$ has type $\?$.

Now, we remark that $\Omega = C[\delta]$ with $C[\cdot] = [\cdot]~(\asc{\delta}{\?})$.

We show by induction on $k$ that $\Omega$ reduces at least $k$
steps, the initial case being trivial.

Suppose that $\Omega$ reduces at least $k$ steps.

By maximality of $\?$ with respect to precision, we have that
$\? \to \? \pre \?$, so we can apply the strengthening of applied to $\delta$, which tells us that
$C[\asc{\asc{\delta}{\?}}{\?\to\?}]$ reduces at least $k$ steps
because $C[\delta]$ reduces at least $k$ steps.

But by $\beta$-reduction, we have that $\Omega$ reduces in one step to
$C[\asc{\asc{\delta}{\?}}{\?\to\?}]$. So $\Omega$ reduces at least
$k+1$ steps.

This means that $\Omega$ diverges, which is a violation of .

This result could be extended to all terms of the untyped lambda calculus, not only $\Omega$, in order to obtain the embedding theorem of  <cit.>. Therefore, the embedding theorem is not an independent property, but rather a consequence of and —that is why we have not included it as such in our overview of the gradual approach (<ref>).

Gradualizing .
We can now prove the same impossibility theorem for , by reducing
it to the case of . Therefore this theorem can be proven
for type theories others than , as soon as they faithfully embed .

A gradual dependent type theory cannot simultaneously satisfy properties
, and .

We show that a gradual dependent type theory satisfying  and must contain a diverging term, thus contravening .
The typing rules of contain the typing rules of ,
using only one universe $[]_0$,
where the function type is interpreted using the dependent
product and the notions of reduction coincide, so embeds
; a well-known result on PTS <cit.>.

This means that  implies .

Additionally, can be specialized to the simply-typed fragment of the theory,
by setting the unknown type $\?$ to be $\?_{[]_0}$. Therefore, we can apply
<ref> and we get a well-typed term that diverges, finishing the proof.

The Fire Triangle in practice
In non-dependent settings, all gradual languages where  is universal admit non-termination and therefore compromise . <cit.> discuss the possibility to gradualize without admitting non-termination, for instance by considering that  is not universal and denotes only base types (in such a system, ? -> ? nprecise ?, so the argument with $\Omega$ is invalid).
Without sacrificing the universal unknown type, one could design a variant of that uses some mechanism to detect divergence, such as termination contracts <cit.>. This would yield a language that certainly satisfies , but it would break . Indeed, because the contract system is necessarily over-approximating in order to be sound (and actually imply ), there are effectively-terminating programs with imprecise variants that yield termination contract errors.

To date, the only related work that considers the gradualization of full dependent types with  as both a term and a type, is the work on GDTL <cit.>. GDTL is a programming language
with a clear separation between the typing and execution phases, like  <cit.>.
GDTL adopts a different strategy in each phase: for typing, it uses Approximate Normalization (AN), which always produces ?_A as a result of going through imprecision and back. This means that conversion
is both total and decidable (satisfies ), but it breaks for the same reason as the degenerate system we discussed in <ref> (notice that the example uses a gain of precision from the unknown type to nat, so the example behaves just the same with AN).
In such a phased setting, the lack of computational content of AN is not critical, because it only means that typing becomes overly optimistic. To execute programs, GDTL relies on standard -like reduction semantics, which is computationally precise, but does not satisfy .

§ : OVERALL APPROACH, MAIN CHALLENGES AND RESULTS

Given the Fire Triangle of Graduality (<ref>), we know that gradualizing implies making some compromise.
Instead of focusing on one possible compromise, this work develops
three novel solutions, each compromising one specific property (, , or ), and does so in a common parametrized framework, .

This section gives an informal, non-technical overview of our approach to gradualizing , highlighting the main challenges and results. As such, it serves as a gentle roadmap to the following sections, which are rather dense and technical.

§.§ : 3-in-1

To explore the spectrum of possibilities enabled by the Fire Triangle of Graduality, we develop a general approach to gradualizing , and use it to define three theories, corresponding to different resolutions of the triangular tension between normalization (), graduality () and conservativity with respect to ().

The crux of our approach is to recognize that, while there is not much to vary within itself to address the tension of the Fire Triangle of Graduality, there are several variants of that can be considered by changing the hierarchy of universes and its
impact on typing—after all, is but a particular Pure Type System
(PTS) <cit.>.

In particular, we consider a parametrized version of a gradual , called , with two parameters (<ref>):

* The first
parameter characterizes how the universe level of a $\Pi$ type is determined
in typing rules: either as taking the maximum of the levels of the involved
types, as in standard , or as the successor of that maximum. The latter option yields a variant
of that we call (read “-shift”). is a subset of , with a stricter constraint on universe levels. In particular loses the closure of universes under dependent product that CIC enjoys. As a consequence, some well-typed terms are not well-typed in .[A minimal example of a well-typed term that is ill typed in is  $\nat -> \square$, where  is the type of functions that accept  arguments. Such dependent arities violate the universe constraint of .]

* The second parameter is the dynamic counterpart of the first parameter: its role is to enforce that universe levels are coherent through type casts during the reduction of casts.
Note that we only allow this reduction parameter to be loose ( using maximum) if the typing parameter is also loose. Indeed, letting the typing parameter be strict ( using successor) while the reduction parameter is loose breaks subject reduction, and hence .

Based on these parameters, this work develops the following three variants of ,
whose properties are summarized in <ref> with pointers to the respective theorems—because is one common parametrized framework, we are able to establish most properties for all variants at once:

* : a theory that satisfies both  and , but sacrifices .
This theory is a rather direct application of the
principles discussed in <ref> by extending with errors and unknown terms, and changing conversion with
consistency. This results in a theory that is not normalizing.

* : a theory that satisfies both and , and supports with respect to . This theory uses the universe hierarchy at the typing level to detect
the potential non-termination induced by the use of consistency
instead of conversion. This theory simultaneously satisfies , and

* : a theory that satisfies both  and , but does not fully validate .
This theory uses the
universe hierarchy at the computational level to detect
potential divergence. Such runtime check failures invalidate the DGG for some terms,
and hence , as well as the SGG.

X         SGG     DGG

(Th. thm:ccic-psafe)
(Th. thm:conservativity)
(Th.  thm:GCICP-graduality)
(Th. thm:static-graduality)
(Th. thm:dgg)

(Th. thm:ccic-pnorm & thm:discrete-model)
(Th. thm:graduality-gcics)
(Th. thm:dgg)

$\mathsf{CIC}$$^{\uparrow}$    (idem)

: safety, : normalization, X: conservativity wrt theory $X$,
: graduality (DGG + ep-pairs),
SGG: static gradual guarantee, DGG: dynamic gradual guarantee

variants and their properties

Practical implications of variants. Regarding the examples from <ref>, all three variants of support the exploration of the type-level precision spectrum for the functions described in <ref>.  In particular, we can define filter by giving it the imprecise type
forall A n (f : A -> bool), vec A n -> vec A ?_nat in order to bypass the difficulty of precisely characterizing the size of the output vector. Any invalid optimistic assumption is detected during reduction and reported as an error.

Unsurprisingly, the semantic differences between the three variants crisply manifest in the treatment of potential non-termination (<ref>), more specifically, self application.

Let us come back to the term $\Omega$
used in the proof of <ref>.
In all three variants, this term is well-typed. In , it
reduces forever, as it would in the untyped lambda calculus. In that
sense, can embed the untyped lambda calculus just as
GTLC <cit.>. In , this term fails at runtime
because of the strict universe check in the reduction of casts, which
breaks graduality because $\coqe{?_Typei -> ? _Typei precise ?_Typei}$
tells us that the upcast-downcast coming from an should not fail.

A description of the reductions in and in is given in
full details in <ref>.

In , Omega fails in the same way as in , but this
does not break graduality because of the shifted universe level on
$\Pi$ types.

A consequence of this stricter typing rule is that in , ?_Typei -> ?_Typei precise ?_Typej for any $j > i$, but ?_Typei -> ?_Typei nprecise ?_Typei.
Therefore, the casts performed in $\Omega$ do not come from an anymore and can legitimately fail.

Another scenario where the differences in semantics manifest is functions with dependent arities.
For instance, the well-known C function  can be embedded in a well-typed fashion in
: it takes as first argument a format string and computes from it both the type and number
of later arguments.

This function brings out the limitation of : since the format string can
specify an arbitrary number of arguments, we need as many $\to$, and
cannot typecheck in a theory where universes are not closed under
function spaces.

In ,  typechecks but the same problem will appear dynamically
when casting  to $\?$ and back to its original type: the result will be
a function that works only on format strings specifying no more arguments than
the universe level at which it has been typechecked.

Note that this constitutes an example of violation of graduality for
, even of the dynamic gradual guarantee.

Finally, in  the function can be gradualized as much as one wants, without surprises.

Which variant to pick? As explained in the introduction, the aim of this paper is to shed light on the design space of gradual dependent type theories, not to advocate for one specific design.

We believe the appropriate choice depends on the specific goals of the language designer, or perhaps more pertinently, on the specific goals of a given project, at a specific point in time.

The key characteristics of each variant are:

* favors flexibility over decidability of type-checking. While this might appear heretical in the context of proof assistants, this choice has been embraced by practical languages such as Dependent Haskell <cit.>, a dependently-typed Haskell where both divergence and runtime errors can happen at the type level. The pragmatic argument is simplicity: by letting programmers be responsible, there is no need for termination checking techniques and other restrictions.

* is theoretically pleasing as it enjoys both normalization and graduality. In practice, though, the fact that it is not conservative wrt full means that one would not be able to simply import existing libraries as soon as they fall outside of the subset.
In , the introduction of  should be done with an appropriate understanding of universe levels. This might not be a problem for advanced programmers, but would surely be harder to grasp for beginners.

* is normalizing and able to import existing libraries without restrictions, at the expense of some surprises on the graduality front. Programmers would have to be willing to accept that they cannot just sprinkle  as they see fit without further consideration, as any dangerous usage of imprecision will be flagged during conversion.

In the same way that systems like , or support
different ways to customize their semantics (such as allowing
, switching off termination checking, using the /
compiler flags)—and of course, many programming languages implementations supporting some sort of customization, GHC being a salient representative—one can imagine a flexible realization of that give users the control over the two parameters we identify in this work, and therefore have access to all three variants.

Considering the inherent tension captured by the Fire Triangle of Graduality, such a pragmatic approach might be the most judicious choice, making it possible to gather experience and empirical evidence about the pros and cons of each in a variety of concrete scenarios.

§.§ Typing, Cast Insertion, and Conversion

As explained in <ref>,
in a gradual language, whenever we reclaim precision, we might be wrong and need to fail in order to preserve safety ().

In a simply-typed setting, the standard approach is to define typing on the
gradual source language, and then to translate terms via a type-directed cast insertion
to a target cast calculus,  a language with explicit runtime type
checks, needed for a well-behaved reduction <cit.> . For instance, in a call-by-value language, the upcast (loss of precision) $\ascdom{10}{\nat}{\?}$ is considered a (tagged) value, and the downcast (gain of precision) $\ascdom{v}{\?}{\nat}$ reduces successfully if $v$ is such a tagged natural number, or to an error otherwise.

We follow a similar approach for , which is
elaborated in a type-directed manner to a second calculus,
named (<ref>).
The interplay between typing and cast insertion is however more subtle in the
context of a dependent type theory. Because typing needs computation, and
reduction is only meaningful in the target language, is used
as part of the typed elaboration in order to compare types (<ref>).
This means that has no typing on its own, independent of its
elaboration to the cast calculus.
[This is similar to what happens in practice in proof assistants such as <cit.>, where terms input by the user in the Gallina language are first elaborated in order to add implicit arguments, coercions, etc. The computation steps required by conversion are
performed on the elaborated terms, never on the raw input syntax.]

In order to satisfy conservativity with respect to (), ascriptions in are required to satisfy consistency: for instance, true::?::nat is well-typed by consistency (twice), but true::nat is ill typed. Such ascriptions in are realized by casts. For instance
in elaborates (modulo sugar and reduction) to $\ascdom{\ascdom{0}{\nat}{\?_{[]}}}{\?_{[]}}{\bool}$ in .
A major difference between ascriptions in and casts in is
that casts are not required to satisfy consistency: a cast between any
two types is well-typed, although of course it might produce an

Finally, standard presentations of use a standalone conversion rule, as usual in declarative presentations of type systems. To gradualize , we have to move to a more algorithmic presentation in order to forbid transitivity, otherwise all terms would be well-typed by way of a transitive step through ?. But  demands that only terms with explicitly-ascribed imprecision enjoy its flexibility.
This observation is standard in the gradual typing literature <cit.>. As in prior work on gradual dependent types <cit.>, we adopt a bidirectional presentation of typing for (<ref>), which allows us to avoid accidental transitivity and directly derive a deterministic typing algorithm for .

§.§ Realizing a Dependent Cast Calculus:

To inform the design and justify the reduction rules provided for
, we build a
syntactic model of by translation to augmented with
induction-recursion <cit.> (<ref>). From a type
theory point of view, what makes peculiar is first of all the
possibility of having errors (both “pessimistic” as raise and
“optimistic” as ?), and the necessity to do intensional type
analysis in order to resolve casts. For the former, we build upon the work of
<cit.> on the exceptional type theory .
For the latter, we reuse the technique of <cit.> to account for
typerec, an elimination principle for the universe Type, which
requires induction-recursion to be implemented.

We call the syntactic model of the discrete model, in contrast with
a semantic model motivated in the next subsection. The discrete model of captures the intuition that the unknown type is
inhabited by “hiding” the underlying type of the injected term. In other words,
?_Typei behaves as a
dependent sum Sigma A:Typei. A.
Projecting out of the unknown type is realized
through type analysis (typerec), and may fail (with an error in the sense).

Note that here, we provide a particular interpretation of the unknown
term in the universe, which is legitimized by an observation
made by <cit.>: does not constrain in
any way the definition of exceptions in the universe.

The syntactic model of allows us to establish that the reduction semantics enjoys strong normalization (), for the two variants and . Together with
safety (), this gives us weak logical consistency for and .

§.§ Precisions and Properties

As explained earlier (<ref>), we need two different notions of
precision to deal with SGG and .

At the source level (), we introduce a notion of syntactic precision that captures the
intuition of a more imprecise term as “the same term with subterms and/or annotated types replaced by ”, and is defined without any assumption of typing.

In , we define a notion of structural precision, which is mostly syntactic except that, in order to account for cast insertion during elaboration, it tolerates precision-preserving casts (for instance, $\ascdom{t}{A}{A}$ is related to $t$ by structural precision).
Armed with these two notions of precision, we prove

elaboration graduality (<ref>), which is
the equivalent of SGG in our setting: if a term $t$ of elaborates to a
term $t'$ of , then a term $u$ less syntactically precise than $t$ in elaborates to
a term $u'$ less structurally precise than $t'$ in .

Because DGG is about the behavior of terms, it is technically stated and
proven for . We show in <ref> that DGG can be proven
for (in its variants and ) on the structural
However, as explained in <ref>, we cannot expect to prove for these variants with respect to structural precision directly.
In order to overcome this problem, we build an alternative model of
called the monotone model (<ref>).
This model endows types with the structure of an ordered set, or poset. In
the monotone model, we can reason about the semantic notion of propositional
precision and prove that it gives rise to embedding-projection
pairs <cit.>, thereby establishing
for (<ref>).

The monotone model only works for a normalizing gradual type theory,
thus we then establish for using a variant of the
monotone model based on Scott's
model <cit.> of the untyped $\lambda$-calculus using $\omega$-complete
partial orders (<ref>).

§ PRELIMINARIES: BIDIRECTIONAL

We develop on top of a bidirectional version of , whose
presentation was folklore among type
theory specialists <cit.>, and that has recently been
studied in details by <cit.>.

As explained before, this bidirectional
presentation is mainly useful to avoid multiple uses of a standalone conversion rule
during typing, which becomes crucial to preserve  in a gradual setting
where conversion is replaced by consistency, which is not transitive.

We give here a comprehensive summary of the bidirectional version of
that will help the reader follow the presentation of in <ref>.

Our syntax for terms, featuring a predicative universe hierarchy $[]_i$, is the following (in Backus-Naur form):

\begin{align}
\label{fig:syntax-cic}
\terms_{\CIC} \ni t ::= x \mid \square{}_i \mid t~t \mid \l x : t . t \mid \P x : t . t \mid I\ulev{i}(\orr{t}) \mid c\ulev{i}(\orr{t},\orr{t}) \mid \match{I}{t}{z.t}{f.\orr{y}.\orr{t}} \tag{Syntax of \CIC}
\end{align}

We reserve letters $x,y,z$ to denote variables. Other lower-case and upper-case Roman letters are used to represent terms, with the latter
used to emphasize that the considered terms should be thought of as types (although the difference does not occur at a syntactic level in
this presentation). Finally Greek capital letters are for contexts
(lists of declarations of the form $x : T$).
We also use bold letters $\mathbf{X}$ to denote sequences of objects
and $t\subs{\mathbf{a}}{\mathbf{y}}$ for the simultaneous substitution of $\orr{a}$ for
We present generic inductive types $I$ with constructors $c$, although we restrict to well-formed (and in particular, strictly positive) ones
to preserve normalization, following <cit.>.

At this point we consider only inductive types without indices; we consider indexed inductive types in <ref>.
Inductive types are formally annotated with a universe level $\ulev{i}$, controlling the level of its parameters:
for instance $\operatorname{List}\ulev{i}(A)$ expects $A$ to be a type in $[]_i$. This level is omitted when inessential.

An inductive type at level $i$ with parameters $\orr{a}$ is noted $I\ulev{i}(\orr{a})$, and we use $\pars(I,i)$ to denote the types of those parameters.

The well-formedness condition on inductives in particular enforces that the $k$-th parameter
$\pars_k(I,i)$ only contains $k-1$ variables, corresponding to the previous $k-1$ parameters.
Thus if $\orr{a}$ is a list of terms of the same length as $\pars(I,i)$ we denote as
$\pars(I,i)\parsub{\orr{a}}$ the list where in parameter type $\pars_k(I,i)$, the $k-1$ first
elements of $\orr{a}$ have been substituted for the $k-1$ free variables.
Similarly $c_k^I\ulev{i}(\orr{a},\orr{b})$ denotes the $k$-th constructor of the
inductive $I$, taking parameters $\orr{a}$ and arguments $\orr{b}$. Again, the type
of parameters is denoted $\pars(I,i)$, and the type of the arguments $\args(I,i,c_k)$.
Similarly as for parameters, we also use $\args(I,i,c_k)\parsub{\orr{a},\orr{b}}$ for
the list where in the $m$-th argument type
$\orr{a}$ have been substituted for parameter variables, and
the first $m-1$ elements of $\orr{b}$ for argument variables.

The inductive eliminator $\match{I}{s}{z.P}{f.\orr{y.t}}$ corresponds to a
fixpoint immediately followed by a match. In , one would write it

fix $f$ $s$ := match $s$ as $z$ return $P$ with | $c_1~\orr{y}$ => $t_1$ ... | $c_n~\orr{y}$ => $t_n$ end

In particular, the return predicate $P$ has access to an extra bound variable $z$ for the scrutinee, and similarly
the branches $t_k$ are given access to variables $f$ and $\orr{y}$,
corresponding respectively to the recursive function and the
arguments of the corresponding constructor.
Describing the exact guard condition to ensure termination is
outside the scope of this presentation, again see <cit.>.
We implicitly assume in the rest of this paper that every fixpoint is guarded.

Bidirectional Typing

$\vdash \Gamma$

⊢·[Empty] infrule:cic-axiom ⊢Γ
□ □_i⊢Γ, x
: T[Concat] infrule:cic-concat

$\Gamma \vdash t \inferty T$

Γ⊢□_i □_i + 1[Univ] infrule:cic-univ (x : T) ∈ΓΓ⊢x
T[Var] infrule:cic-var Γ⊢A □ □_j
Γ, x :
A ⊢B □ □_iΓ⊢x : A . B
□_max(i,j)[Prod] infrule:cic-prod

Γ⊢A □ □_i
Γ, x : A ⊢t BΓ⊢łx : A . t x : A . B[Abs] infrule:cic-abs Γ⊢t   x : A . B
Γ⊢u AΓ⊢t u Bxu[App] infrule:cic-app

Γ⊢a_k _k(I,i)a
Γ⊢Ii(a) □_i[Ind] infrule:cic-ind
Γ⊢a_k _k(I,i)a

Γ⊢b_m _m(I,i,c)a, b
Ii(a)[Cons] infrule:cic-cons

Γ⊢s I Ii(a)

Γ, z : I(a) ⊢P □ □_j

Γ, f : (z : Ii(a). P), y : (I,i,c_k)a,y ⊢t_k Pc^I_ki(a,y)z
Γ⊢Isz.Pf.y.t Psz[Fix]

$\Gamma \vdash t \checkty T$

Γ⊢t T'
T' TΓ⊢t T[Check] infrule:cic-check

$\Gamma \vdash t \pcheckty{\bullet} T$

Γ⊢t T
T x : A. BΓ⊢t  x : A . B[Prod-Inf] infrule:cic-prod-inf Γ⊢t T
T Ii(a)Γ⊢t I Ii(a)[Ind-Inf] infrule:cic-ind-inf Γ⊢t T
T □_iΓ⊢t □ □_i[Univ-Inf] infrule:cic-univ-inf

$t \redCCIC u$ (congruence rules omitted)

(łx: A . t) u t ux Ic_k(𝐚, 𝐛)z.Pf.y.t
t_k łx: I(𝐚).
f 𝐛𝐲

$t \conv u$

$$t \conv u \quad:=\quad \exists v~v', t \rtred v \wedge u \rtred v'
\wedge v =_\alpha v'$$

where $=_\alpha$ denotes syntactic equality up-to renaming

: Bidirectional typing

In the usual, declarative, presentation of , conversion between types is
allowed at any stage of a typing derivation through a free-standing conversion

However, when conversion is replaced by a non-transitive relation of consistency, this free-standing rule is much too permissive and would violate .

Indeed, as every type should be consistent with the unknown type
$\?_{\square{}}$, using such a rule twice in a row makes it possible to change the type of a
typable term to any arbitrary type: if $\Gamma \vdash t : T$, because $T \cons \?_{[]}$
and $\?_{[]} \cons S$, we could derive $\Gamma \vdash t : S$. This in turn would allow typeability of any term, including fully-precise terms, which is in contradiction with .

Thus, we rely on a bidirectional presentation of typing, presented in <ref>, where the usual judgment $\Gamma \vdash t : T$ is decomposed into several mutually-defined judgments. The difference between the judgments lies in the role of the type:
in the inference judgment $\Gamma \vdash t \inferty T$, the type is considered an output, whereas in the
checking judgment $\Gamma \vdash t \checkty T$, the type is instead seen as an input.

Conversion can then be restricted to specific positions, namely to mediate between
inference and checking judgments (see infrule:cic-check), and can thus never appear
twice in a row.

Additionally, in the framework of an elaboration procedure, it is interesting to make a clear distinction between the subject of the rule (the object that is to be elaborated), inputs that can be used for this elaboration, and outputs that must be constructed during the elaboration.
In the context checking judgment $\vdash \Gamma$, $\Gamma$ is the subject of the judgment. In all the other judgments, the subject is the term, the context is an input, and the type is either an input or an output, as we just explained.

An important discipline, that goes with this distinction, is that judgments should ensure that outputs are well-formed, under the hypothesis that the inputs are. All rules are built to ensure this invariant. This distinction between inputs, subject and output, and the associated discipline, are inspired by <cit.>.

This is also the reason why no rule for term elaboration re-checks the context, as it is an input that is assumed to be well-formed. Hence, most properties we state in an open context involve an explicit hypothesis that the involved context is well-formed.

Constrained Inference
Apart from inference and checking, we also use a set of constrained inference judgments $\Gamma \vdash t \pcheckty{\bullet} T$, with the same modes as inference. These judgments infer the type $T$ but under some constraint $\bullet$: for instance that it should be a universe at some level ($\bullet=\square{}$), a $\Pi$-type ($\bullet=\P$), or an instance of an inductive $I$ ($\bullet=\text{I}$).
Constrained inference judgments come from a close analysis of typing algorithms, such as the one of , where in some places, an intermediate judgment between inference and checking happens: inference is performed, but then the type is reduced to expose its head constructor, which is imposed to be a specific one.
A stereotypical example is infrule:cic-app: one starts by inferring a type for $t$, but want it to be a $\Pi$-type so that its domain can be used to check $u$.
To the best of our knowledge, these judgments have never been formally described elsewhere.
Instead, in the rare bidirectional presentations of , they are inlined in some way, as they only amount to some reduction.
However, this is no longer true in a gradual setting: $\?$ introduces an alternative, valid solution to the constrained inference, as a term of type $\?$ can be used where a term with a $\Pi$-type is expected. Thus, we will need multiple rules for constrained inference, which is why we make it explicit already at this stage.

From here on, we impose no reduction strategy by default, and use $\redCCIC$ and the unqualified word "reduction" for full reduction, reduction that can be performed at an arbitrary place in a term, and $\rtred$ for its reflexive, transitive closure. Most of the properties would however carry over if we fixed weak-head reduction instead, and we sketch at the end of some proofs how they would carry over to such a fixed strategy. As uniqueness of inferred types and elaborated terms becomes stronger with a deterministic reduction strategy, we discuss weak-head reduction specifically in that case.

Finally, we observe that the equivalence of this bidirectional
formulation with standard relies on the transitivity of
conversion; this has been very recently spelled out in details and formalized by

However, in the gradual setting, this property does not hold. This is precisely the point of
using a bidirectional formulation: since
consistency is not a transitive relation, a standard
presentation of typing is not appropriate.

§ FROM TO

We now present the elaboration from the source gradual system to the cast calculus .
We start with , describing its typing, reduction
and metatheoretical properties (<ref>).

We next describe and its elaboration to
, along with few direct properties (<ref>). This elaboration is mainly an extension of the bidirectional presented in the previous section.

We illustrate the semantics of the different variants by considering the $\Omega$ term (<ref>).
We finally expose technical properties
of the reduction of (<ref>) used to prove the most
important theorems on elaboration: conservativity over or , as well as
the gradual guarantees (<ref>).

The syntax of [Written using a blue color.]
extends that of (<ref>)
with three new term constructors: the unknown term $\tcol{\?_T}$ and dynamic
error $\tcol{\err_T}$ of type $\tcol{T}$, as well as the cast $\tcol{\cast{S}{T}{t}}$ of a term $\tcol{t}$ of type $\tcol{S}$ to type $\tcol{T}$

\begin{align}
\label{fig:syntax-castcic}
\tcol{\terms_{\CCIC}} \ni \tcol{t} ::= \dots \mid \tcol{\?_t} \mid \tcol{\err_t} \mid \tcol{\cast{t}{t}{t}} \tag{Syntax of \CCIC}
\end{align}

with casts associating to the right: $\tcol{\cast{S}{S'}{\cast{T'}{T}{t}}}$ is $\tcol{\cast{S}{S'}{\left( \cast{T}{T'}{t}\right)}}$. We also compress successive ones in the following way: $\tcol{\cast{T}{T'' \Leftarrow T'}{t}}$ is shorthand for $\tcol{\cast{T'}{T''}{\cast{T}{T'}{t}}}$.
The unknown term and dynamic error both behave as exceptions as
defined in  <cit.>.

Casts keep track of the use of consistency during elaboration, implementing
a form of runtime type-checking, raising the error $\tcol{\err_T}$ in case of a type mismatch.

We call static the terms of that do not use any of these new constructors—static terms correspond to terms.

Universe parameters

\begin{align}
\qquad \sortOfPi{i}{j} &:= \max(i,j) &   \castOfPi{i} &:= i \label{eq:spi-cpi-gcicp}\tag{\text{\GCICP-\CCICP}}\\[-0.5em]
\sortOfPi{i}{j} &:= \max(i,j) & \castOfPi{i} &:= i-1 \label{eq:spi-cpi-gcict}\tag{\text{\GCICT-\CCICT}}\\[-0.5em]
\sortOfPi{i}{j} &:= \max(i,j)+1 &  \castOfPi{i} &:= i-1 \label{eq:spi-cpi-gcics}\tag{\text{\GCICs-\CCICs}}
\end{align}

Universe parameters

is parametrized by two functions, described in <ref>, to account for the three
different variants of we consider (<ref>).

The first function $\sortOfPiName$ computes
the level of the universe of a dependent product, given
the levels of its domain and codomain (see the updated infrule:ccic-prod rule in <ref>). The second function
$\castOfPiName$ controls the universe level in the reduction of a cast between
$\? \rightarrow \?$ and $\?$ (see <ref>).

<ref> gives the typing rules for the three new primitives of . Apart from the modified infrule:ccic-prod rule, which uses the $\sortOfPiName$ parameter, all other typing rules are exactly the same as in . When disambiguation is needed, we note this typing judgment as $\caty$.

The typing rules infrule:ccic-unk and infrule:ccic-err
say that both $\tcol{\?_T}$ and $\tcol{\err_T}$ infer $\tcol{T}$
when $\tcol{T}$ is a type.

Note that in , as is sometimes the case in cast calculi <cit.>, no consistency premise is required for a cast to be well-typed.
Here, consistency only plays a role in , but disappears after
Instead, we rely on the usual conversion, defined as
in as the existence of $\alpha$-equal reducts for the reduction
described hereafter.

The infrule:ccic-cast rule only ensures that both the source and target of the cast are indeed types, and that the casted term indeed has the source type.

$\tcol{\Gamma} \vdash t \inferty T$

Γ ⊢A [] []_j

Γ, x : A ⊢B [] []_i
Γ ⊢x : A . B []_ij[Prod] infrule:ccic-prod

Γ ⊢T [] []_i
Γ ⊢_T T[Unk]
Γ ⊢T [] []_i
Γ ⊢_T T[Err]
Γ ⊢A [] []_i

Γ ⊢B [] []_j

Γ ⊢t A
Γ ⊢ABt B[Cast]

: Bidirectional typing (extending <ref>,
replacing infrule:cic-prod)

$\H$, $: _ →$̋ and $\stalk : \H \to \types_{\CCIC}$

∋̋h ::= □_i |Π|I

(x : A . B) := Π(□_i) := □_i  (I(𝐚)) := I

:= {
[]_j      if $j < i$

_[]_i     if $j \geq i$
:= I((I,i))
:= {
[]_i →[]_i     if $\castOfPi{i}
\geq 0$

_[]_i     if $\castOfPi{i}
< 0$

Head constructor and germ

The typing rules provide little insight on the new primitives; the interesting
part really lie in their reduction behavior. The reduction rules of are given in
<ref> (congruence rules omitted).
Reduction relies on two auxiliary functions relating head constructors $h \in \H$ (\cref{fig:head-germ}) to those terms that start with either $Π$, $[]$ or $I$, the set of which we call $_$.
The first is the function $$, which returns the head constructor of a type.
In the other direction, the germ%
\footnote{
The germ function corresponds to an abstraction function as in
AGT~\cite{garciaAl:popl2016}, if one interprets the head $h$ as the set of all
types whose head type constructor is $h$. \citet{wadlerFindler:esop2009}
christened the corresponding notion a \emph{ground type}, later reused in the
gradual typing literature. This terminology however clashes with
its prior use in denotational semantics~\cite{Levy2004}: there a ground type
is a first-order datatype. Note that \citet{siekTaha:sfp2006} also call ground types the base types of the language, such as $\bool$ and $\nat$. We therefore prefer the less overloaded term {\em germ}, used by analogy with the
geometrical notion of the \emph{germ of a section}~\cite{maclane-moerdijk}: the
germ of a head constructor represents an equivalence class of types that are
locally the same.
} function
$ih$ constructs the least
precise type with head $h$ at level $i$.
In the case where no such type exists (\eg when $i < 0$),
this least precise type is the error.

\begin{figure}
\boxedrule{$\tcol{t} \redCCIC \tcol{t}$}
\begin{mathpar}
\text{\textbf{Propagation rules for $\tcol{\?}$ and $\tcol{\err}$}} \\
\redrule{
\tcol{\?_{\P(x:A).B}}
\tcol{\l (x : A). \?_{B}}
\hfill}[Prod-Unk]
\ilabel{redrule:prod-unk} \\
\redrule{
\tcol{\err_{\P(x:A).B}}
\tcol{\l (x : A). \err_{B}}
\hfill}[Prod-Err]
\ilabel{redrule:prod-err} \\
\redrule{
\tcol{\match{I}{\?_{I(\mathbf{a})}}{z.P}{f.\mathbf{y.t}}}
\tcol{\?_{P\subs{\?_{I(\orr{a})}}{z}}}
\hfill}[Match-Unk] \ilabel{redrule:match-unk} \\
\redrule{
\tcol{\match{I}{\err_{I(\mathbf{a})}}{z.P}{f.\mathbf{y.t}}}
\tcol{\err_{P\subs{\err_{I(\orr{a})}}{z}}}
\hfill}[Match-Err] \ilabel{redrule:match-err} \\
\redrule{
\tcol{\ascdom{\?_{I(\orr{a})}}{I(\orr{a''})}{I(\orr{a'})}}
\tcol{\?_{I(\orr{a'})}}
\hfill}[Ind-Unk] \ilabel{redrule:ind-unk} \\
\redrule{
\tcol{\ascdom{\err_{I(\orr{a})}}{I(\orr{a''})}{I(\orr{a'})}}
\tcol{\err_{I(\orr{a'})}}
\hfill}[Ind-Err] \ilabel{redrule:ind-err} \\
\redrule{
\tcol{\ascdom{\?_{\?_{\square}}}{\?_{\square}}{X}}
\tcol{\?_{X}}
\hfill}[Down-Unk] \ilabel{redrule:down-unk} \\
\redrule{
\tcol{\ascdom{\err_{\?_{\square}}}{\?_{\square}}{X}}
\tcol{\err_{X}}
\hfill}[Down-Err] \ilabel{redrule:down-err} \\

\text{\textbf{Reduction rules for cast}} \\

\redrule{
\tcol{\ascdom{(\l x : A . t)}{\P (x: A_1). B_1}{\P (y:A_2).B_2}}
\myflushright
}[Prod-Prod] \ilabel{redrule:prod-prod} \\
\myflushright \tcol{ \l y : A_2. \ascdom{(t\subs{\cast{A_2}{A}{y}}{x})}{B_1\subs{\cast{A_2}{A_1}{y}}{x}}{B_2} } \\
\redrule{
\tcol{\ascdom{A}{[]_i}{[]_i}}
}{\tcol{A} \hfill}[Univ-Univ] \ilabel{redrule:univ-univ} \\
\redrule{
\tcol{\ascdom{c(\orr{a},b_1, \dots, b_n)}{I(\orr{a_1})}{I(\orr{a_2})}}
\tcol{ c(\orr{a'}, \orr{b'_1}, \dots, \orr{b'_n})}
\hfill}[Ind-Ind] \label{redrule:ind-ind} \\
\myflushright
\text{with $\tcol{\orr{b_k'}} :=
\tcol{\ascdom{b_k}{\args_k(I,i,c)\parsub{\orr{a},\orr{b}}}{\args_k(I,i,c)\parsub{\orr{a'},\orr{b'}}}}$} \\
\redrule{
\tcol{\ascdom{t}{T}{T'}}
\tcol{\err_{T'}}
}[Head-Err] \ilabel{redrule:head-err}
\hfill \text{when $\tcol{T}, \tcol{T'} \in \types_{\CCIC}$ and $\hd \tcol{T} \neq \hd \tcol{T'}$}
\\
\redrule{
\tcol{\ascdom{t}{\err_{\square}}{T}}
\tcol{\err_T}
\hfill}[Dom-Err] \ilabel{redrule:err-dom} \\
\redrule{
\tcol{\ascdom{t}{T}{\err_{\square}}}
\tcol{\err_{\err_\square}}
}[Codom-Err] \label{redrule:err-codom}
\hfill \text{when $T \in \types_{\CCIC}$} \\
\redrule{
\tcol{\ascdom{f}{\P x:A.B}{\?_{\square_i}}}
\tcol{\cast{\P x:A.B}{\?_{[]_i} \Leftarrow \stalkCIC{i}{\Pi}}{f}}
\hfill}[Prod-Germ] \label{redrule:prod-germ} \\
\myflushright \text{when $\tcol{\P x : A . B} \neq \tcol{\stalkCIC{j}{\Pi}}$ for $j \geq i$} \\
\redrule{
\tcol{\ascdom{t}{I(\orr{a})}{\?_{\square_i}}}
\tcol{\cast{I(\orr{a})}{\?_{[]_i} \Leftarrow \stalkCIC{i}{I}}{t}}
}[Ind-Germ] \label{redrule:ind-germ}
\hfill \text{when $\tcol{I(\orr{a})} \neq \tcol{\stalkCIC{j}{I}}$ for $j\geq i$} \\
\redrule{
\tcol{\cast{\stalkCIC{i}{h}}{X \Leftarrow \?_{\square_i}}{t}}
\tcol{\ascdom{t}{\stalkCIC{i}{h}}{X}}
}[Up-Down] \label{redrule:up-down}
\hfill \text{when $\tcol{\stalkCIC{i}{h}} \neq \tcol{\err_{[]_i}}$} \\
\redrule{
\tcol{\ascdom{t}{A}{\?_{\square_i}}}
\tcol{\err_{\?_{\square_i}}}
}[Size-Err] \label{redrule:size-err}
\hfill \text{when $\min \{j \mathop{|} \exists h \in \H, \tcol{\stalkCIC{j}{h}} = A\} > i$}
\end{mathpar}
\caption{\CCIC: Reduction rules (extending \cref{fig:bidir},
congruence rules omitted)}
\label{fig:CCIC-reduction}

\end{figure}

The design of the reduction rules is mostly dictated by the discrete
and monotone models of \CCIC presented later
Nevertheless, we now provide some intuition about their meaning.
Let us start with rules \nameref{redrule:prod-unk}, \nameref{redrule:prod-err}, \nameref{redrule:match-unk} and \nameref{redrule:match-err}. These rules specify the exception-like propagation behavior of both $$
and $$ at product and inductive types.
Rules \nameref{redrule:ind-unk} and \nameref{redrule:ind-err}
similarly propagate $$ and $$ when cast between the same inductive
type, and rules \nameref{redrule:down-unk} and \nameref{redrule:down-err} do the same
from the unknown type to any type $X$.

Next are rules \nameref{redrule:prod-prod}, \nameref{redrule:ind-ind} and \nameref{redrule:univ-univ},
which correspond to success cases of dynamic checks, where the cast is between types with the same head.
In that case, casts are either completely
erased when possible, or propagated. As usual in gradual typing, directly inspired by higher-order contracts~\cite{findlerFelleisen:icfp2002}, \nameref{redrule:prod-prod} distributes the function cast in two casts, one for the argument and one for the body; note the substitution in the source codomain in order to account for dependency.
Also, because constructors and inductives are fully-applied,
this \nameref{redrule:prod-prod} rule cannot be blocked on a partially-applied constructor or inductive.
Regarding inductive types, the restriction to reduce only on constructors means that a cast between $$ and $$ is blocked until its argument term is a constructor, rather than disappearing right away as for the universe.
We follow this somewhat non-optimal strategy to be consistent
between inductive types, because for more complex inductive types such as lists, the propagation of casts on subterms cannot be avoided.

On the contrary, rule \nameref{redrule:head-err} specifies failure of a dynamic check when the considered types have different heads. Similarly, rules \nameref{redrule:err-dom}, \nameref{redrule:err-codom} specify that cast to or from the error type is always an error.

Finally, there are specific rules pertaining to casts to and from $$, showcasing its behaviour as a universal type. Rules \nameref{redrule:prod-germ} and \nameref{redrule:ind-germ} decompose an upcast into $$ as an upcast to a germ followed by an upcast from the germ to $$. This decomposition of an upcast to $$ into a series of "atomic" upcasts from a germ to $$ is a consequence of the way the cast operation is implemented in \cref{sec:realizing-ccic}, but similar decompositions appear e.g. in \citet{siekAl:snapl2015}, where the equivalent of our germs are called ground types.
The side conditions guarantee that this rule is used when no other applies.
Rule \nameref{redrule:up-down} erases the succession of an upcast to $$ and a downcast from it. Note that in this rule the upcast $thi_[]_i$ works like a constructor for $_[]_i$ and $_[]_iX$ as a destructor---a view reflected by the canonical and neutral forms of \cref{fig:CCIC-canonical} for $_[]$.%
\footnote{
In a simply-typed language such as GTLC~\cite{siekAl:snapl2015},
where there are no neutrals at the type level,
casts from a germ/ground type
to the unknown type are usually interpreted as tagged values~\cite{siekTaha:sfp2006}.
Here, these correspond exactly to the canonical forms of $\tcol{\?_{[]}}$, but we also have to account for the many neutral forms that appear in open contexts.
Finally, rule \nameref{redrule:size-err} corresponds to a peculiar kind of error, which only happens due to the presence of a type hierarchy:
$?_[]_i$ is only universal with respect to types at level $i$, and so a type might
be of a level too high to fit into it. To detect such a case, we check whether $A$ is a germ for a level that is below $i$, and when not throw an error.

\paragraph{Meta-Theoretical Properties}
The typing and reduction rules just given ensure two of the
meta-theoretical properties introduced in \cref{sec:tradeoffs}:
\psafe for the three variants of \CCIC, as well as \pnorm for \CCICT and
\CCICs.
Before turning to these properties, let us establish a crucial lemma, namely the
confluence of the rewriting system induced by reduction.
\begin{lemma}[Confluence of \CCIC]
\label{lem:confluence}
If $\tcol{t}$ and $\tcol{u}$ are related by the symmetric, reflexive, transitive closure
of $\redCCIC$, then there exists $s$ such that $\tcol{t} \rtred \tcol{s}$ and $\tcol{u} \rtred \tcol{s}$.
\end{lemma}

\begin{proof}
We extend the notion of parallel reduction ($\paraRed$) for \CIC
from~\cite{SozeauBFTW20} to account for our additional reduction
rules and show that the triangle property---the existence, for any
term $t$, of an optimal reduced term $\tcol{\optRed{t}}$ in one step (\cref{fig:triangle})---still
holds. From the triangle property, it is
easy to deduce confluence of parallel reduction in one step
(\cref{fig:triangle-confluence}), which implies confluence
because parallel reduction is between one-step reduction and
iterated reductions.
This proof method is basically an extension of the Tait-Martin Löf criterion on
parallel reduction~\citep{barendregt:84,TAKAHASHI1995120}.
\begin{figure}
\begin{subfigure}[b]{.4\textwidth}
\xymatrix{\tcol{t} \ar@3{->}[d] \ar@3{->}[rd] & \\
\tcol{u} \ar@3{->}[r] & \tcol{\optRed{t}}}
\caption{The triangle property.}
\label{fig:triangle}
\end{subfigure}
\begin{subfigure}[b]{.5\textwidth}
<EMAIL_ADDRESS>\tcol{t} \ar@3{->}[ld] \ar@3{->}[dd] \ar@3{->}[rd] &  \\
\tcol{u} \ar@3{->}[rd] & &  \tcol{u'} \ar@3{->}[ld] \\
& \tcol{\optRed{t}}& }
\caption{The triangle property implies confluence.}
\label{fig:triangle-confluence}
\end{subfigure}
\caption{Representation of the triangle property (left) and its
consequence on confluence (right).}
\end{figure}
\end{proof}

Let us now turn to \psafe, which we prove using the standard
progress and subject reduction properties~\cite{wrightFelleisen1994}.
Progress describes a set of canonical forms, asserting that all terms that do not belong to
such canonical forms are not in normal form, \ie can take at least
one reduction step. \cref{fig:CCIC-canonical} provides the definition
of canonical forms, considering head reduction.

As standard in dependent type theories,
we distinguish between canonical forms and neutral
terms. Neutral terms
correspond to (blocked) destructors, waiting for a substitution to
happen, while other canonical forms correspond to constructors.
Additionally, the notion of neutral terms naturally induces a weak-head
reduction strategy that consists in either applying a top-level
reduction or reducing the (only) argument of the
top-level destructor that is in a neutral position.

The canonical forms for plain \CIC are given by the first three lines of \cref{fig:CCIC-canonical}.
The added rules deal with
errors, unknown terms and casts.
First, an error $_t$ or an unknown term $_t$ is neutral when
$t$ is neutral, and is canonical only when $t$ is $[]$ or $I(a)$,
but not a $Π$-type. This is because exception-like terms reduce on
Second, there is an additional specific form of canonical
inhabitants of $_[]$: these are upcasts from a germ, which can be
seen as a term tagged with the head constructor of its type, in a
matter reminiscent of actual implementations of dynamic typing using
type tags. As we explained when presenting \cref{fig:CCIC-reduction},
these canonical forms work as constructors for $_[]$.
Finally, the cast operation behaves as a destructor on the
universe $[]$---as if it were an inductive type of usual \CIC.
This destructor first scrutinizes the source type of
the cast. This is why the cast is neutral as soon as its source type
is neutral. When the source type reduces to a head constructor, there are two
possibilities. Either that constructor is $_[]$, in which case the cast
scrutinizes its argument to be a canonical form $t_[]ih$ and is neutral when this is not the case.
In all other cases, it first scrutinizes the target type, so the cast is neutral when the target type is neutral.
Finally, when both types have head constructors, the cast
might still need its argument to be either a $λ$-abstraction or an inductive
constructor to reduce.

\begin{figure}
\begin{small}
\boxedrule{$\can{\tcol{t}}, \neu{\tcol{t}}$}\\
\begin{mathpar}
\inferrule{ }{\can{\tcol{\l x : A . t}}} \and
\inferrule{ }{\can{\tcol{c(\orr{a},\orr{b})}}} \and
\inferrule{ }{\can{\tcol{\P x : A . B}}} \\
\inferrule{ }{\can{\tcol{[]}}} \and
\inferrule{ }{\can{\tcol{I(\orr{a})}}} \and
\inferrule{\neu{\tcol{t}}}{\can{\tcol{t}}} \\
\inferrule{ }{\neu{\tcol{x}}} \and
\inferrule{\neu{\tcol{t}}}{\neu{\tcol{t~u}}} \and
\inferrule{\neu{\tcol{t}}}{\neu{\tcol{\match{I}{t}{z.P}{\orr{f.y.b}}}}} \\
\inferrule{ \tcol{T} \in \{ ~\tcol{[]},\tcol{I(\orr{a})}, \tcol{\?_{[]}}, \tcol{\err_{[]}}~\} }{\can{\tcol{\?_{T}}}} \and
\inferrule{\neu{\tcol{t}}}{\neu{\tcol{\?_{t}}}} \and %\\
\inferrule{ \tcol{T} \in \{ ~\tcol{[]},\tcol{I(\orr{a})}, \tcol{\?_{[]}}, \tcol{\err_{[]}}~\} }{\can{\tcol{\err_{T}}}} \and
\inferrule{\neu{\tcol{t}}}{\neu{\tcol{\err_{t}}}} \\
\inferrule{ }{\can{\tcol{\cast{\stalkCIC{i}{h}}{\?_{[]_i}}{t}}}} \and
\inferrule{\neu{\tcol{S}}}{\neu{\tcol{\cast{S}{T}{t}}}} \and
\inferrule{\neu{\tcol{t}}}{\neu{\tcol{\cast{\?_{[]}}{T}{t}}}} \\
\inferrule{\neu{\tcol{T}}}{\neu{\tcol{\cast{[]}{T}{t}}}} \and
\inferrule{\neu{\tcol{T}}}{\neu{\tcol{\cast{\P x : A. B}{T}{t}}}} \and
\inferrule{\neu{\tcol{t}}}{\neu{\tcol{\cast{\P x : A. B}{\P x : A'. B'}{t}}}} \and
\inferrule{\neu{\tcol{T}}}{\neu{\tcol{\cast{I(\orr{a})}{T}{t}}}} \and
\inferrule{\neu{\tcol{t}}}{\neu{\tcol{\cast{I(\orr{a})}{I(\orr{a'})}{t}}}} \and
\end{mathpar}
\end{small}
\caption{Head neutral and canonical forms for \CCIC}
\label{fig:CCIC-canonical}
\end{figure}

Equipped with the notion of canonical forms, we can state \psafe for \CCIC:

\begin{theorem}[Safety of the three variants of \CCIC (\psafe)]
\label{thm:ccic-psafe}
\CCIC enjoys:
\begin{description}
\item[Progress:]
if $\tcol{t}$ is a well-typed term of \CCIC, then either $\can{\tcol{t}}$ or there is some $\tcol{t'}$ such that $\tcol{t} \redCCIC \tcol{t'}$.
\item[Subject reduction:] if $\tcol{\Gamma} \caty \tcol{t} \inferty \tcol{A}$ and $\tcol{t} \redCCIC{} \tcol{t'}$ then $\tcol{\Gamma} \caty \tcol{t'} \checkty \tcol{A}$.
\end{description}
Thus \CCIC enjoys \psafe.
\end{theorem}
\begin{proof}

\begin{description}
\item[Progress:]
The proof is by induction on the typing derivation of $\tcol{t}$.
As standard, we show that in all cases,
either a reduction on a subterm happens, $\tcol{t}$ itself reduces
because some canonical form was not neutral and creates a redex, or $\tcol{t}$ is neutral.

\item[Subject reduction:]
Subject reduction can be derived from the injectivity of type
constructors, which is a direct consequence of confluence. See
\cite{SozeauBFTW20} for a detailed account of this result in the
simpler setting of \CIC.
\end{description}
\end{proof}

We now establish normalization of \CCICT and \CCICs, although the proof below
relies on the discrete model defined in \cref{sec:bare-model}.

\begin{theorem}[Normalization of \CCICT and \CCICs (\pnorm)]
\label{thm:ccic-pnorm}
Every reduction path for a well-typed term in \CCICT or \CCICs is finite.
\end{theorem}

\begin{proof}
The translation induced by the discrete model presented
in~\cref{sec:bare-model} maps each reduction step to at least one
step (\cref{thm:discrete-model}). So strong normalization holds
because the target calculus of the translation is normalizing.
\end{proof}

\subsection{Elaboration from \GCIC to \CCIC}
\label{sec:elaboration}
Now that \CCIC has been described, we move on to \GCIC. The typing judgment of \GCIC is {\em defined} by an elaboration judgment from \GCIC to \CCIC, based upon \cref{fig:bidir}, augmenting all judgments with an extra output: the elaborated \CCIC term. This definition of typing using elaboration is required because of the intricate interdependency between typing and reduction exposed in \cref{sec:gcic-overview}.

\paragraph{Syntax}
\label{gcic-syntax}
The syntax of \GCIC\footnote{We use \sourcecolor{green} for terms of
\GCIC. To maintain a distinction in the absence of colors, we also
use tildes ($\sourcecolor{\tilde{t}}$) for terms in \GCIC in expressions mixing both source and target terms.} extends that of \CIC
with a single new term constructor $i$, where $i$ is a universe level. From a user perspective, one is not given direct access to the failure and cast primitives, those only arise through uses of $$.

\paragraph{Consistent conversion}

\begin{figure}
\begin{small}
\boxedrule{$\tcol{t} \acons \tcol{t}$}
\begin{mathpar}
\inferrule{ }{\tcol{x} \acons \tcol{x}} \and
\inferrule{ }{\tcol{\square{}_{i}} \acons \tcol{\square{}_{i}}} \and
\inferrule{\tcol{A} \acons \tcol{A'} \\ \tcol{t} \acons \tcol{t'}}
{\tcol{\l x : A . t} \acons \tcol{\l x : A' . t'}} \and
\inferrule{\tcol{A} \acons \tcol{A'} \\ \tcol{B} \acons \tcol{B'}}
{\tcol{\P x : A . B} \acons \tcol{\P x : A'.B'}} \and
\inferrule{\tcol{t} \acons \tcol{t'} \\ \tcol{u} \acons \tcol{u'}}{\tcol{t~u} \acons \tcol{t'~u'}} \and
\inferrule{\tcol{\orr{a}} \acons \tcol{\orr{a'}}}{\tcol{I(\orr{a})} \acons \tcol{I(\orr{a'})}} \and
\inferrule{\tcol{\orr{a}} \acons \tcol{\orr{a'}} \\ \tcol{\orr{b}} \acons \tcol{\orr{b'}}}
{\tcol{c_k(\orr{a},\orr{b})} \acons \tcol{c_k(\orr{a'},\orr{b'})}} \and
\inferrule{\tcol{s} \acons \tcol{s'} \\ \tcol{P} \acons \tcol{P'} \\ \tcol{\orr{t}} \acons \tcol{\orr{t'}}}
{\tcol{\match{I}{s}{z.P}{f.\orr{y.t}}} \acons \tcol{\match{I}{s'}{z.P'}{f.\orr{y.t'}}}} \\
\inferrule{\tcol{t} \acons \tcol{t'}}
{\tcol{t} \acons \tcol{\cast{A'}{B'}{t'}}} \and
\inferrule{\tcol{t} \acons \tcol{t'}}
{\tcol{\cast{A}{B}{t}} \acons \tcol{t'} } \and
\inferrule{ }{\tcol{t} \acons \tcol{\?_{T'}}} \and
\inferrule{ }{\tcol{\?_T} \acons \tcol{t}}
\end{mathpar}
\end{small}
\caption{\CCIC: $\alpha$-consistency}
\label{fig:acons}
\end{figure}

Before we can describe typing, we should focus on conversion. Indeed, to account for the imprecision introduced by $$, elaboration employs {\em consistent conversion} to compare \CCIC terms rather than usual conversion relation.

\begin{definition}[Consistent conversion]
\label{def:cons}
Two \CCIC terms are \emph{$\alpha$-consistent}, written $\acons$, if they are in the relation defined by the inductive rules of \cref{fig:acons}.

Two terms are \emph{consistently convertible}, or simply \emph{consistent}, noted $\tcol{s} \cons \tcol{t}$, if and only if there exists $\tcol{s'}$ and $\tcol{t'}$ such that $\tcol{s} \rtred \tcol{s'}$, $\tcol{t} \rtred \tcol{t'}$ and $\tcol{s'} \acons \tcol{t'}$.
\end{definition}

Thus $α$-consistency is an extension of $α$-equality that takes imprecision into account. Apart from the standard rules making $$ consistent with any term, $α$-consistency optimistically ignores casts, and does not consider errors to be consistent with themselves.
The first point is to prevent casts inserted by the elaboration from disrupting valid conversions, typically between static terms. The second is guided by the idea that if errors are encountered at elaboration already, the term cannot be well behaved, so it must be rejected as early as possible and we should avoid typing it.
The consistency relation is then built upon $α$-consistency in a way totally similar to how conversion in \cref{fig:bidir,fig:CCIC-reduction} is built upon $α$-equality. Also note that this formulation of consistent conversion makes no assumption of
normalization, and is therefore usable as such in the non-normalizing \GCICP.

An important property of consistent conversion,
and a necessary condition for the conservativity of \GCIC with respect to\ \CIC (\pconst{\CIC}),
is that it corresponds to conversion on static terms.

\begin{proposition}[Properties of consistent conversion]~
\label{prop:cons-static}
\begin{enumerate}
\item Two static terms are consistently convertible if and only if they are convertible in \CIC.
\item If $\tcol{s}$ and $\tcol{t}$ have a normal form, then $\tcol{s} \cons \tcol{t}$ is decidable.
\end{enumerate}
\end{proposition}

\begin{proof}
\emph{(1)} First remark that $\alpha$-consistency between static terms corresponds to $\alpha$-equality of terms. Thus, and because the reduction of static terms in \CCIC is the same as the reduction of \CIC, two consistent static terms must reduce to $\alpha$-equal terms, which in turn implies that they are convertible.
Conversely two convertible terms of \CIC have a common reduct,
which is $\alpha$-consistent with itself. % making the two terms consistent.

\emph{(2)} If $\tcol{s}$ and $\tcol{t}$ are normalizing, they have a finite number
of reducts, thus to decide their consistency it is sufficient to check each pair of reducts for the decidable
$\alpha$-consistency. Comparing normal forms is not enough, because a term $\tcol{t}$might be stuck because of a cast while another one $\tcol{s}$ can be $\alpha$-consistent with it and reduce further, so that the normal form of $\tcol{t}$ and $\tcol{s}$ are not $\alpha$-consistent while $\tcol{t}$ and $\tcol{s}$ are consistent.
\end{proof}

\paragraph{Elaboration}

\begin{figure}
\begin{small}

\boxedrule{$\sinferelab{\Gamma}{t}{T}{\Gamma}{t}{T}$}
\begin{mathpar}
\inferrule{\tcol{(x : T) \in \Gamma}}{\sinferelab{}{x}{}{\Gamma}{x}{T}}[Var] \ilabel{infrule:gcic-var} \and
\inferrule{ }{\sinferelab{}{\square{}_{i}}{}{\Gamma}{\square{}_{i}}{\square{}_{i+1}}}[Univ] \ilabel{infrule:gcic-univ} \\

\inferrule{
\spcheckelab{\square{}}{}{\tilde{A}}{}{\Gamma}{A}{\square{}_i} \\
\spcheckelab{\square{}}{}{\tilde{B}}{\square{}_{j}}{\Gamma, x : A}{B}{\square{}_j}}
{\sinferelab{}{ \P x : \tilde{A} . \tilde{B}}{}{\Gamma}{\P x : A.B}{\square{}_{\sortOfPi{i}{j}}}}[Prod] \ilabel{infrule:gcic-prod} \and
\inferrule{
\spcheckelab{\square{}}{}{\tilde{A}}{}{\Gamma}{A}{\square{}_i} \\
\sinferelab{}{\tilde{t}}{}{\Gamma, x : A}{t}{B}}
{\sinferelab{}{\l x : \tilde{A} . \tilde{t}}{}{\Gamma}{\l x : A. t}{ \P x : A . B}}[Abs] \ilabel{infrule:gcic-abs} \and
\inferrule{
\spcheckelab{\Pi}{}{\tilde{t}}{}{\Gamma}{t}{\P x : A . B} \\
\scheckelab{}{\tilde{u}}{}{\Gamma}{u}{A}}
{\sinferelab{}{\tilde{t}~\tilde{u}}{}{\Gamma}{t~u}{B\subs{u}{x}}}[App] \ilabel{infrule:gcic-app}

\inferrule{ }
{\sinferelab{}{\?\ulev{i}}{}{\Gamma}{\?_{\?_{[]_i}}}{\?_{[]_i}}}[Unk] \ilabel{infrule:gcic-unk}

\\
\inferrule{\scheckelab{}{\tilde{a}_k}{}{\Gamma}{a_k}{\pars_k(I,i)\parsub{\orr{a}}}}
{\sinferelab{}{I\ulev{i}(\orr{\tilde{a}})}{}{\Gamma}{I\ulev{i}(\orr{a})}{[]_i}}[Ind] \ilabel{infrule:gcic-ind}
\and
\inferrule{
\scheckelab{}{\tilde{a}_k}{}{\Gamma}{a_k}{\pars_k(I,i)\parsub{\orr{a}}} \\
\scheckelab{}{\tilde{b}_m}{}{\Gamma}{b_m}{\args_m(I,i,c)\parsub{\orr{a},\orr{b}}}}
{\sinferelab{}{c_k\ulev{i}(\orr{\tilde{a}},\orr{\tilde{b}})}{}{\Gamma}{c(\orr{a},\orr{b})}{I(\orr{a})}}[Cons] \ilabel{infrule:gcic-cons} \\
\inferrule{
\spcheckelab{I}{}{\tilde{s}}{}{\Gamma}{s}{I(\orr{a})} \\
\spcheckelab{\square{}}{}{\tilde{P}}{}{\Gamma, z : I(\orr{a})}{P}{\square{}_i} \\\\
\scheckelab{}{\tilde{t}_k}{}{\Gamma, f : (\P z : I(\orr{a}), P), \orr{y} : \args(I,i,c_k)\parsub{\orr{a},\orr{y}}}{t_k}{P\subs{c_k(\orr{a},\orr{y})}{z}}
\sinferelab{}{\match{I}{\tilde{s}}{z.\tilde{P}}{f.\orr{y.\tilde{t}}}}{}{\Gamma}{\match{I}{s}{z.P}{\orr{f.y.t}}}{P\subs{s}{z}}}[Fix]
\ilabel{infrule:gcic-fix}
\end{mathpar}

\boxedrule{$\scheckelab{\Gamma}{t}{T}{\Gamma}{t}{T}$}
\begin{mathpar}
\inferrule{
\sinferelab{}{\tilde{t}}{}{\Gamma}{t}{T} \\ \targetcolor{T \cons S}}
{\scheckelab{}{\tilde{t}}{}{\Gamma}{\cast{T}{S}{t}}{S}}[Check] \ilabel{infrule:gcic-check}
\end{mathpar}

\boxedrule{$\spcheckelab{\bullet}{\Gamma}{t}{T}{\Gamma}{t}{T}$} \vspace{1em}
\begin{mathpar}
\inferrule{
\sinferelab{}{\tilde{t}}{}{\Gamma}{t}{T} \\ \targetcolor{T \rtred \square{}_{i}}}
{\spcheckelab{\square{}}{}{\tilde{t}}{}{\Gamma}{t}{\square{}_{i}}}[Inf-Unk] \ilabel{infrule:gcic-inf-univ} \and
\inferrule{
\sinferelab{}{\tilde{t}}{}{\Gamma}{t}{T} \\ \targetcolor{T \rtred \?_{[]_{i+1}}}}
{\spcheckelab{\square}{}{\tilde{t}}{}{\Gamma}{\cast{T}{[]_i}{t}}{[]_i}}[Inf-Univ?] \ilabel{infrule:gcic-univ-unk} \\
\inferrule{
\sinferelab{}{\tilde{t}}{}{\Gamma}{t}{T} \\ \targetcolor{T \rtred \P x : A. B}}
{\spcheckelab{\Pi}{}{\tilde{t}}{}{\Gamma}{t}{\P x : A. B}}[Inf-Prod] \ilabel{infrule:gcic-inf-prod} \and
\inferrule{
\sinferelab{}{\tilde{t}}{}{\Gamma}{t}{T} \\ \targetcolor{T \rtred \?_{[]_i}} \\ \castOfPi{i} \geq 0}
{\spcheckelab{\Pi}{}{\tilde{t}}{}{\Gamma}{\cast{T}{\stalkCIC{i}{\Pi}}{t}}{\stalkCIC{i}{\Pi}}}[Inf-Prod?] \ilabel{infrule:gcic-prod-unk} \\
\inferrule{\sinferelab{}{\tilde{t}}{}{\Gamma}{t}{T} \\ \targetcolor{T \rtred I(\orr{a})}}
{\spcheckelab{I}{}{\tilde{t}}{}{\Gamma}{t}{I(\orr{a})}}[Inf-Ind] \ilabel{infrule:gcic-inf-ind} \and
\inferrule{
\sinferelab{}{\tilde{t}}{}{\Gamma}{t}{T} \\ \targetcolor{T \rtred \?_{[]_i}}}
{\spcheckelab{I}{}{\tilde{t}}{}{\Gamma}{\cast{T}{\stalkCIC{i}{I}}{t}}{\stalkCIC{i}{I}}}[Inf-Ind?] \ilabel{infrule:gcic-ind-unk}
\end{mathpar}
\end{small}
\caption{Type-directed elaboration from \GCIC to \CCIC}
\label{fig:elaboration}
\end{figure}

Elaboration from \GCIC to \CCIC is given in \cref{fig:elaboration}, closely following the bidirectional presentation of \CIC (\cref{fig:bidir}) for most rules, simply carrying around the extra elaborated terms. Note that only the subject of the judgment is a \sourcecolor{source term} in \GCIC;
other inputs (that have already been elaborated), as well as outputs (that are to be constructed), are \targetcolor{target terms} in \CCIC. Let us comment a bit on the specific modifications and additions compared to \cref{fig:bidir}.

The most salient feature of elaboration is the insertion of casts that mediate
between merely consistent but not convertible types.
They of course are needed in the rule \nameref{infrule:gcic-check} where the terms are compared using consistency. But this is not enough: casts also appear in the newly-introduced rules \nameref{infrule:gcic-univ-unk} \nameref{infrule:gcic-prod-unk} and \nameref{infrule:gcic-ind-unk} for constrained inference, where the type $?_[]_i$ is replaced by the least precise type of the appropriate universe level
having the constrained head constructor, which is exactly what the $$ function gives us. Note that in the case of \nameref{infrule:gcic-univ-unk} we could have replaced $[]_i$ with $i+1[]_i$ to make for a presentation similar to the other two rules. The role of these three rules is to ensure that a term of type $_[]_i$ can be used as a function, or as a scrutinee of a match, by giving a way to derive constrained inference for such a term.

It is interesting to observe that the rules for constrained elaboration in a gradual setting bear a close resemblance with those described by \citet[Section 3.3]{ciminiSiek:popl2016}, where a matching operator is introduced to verify that an output type can fit into a certain type constructor---either by having that type constructor as head symbol or by virtue of being $$. Such a form of matching was already present in our static, bidirectional system, because of the presence of reduction in types. In a way, both \citet{ciminiSiek:popl2016} and \citet{LennonBertrand2021} have the same need of separating the inferred type from operations on it to recover its head constructor, and our mixing of both computation and gradual typing makes that need even clearer.

Rule \nameref{infrule:gcic-unk} also deserves some explanation: $i$ is elaborated to
$__[]_i$, the least precise term of the least precise type of the whole universe $[]_i$. This avoids unneeded type annotations on $$ in \GCIC. Instead, the context is responsible for
inserting the appropriate cast, \eg $T$ elaborates to a term reducing to $_T$.
We do not drop annotations altogether because of an important property on which
bidirectional \CIC is built: any well-formed term should \emph{infer} a type, not just check.
Thus, we must be able to infer a type for $$. The obvious choice is to have $$ infer $$, but this $$ is a term of \CCIC, and thus needs a type index.
Because this $$ is used as a type, this index must be $[]$, and the universe level of the source $$ is there to give us the level of this $[]$.
In a real system, this should be handled by \emph{typical ambiguity},\footnote{Typical ambiguity~\cite{Harper1991} is the possibility to avoid giving explicit
universe levels, letting the system decide whether a consistent assignment
of levels can be found. In \Coq, for instance, one almost never has to be explicit about universe levels when writing \texttt{Type}.\label{note:typ-amb}}
alleviating the user from the need to give any annotations when using $$.

\paragraph{Direct properties}

As the elaboration rules are completely syntax-directed, they
immediately translate to
an algorithm for elaboration. Coupled with decidability of consistency (\cref{prop:cons-static}),
this makes elaboration decidable whenever $$ is normalizing;
when $$ is not normalizing, the elaboration algorithm might diverge, resulting in only semi-decidability of typing (as in, for instance, Dependent Haskell~\cite{eisenberg2016dependent}).

\begin{theorem}[Decidability of elaboration]
\label{thm:decidability}
The relations of inference, checking and partial inference of \cref{fig:elaboration} are decidable in \GCICT and \GCICs. They are semi-decidable in \GCICP.
\end{theorem}

Let us now establish two important properties of elaboration that we can
prove at this stage: elaboration is {\em correct}, insofar as it produces well-typed
\CCIC terms, and functional, in the sense that a given \GCIC term can
be elaborated to at most one \CCIC term up to conversion.

\begin{theorem}[Correctness of elaboration]
\label{thm:correction}
The elaboration produces well-typed terms in a well-formed context. Namely, given $\tcol{\Gamma}$ such that $\caty \tcol{\Gamma}$, we have that:
\begin{itemize}
\item if $\inferelab{}{\tilde{t}}{}{\Gamma}{t}{T}$, then $\tcol{\Gamma} \caty \tcol{t} \inferty \tcol{T}$;
\item if $\pcheckelab{\bullet}{}{\tilde{t}}{}{\Gamma}{t}{T}$ then $\tcol{\Gamma} \caty \tcol{t} \pcheckty{\bullet} \tcol{T}$ (with $\bullet$ denoting
the same index in both derivations);
\item if $\checkelab{}{\tilde{t}}{}{\Gamma}{t}{T}$ and $\tcol{\Gamma} \caty \tcol{T} \pcheckty{[]} \tcol{[]_i}$, then $\tcol{\Gamma} \caty \tcol{t} \checkty \tcol{T}$.
\end{itemize}
\end{theorem}

\begin{proof}
The proof is by induction on the elaboration derivation,
mutually with similar properties for all typing judgments.
In particular, for checking, we have an extra hypothesis that the
given type is well-formed, as it is an input that should already
have been typed.

Because the bidirectional typing rules of \CIC are very similar to the \GCIC-to-\CCIC elaboration rules, the induction is mostly routine. Let us point however that the careful design of the bidirectional rules already in \CIC regarding the input/output separation is important here. Indeed, we have that inputs to the successive premises of a rule are always well-formed, either as inputs to the conclusion, or thanks to previous premises. In particular, all context extensions
are valid, \ie $\tcol{\Gamma, x : A}$ is used only when $\tcol{\Gamma} \vdash \tcol{A} \pcheckty{[]} \tcol{[]_i}$, and similarly only well-formed types are used for checking. This ensures that we can always use the induction hypothesis.

The only novel points to consider are the rules where a cast is inserted. For these, we rely on the validity property (an inferred type is always well-typed itself) to ensure that the domain of inserted casts is well-typed, and thus that the casts can be typed.
\end{proof}

Because of the absence of a fixed, deterministic reduction strategy, the elaborated term is not unique. Indeed, since a type can be reduced to multiple product types in rule \cref{infrule:gcic-prod}, a term can infer multiple, different types, and since those appear later on in casts, the elaborated terms can differ by having different, albeit convertible, types in their casts. We thus state two theorems: one is uniqueness up to conversion, in case full reduction is used. The second is a strengthening if a weak-head reduction strategy is imposed for reduction.

\begin{theorem}[Uniqueness of elaboration---Full reduction]
\label{thm:uniqueness}
Elaborated terms are convertible:
\begin{itemize}
\item if $\inferelab{}{\tilde{t}}{}{\Gamma}{t}{T}$ and $\inferelab{}{\tilde{t}}{}{\Gamma}{t'}{T'}$, then $\tcol{t} \conv \tcol{t'}$ and $\tcol{T} \conv \tcol{T'}$;
\item if $\pcheckelab{\bullet}{}{\tilde{t}}{}{\Gamma}{t}{T}$ and $\pcheckelab{\bullet}{}{\tilde{t}}{}{\Gamma}{t'}{T'}$ then $\tcol{t} \conv \tcol{t'}$ and $\tcol{T} \conv \tcol{T'}$;
\item if $\checkelab{}{\tilde{t}}{}{\Gamma}{t}{T}$ and $\checkelab{}{\tilde{t}}{}{\Gamma}{t'}{T}$ then $\tcol{t} \conv \tcol{t'}$.
\end{itemize}
\end{theorem}
\noindent
(Recall that conversion $$ in \CCIC is defined (similarly as in \CIC) as the existence of $α$-equal reducts for the reduction given in \cref{fig:CCIC-reduction}.)

\begin{theorem}[Uniqueness of elaboration---Weak-head reduction]
\label{thm:uniqueness-wh}
If in \cref{fig:elaboration}, $\rtred$ is replaced by weak-head reduction, then elaborated terms are unique:
\begin{itemize}
\item given $\tcol{\Gamma}$ and $\scol{\tilde{t}}$, there is at most one $\tcol{t}$ and one $\tcol{T}$ such that $\inferelab{}{\tilde{t}}{}{\Gamma}{t}{T}$;
\item given $\tcol{\Gamma}$ and $\scol{\tilde{t}}$, there is at most one $\tcol{t}$ and one $\tcol{T}$ such that $\pcheckelab{\bullet}{}{\tilde{t}}{}{\Gamma}{t}{T}$;
\item given $\tcol{\Gamma}$, $\scol{\tilde{t}}$ and $\tcol{T}$, there is at most one $\tcol{t}$ such that $\checkelab{}{\tilde{t}}{}{\Gamma}{t}{T}$.
\end{itemize}\end{theorem}

\begin{proof}
Like for \cref{thm:correction}, those are proven mutually by induction on the typing derivation.

The main argument is that there is always at most one rule that can apply to get a typing conclusion for a given term. This is true for all inference statements because there is exactly one inference rule for each term constructor, and for checking because there is only one rule to derive checking. In those cases simply combining the hypothesis of uniqueness is enough.

For $\pcheckty{\Pi}$, by confluence of \CCIC the inferred type cannot at the same time reduce to $\tcol{\?_{\square{}}}$ and $\tcol{\P x : A . B}$, because those do not have a common reduct. Thus, only one of the two rules \nameref{infrule:gcic-inf-prod} and \nameref{infrule:gcic-prod-unk} can apply. It is enough to conclude for \cref{thm:uniqueness}, because reducts of convertible types are still convertible. For \cref{thm:uniqueness-wh} the deterministic reduction strategy ensures that the inferred type is indeed unique, rather than unique up to conversion. The reasoning is similar for the other constrained inference judgments.
\end{proof}

\subsection{Illustration: Back to Omega}
\label{sec:back-to-omega}

Now that \GCIC has been entirely presented, let us come back to the important example of $Ω$, and explain in detail the behavior described in \cref{sec:gcic:-3-1} for the three \GCIC variants.

Recall that $Ω$ is the
term $δ δ$, with $δ := łx : i+1 .
x x$. We leave out the casts present in
\cref{sec:tradeoffs,sec:gcic-overview}, knowing that they will be introduced by
elaboration. We also use $$ at level $i + 1$, because
$i+1$, when elaborated as a type, becomes $T :=
_[]_i+1[]_i__[]_i+1$, such that $T _[]_i$.
For the rest of this section, we write $_j$ instead of $_[]_j$
to avoid stacked indices and ease readability.

If $i = 0$ the elaboration of $δ$ (and thus of $Ω$)
fails in \GCICs and \GCICT,
because the inferred type for $x$ is $T$, which reduces to $_0$.
Then, because $0 = -1 < 0$ in both \GCICs and \GCICT, rule \nameref{infrule:gcic-prod-unk} does not apply and $δ$ is deemed ill-typed, as is $Ω$.

Otherwise, if $i > 0$ or we are considering \GCICP, $δ$ can be elaborated, and we have
\[ \inferelab{}{\delta}{}{\cdot}{\tcol{\l x : T . \left(\cast{T}{\stalkCIC{i}{\Pi}}{x}
\right)~\left(\cast{T}{\?_{\castOfPi{i}}}{x} \right)}}{T \to \?_{\castOfPi{i}}} \]
From this, we get that $Ω$ also elaborates, namely
(with $δ'$ the elaboration of $δ$ above)
\[ \inferelab{}{\Omega}{}{\cdot}{\delta'~\left(\cast{T \to \?_{\castOfPi{i}}}{T}{\delta'}\right)}{\?_{\castOfPi{i}}} \]
Let us now look at the reduction behavior of this elaborated term $Ω'$ in
the three systems: it reduces seamlessly when $i = i$ (\GCICP/\CCICP),
while having $i < i$ makes it fail (\GCICs/\CCICs and \GCICT/\CCICT).
The reduction of $Ω'$ in \CCICP is as follows:
\tcol{\Omega'} & \rtred & \tcol{
\left(\l x : \?_{i} . \left(\cast{T}{\?_i \to \?_i}{x}\right)~\left(\cast{T}{\?_i}{x}\right)\right)~\left(\cast{T \to \?_i}{T}{\delta'}\right)
} \\
& \rtred & \tcol{\left(\l x : \?_{i} . \left(\cast{\?_i}{\?_i \to \?_i}{x}\right)~\left(\cast{\?_i}{\?_i}{x}\right)\right)\left(\cast{\?_i \to \?_i}{\?_i}{\delta'}\right) } \\
& \rtred & \tcol{\left(\cast{\?_i \to \?_i}{\?_i \to \?_i \Leftarrow \?_i}{\delta'}\right)~\left(\cast{\?_i \to \?_i}{\?_i \Leftarrow \?_i}{\delta'}\right)} \\
& \rtred & \tcol{\left(\cast{\?_i \to \?_i}{\?_i \to
\?_i}{\delta'}\right)~\left(\cast{\?_i \to
\?_i}{\?_i}{\delta'}\right)} \\
& \rtred & \tcol{\left(\l x : \?_i . \castbg{pastelgray}{\?_i}{\?_i}{\left(\left(\cast{\?_i}{\?_i \to \?_i}{x}\right)~(\castbg{pastelgray}{\?_i}{\?_i}{x})\right)}\right)~\left(\cast{\?_i \to \?_i}{\?_i}{\delta'}\right)} \\
\end{array}
The first step is the identity, simply replacing $Ω', i$ and the first occurrence of $δ'$ by their definitions.
The second reduces $T$ to $_i$. In the third, the casted $δ'$ is substituted for $x$ by a $β$ step. Casts are finally simplified using \nameref{redrule:up-down} and \nameref{redrule:prod-prod}.
At that point, the reduction has almost looped back to the second step, apart from the casts $pastelgray_i_i$ in the first occurrence of $δ'$, which will simply accumulate through reduction, but without hindering divergence.

On the contrary, the normalizing variants have $i < i$,
and thus share the following reduction path:
\tcol{\Omega'}
&\rtred & \tcol{\left(\cast{\?_i \to \?_{i-1}}{\?_{i-1} \to \?_{i-1} \Leftarrow \?_i}{\delta'}\right)~\left(\castbg{pastelgray}{\?_i \to \?_{i-1}}{\?_{i-1} \Leftarrow \?_i}{\delta'}\right)} \\
&\rtred & \tcol{\left(\cast{\?_i \to \?_{i-1}}{\?_{i-1} \to \?_{i-1} \Leftarrow \?_i}{\delta'}\right)
\left(\cast{\?_i \to \?_{i-1}}{\?_{i-1} \Leftarrow \?_{i-1} \to \?_{i-1}}{\delta'}\right)} \\
&\rtred & \tcol{\left(\cast{\?_i \to \?_{i-1}}{\?_{i-1} \to \?_{i-1} \Leftarrow \?_i}{\delta'}\right)~\err_{\?_{i-1}}} \\
&\rtred & \tcol{\left(\cast{\?_i \to \?_{i-1}}{\?_{i-1} \to \?_{i-1} \Leftarrow \?_{i-1} \to \?_{i-1}}{\delta'}\right)~\err_{\?_{i-1}}} \\
&\rtred & \tcol{\left(\l x : \?_{i-1} . \cast{\?_{i-1}}{\?_{i-1} \Leftarrow \?_{i-1}}{\left(\left(\cast{\?_i}{\?_{i-1} \to \?_{i-1}}{x'}\right)~\left(\cast{\?_i}{\?_{i-1}}{x'}\right)\right)}\right)~\err_{\?_{i-1}}} \\
&& \text{ where $\tcol{x'}$ is $\tcol{\cast{\?_{i-1}}{\?_i \Leftarrow \?_{i-1}}{x}}$} \\
&\rtred & \tcol{\cast{\?_{i-1}}{\?_{i-1} \Leftarrow \?_{i-1}}{(\err_{\?_{i-1} \to \?_{i-1}}~\err_{\?_{i-1}})}} \\
&\rtred & \tcol{\err_{\?_{i-1}}}
\end{array}
The first step corresponds to the first three above, the only difference being the value of $i$. The reductions however differ in the next step because $_i →_i-1 ≠iΠ$, so \nameref{redrule:prod-germ} applies before \nameref{redrule:up-down}.
For the third step, note that $_i-1 →_i-1 = iΠ$,
so that \nameref{redrule:down-err} applies in the rightmost sequence of casts.
The last three steps of reduction then propagate the error by first using \nameref{redrule:prod-germ}, \nameref{redrule:up-down} and \nameref{redrule:prod-prod}, then the $β$ rule, and finally \nameref{redrule:down-err}, \nameref{redrule:prod-err} and a last $β$ step.
At a high-level, the error can be seen as a dynamic universe inconsistency, triggered by the invalid downcast $pastelgray_i_i-1$ highlighted on the first line.

\subsection{Precision is a simulation for reduction}
\label{sec:gcic-simulation}

Establishing the graduality of elaboration---the formulation of
the static gradual guarantee (SGG) in our setting---is no small feat, as it
requires properties about
computations in \CCIC that amount to the {\em dynamic} gradual guarantee (DGG).
Indeed, to handle
the typing rules for checking and constrained inference, it is
necessary to know how consistency and reduction evolve as a type
becomes less precise.
As already explained in \cref{sec:precision-graduality}, we
cannot directly prove graduality for a syntactic notion of
precision. However, we can still show that this relation is a simulation for reduction. While weaker than graduality, this property implies the DGG and suffices to conclude that graduality of elaboration holds.
The purpose of this section is to establish it.
Our proof is partly inspired by the proof of DGG by
\citet{siekAl:snapl2015}.\footnote{
Lemma 7 in \citet{siekAl:snapl2015} is similar to our \cref{thm:simulation}, and \cref{fig:apre-ccic} draws from their Fig. 9, especially for \nameref{infrule:capre-castr} and \nameref{infrule:capre-castl}. Also, while we do not make them explicit here, Lemmas 8, 10 and 11 also appear in our proofs.
We however had to adapt to the much higher complexity of \CIC compared to \STLC.
In particular, the presence of computation in the domain and codomain of casts is quite subtle to tame, as we must in general reduce types in a cast before we can reduce the cast itself.\footnote{
Thus, while \cref{lem:catchup-lambda,lem:catchup-cons} correspond roughly to Lemma 9 in \citet{siekAl:snapl2015}, \cref{lem:catchup-univ,lem:catchup-type} are completely novel.

Technically, we need to distinguish between two notions of precision, one for \GCIC and one for \CCIC:
(i) {\em syntactic precision} on terms in \GCIC, which corresponds to the
usual syntactic precision of gradual typing~\cite{siekAl:snapl2015}, (ii)
{\em structural precision} on terms in \CCIC, which corresponds
to syntactic precision together with a proper account of casts.
In this section, we concentrate on properties of structural precision in \CCIC.
We only state and discuss the various lemmas and
theorems on a high level, and refer the reader to \cref{sec:precision-reduction} for
the detailed proofs.

\paragraph{Structural precision for \CCIC} As emphasized already, the key property we want to establish is that precision is a simulation for reduction,
\ie that less precise terms reduce at least as well as more precise ones. This property guides the quite involved definition we are about to give for structural precision: it is rigid enough to give the induction hypotheses needed to prove simulation, while being lax enough to be a consequence of syntactic precision after elaboration, which is the key point to establish elaboration graduality (\cref{thm:static-graduality}), our equivalent of the static gradual guarantee.

\begin{figure}
\boxedrule{$\tcol{\GG} \vdash \tcol{t} \capre \tcol{t'}$}
\begin{mathpar}
\inferrule{ }{\tcol{\GG} \vdash \tcol{[]_{i}} \capre \tcol{[]_{i}}}[Diag-Univ] \ilabel{infrule:capre-univ} \and
\inferrule{\tcol{\GG} \vdash \tcol{A} \capre \tcol{A'} \\ \tcol{\GG, x : A \mid A'} \vdash \tcol{B} \capre \tcol{B'}}
{\tcol{\GG} \vdash \tcol{\P x : A . B} \capre \tcol{\P x : A'.B'}}[Diag-Prod] \ilabel{infrule:capre-prod} \and
\inferrule{\tcol{\GG} \vdash \tcol{A} \cdpre \tcol{A'} \\ \tcol{\GG, x : A \mid A'} \vdash \tcol{t} \capre \tcol{t'}}
{\tcol{\GG} \vdash \tcol{\l x : A . t} \capre \tcol{\l x : A' . t'}}[Diag-Abs] \ilabel{infrule:capre-abs} \and
\inferrule{\tcol{\GG} \vdash \tcol{t} \capre \tcol{t'} \\ \tcol{\GG} \vdash \tcol{u} \capre \tcol{u'}}
{\tcol{\GG} \vdash \tcol{t~u} \capre
\tcol{t'~u'}}[Diag-App] \ilabel{infrule:capre-app}
\and
\inferrule{ }{\tcol{\GG} \vdash \tcol{x} \capre \tcol{x}}[Diag-Var] \ilabel{infrule:capre-var} \and
\inferrule{\tcol{\GG} \vdash \tcol{A} \capre \tcol{A'} \\ \tcol{\GG} \vdash \tcol{B} \capre \tcol{B'} \\ \tcol{\GG} \vdash \tcol{t} \capre \tcol{t'} }
{\tcol{\GG} \vdash \tcol{\cast{A}{B}{t}} \capre \tcol{\cast{A'}{B'}{t'}}}[Diag-Cast] \ilabel{infrule:capre-diag-cast} \and
\inferrule{\tcol{\GG} \vdash \tcol{\orr{a}} \capre \tcol{\orr{a'}} \\ i = i'}
{\tcol{\GG} \vdash \tcol{I\ulev{i}(\orr{a})} \capre \tcol{I\ulev{i'}(\orr{a'})}}[Diag-Ind] \ilabel{infrule:capre-ind} \and
\inferrule{\tcol{\GG} \vdash \tcol{\orr{a}} \capre \tcol{\orr{a'}} \\ \tcol{\GG} \vdash \tcol{\orr{b}} \capre \tcol{\orr{b'}} \\ i = i'}
{\tcol{\GG} \vdash \tcol{c\ulev{i}(\orr{a},\orr{b})} \capre \tcol{c\ulev{i'}(\orr{a},\orr{b})}}[Diag-Cons] \ilabel{infrule:capre-cons} \and
\inferrule{
\tcol{\GG} \vdash \tcol{s} \capre \tcol{s'} \\
\tcol{\fs{\GG}} \vdash \tcol{s} \pcheckty{I} \tcol{I(\orr{a})} \\
\tcol{\sn{\GG}} \vdash \tcol{s'} \pcheckty{I} \tcol{I(\orr{a'})} \\
\tcol{\GG, z : I(\orr{a}) \mid I(\orr{a'})} \vdash \tcol{P} \capre \tcol{P'} \\
\tcol{\GG, f : (\P z : I(\orr{a}), P) \mid (\P z : I(\orr{a'}), P'), \orr{y} : \orr{Y_k}\subs{\orr{a}}{\orr{x}} \mid \orr{Y_k}\subs{\orr{a'}}{\orr{x}}} \vdash \tcol{t_k} \capre \tcol{t_k'}}
{\tcol{\GG} \vdash \tcol{\match{I}{s}{z.P}{\orr{f.y.t}}} \capre \tcol{\match{I}{s'}{z.P'}{\orr{f.y.t'}}}}[Diag-Fix] \ilabel{infrule:capre-fix} \\
\inferrule{
\tcol{\fs{\GG}} \vdash \tcol{t} \inferty \tcol{T} \\