{'fraction_non_alphanumeric': 0.030718091376302513, 'fraction_numerical': 0.004102032156160121, 'mean_word_length': 4.468480082506123, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 1, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Complete Bidirectional Typing for the Calculus of Inductive Constructions

This article presents a bidirectional type system for the Calculus of Inductive Constructions (CIC). It introduces a novel judgement intermediate between the usual inference and checking, dubbed constrained inference, to handle the presence of computation in types. The key property is the completeness of the system with respect to the usual undirected one, which has been formally proven in Coq as a part of the MetaCoq project. Although it plays a central role in an ongoing completeness proof for a realistic typing algorithm, the interest of bidirectionality is much wider, as it clarifies previous works in the area and gives strong insights and structure when trying to prove properties on CIC or design variations and extensions.


Introduction
In logical programming, a very important information about judgements is the mode of the objects involved, i.e., which ones are considered inputs or outputs. When examining this distinction for a typing judgement Γ ⊢ t : T , both the term t under inspection and the context Γ of this inspection are known, they are thus inputs. The mode of the type T , however, is much less clear: should it be inferred based upon Γ and t, or do we merely want to check whether t conforms to a given T ? Both are sensible approaches, and in fact typing algorithms for complex type systems usually alternate between them during the inspection of a single term/program. The bidirectional approach makes this difference between modes explicit, by decomposing undirected 1 typing Γ ⊢ t : T into two separate judgments Γ ⊢ t ▷ T (inference) and Γ ⊢ t ◁ T (checking) 2 , that differ only by modding. This decomposition allows theoretical work on practical typing algorithms, but also gives a finer grained structure to typing derivations, which can be of purely theoretical interest even without any algorithm in sight.
Although those seem appealing, and despite advocacy by McBride [9,10] to adopt this approach when designing type systems, most of the dependent typing world to this day remains undirected. Some others than McBride's appeal to bidirectionality, starting with Coquand [7] and continuing with Norell [12] or Abel [1]. However, all of these consider unannotated λ-abstractions. This lack of annotations, although sensible for lightness, poses an inherent completeness problem, as a term like (λ x.x) 0 does not type-check against type from Asperti and the Matita team [3], who however concentrate mostly on specific problems pertaining to unification and implementation of the Matita elaborator, without giving a general bidirectional framework. They also do not consider the problem of completeness with respect to a given undirected system, as it would fail in their setting due to the undecidability of higher order unification.
Thus, we wish to fill a gap in the literature, by describing a bidirectional type system that is complete with respect to the (undirected) Calculus of Inductive Constructions (CIC). By completeness, we mean that any term that is typable in the undirected system should also infer a type in the bidirectional one. This feature is very desirable when implementing kernels for proof assistants, whose algorithms should correspond to their undirected specification, never missing any typable term. The bidirectional systems we describe thus forms intermediates between actual algorithms and undirected type systems. This step has proven useful in an ongoing completeness proof of MetaCoq's [17] type-checking algorithm 3 : rather than proving the algorithm complete directly, the idea is to prove it equivalent to the bidirectional type system, separating the implementation problems from the ones regarding the bidirectional structure.
But having a bidirectional type system equivalent to the undirected one has other purely theoretical interests. First, the structure of a bidirectional derivation is more constrained than that of an undirected one, especially regarding the uses of computation. This finer structure can make proofs easier, while the equivalence ensures they can be transported to the undirected world. For instance, in a setting with cumulativity/subtyping, the inferred type for a term t should by construction be smaller than any other types against which t checks. This provides an easy proof of the existence of principal types in the undirected system. The bidirectional structure also provides a better base for extensions. This was actually the starting point for this investigation: in [8], we quickly describe a bidirectional variant of CIC, as the usual undirected CIC is unfit for the gradual extension we envision due to the too high flexibility of a free-standing conversion rule. This is the system we wish to thoroughly describe and investigate here.
Our main technical contributions are twofold. First the identification of a new constrained inference judgement introduced in Section 2 together with general ideas around bidirectional typing in the rather simple setting of pure type systems. Secondly, a formalized proof of equivalence 4 between PCUIC -the extension of CIC nowadays at the heart of Coq -and a bidirectional type system described on a high level in Section 3, built on top of MetaCoq. We next turn to less technical considerations, as we believe that the bidirectional structure is of general interest. Section 4 thus describes the interest of basing an extension of CIC on the bidirectional system directly rather than on the equivalent undirected one. Finally Section 5 investigates in length the related work, and in particular identifies the implicit presence of the bidirectional structure in various earlier articles, showing how making this structure explicit clarifies those.

Undirected CCω
As a starting point, let us consider CCω. It is the backbone of CIC, and we can already illustrate most of our methodology on it. CCω belongs to the wider class of pure type systems (PTS), that has been thoroughly studied and described, see for instance [4]. Since there are many presentational variations, let us first give a precise account of our conventions. Terms in CCω are given by the grammar where the letter x denotes a variable (so will letters y and z), and the letter i is an integer (we will also use letters j, k and l for those). All other Latin letters will be used for terms, with the upper-case ones used to suggest the corresponding terms should be though of as types -although this is not a syntactical separation. We abbreviate Π x : A.B by A → B when B does not depend on x, as is customary. On those terms, reduction → is defined as the least congruence such that (λ x : Conversion ≡ is the symmetric, reflexive, transitive closure of reduction. Finally, contexts are lists of variable declarations x : t and are denoted using capital Greek letters. We write · for the empty list, Γ, x : T for concatenation, and (x : T ) ∈ Γ if (x : T ) appears in Γ. Combining those, we can define typing Γ ⊢ t : T as in Figure 1, where i ∨ j denotes the maximum of i and j. We use well-formed to denote ⊢ Γ for a context, the existence of i such that Γ ⊢ T : □ i for a type T (in an implicit context), or the existence of T such that Γ ⊢ t : T for a term t (again in an implicit context). We also say t is well-typed for the latter. As any PTS, CCω has many desirable properties. We summarize the ones we need here, see [4] for proofs.

23:4
Complete Bidirectional Typing for the Calculus of Inductive Constructions ▶ Proposition 1 (Properties of CCω). The type system CCω as just described enjoys the following properties: Confluence Reduction → is confluent. As a direct consequence, two terms are convertible just when they have a common reduct:

Turning CCω Bidirectional
McBride's discipline. To design our bidirectional type system, we follow a discipline exposed by McBride [9,10]. The central point is to distinguish in a judgment between the subject, whose well-formedness is under scrutiny, from inputs, whose well-formedness is a condition for the judgment to behave well, and outputs, whose well-formedness is a consequence of the judgment. For instance, in inference Γ ⊢ t ▷ T , the subject is t, Γ is an input and T is an output. This means that one should consider whether Γ ⊢ t ▷ T only in cases where ⊢ Γ is already known, and if the judgment is derivable it should be possible to conclude that both t and T are well-formed. All inference rules are to preserve this invariant. This means that inputs to a premise should be well-formed whenever the inputs to the conclusion and outputs and subjects of previous premises are. Similarly the outputs of the conclusion should be well-formed if the inputs of the conclusion and the subjects and outputs of the premises are assumed to be so.
This distinction also applies to the computation-related judgments, although those have no subject. For conversion testing T ≡ T ′ both T and T ′ are inputs, and thus should be known to be well-formed beforehand. For reduction T → * T ′ , T is an input and T ′ is an output, so only T needs to be well-formed, with the subject reduction property of the system ensuring that the output T ′ is also well-formed.
Constrained inference. Beyond the already described inference and checking judgements another one appears in the bidirectional typing rules of Figure 2: constrained inference, written Γ ⊢ t ▷ h T , where h is either Π or □ -and will be extended once we introduce inductive types. Constrained inference is a judgement (or, rather, a family of judgements indexed by h) with the exact same modding as inference, but where the type output is not completely free. Rather, as the name suggests, a constraint is imposed on it, namely that its head constructor can only be the corresponding element of h. This is useful to handle the behaviour absent in simple types that some terms might not have a desired type "on the nose". This is exemplified by the first premise Γ ⊢ t ▷ Π Π x : A.B of the App rule for t u. Indeed, it would be too much to ask t to directly infer a Π-type, as some reduction might be needed on T to uncover this Π. Checking also cannot be used, because the domain and codomain of the tentative Π-type are not known at that point: they are to be inferred from t.

Structural rules.
To transform the rules of Figure 1 to those of Figure 2, we start by recalling that we wish to present a obtain bidirectional typing. Therefore any term should infer a type, and thus all structural rules (i.e. all rules where the subject of the conclusion starts with a term constructor) should give rise to an inference rule. It thus remains to chose the judgements for the premises, which amounts to choosing how to mod them. If a term in a premise appears as input in the conclusion or output of a previous premise, then it can be considered an input, otherwise it must be an output. Moreover, if a type output is unconstrained, then inference can be used, otherwise we must resort to constrained inference. This applies straightforwardly to most rules but the PST-style Abs rule. Indeed, if one looks at the undirected premises, the premise Γ ⊢ Π x : A.B : □ i needs A and B to be known, and only A is known from the conclusion, thus it cannot be the first premise. However, one also cannot put Γ, x : A ⊢ t : B as the first premise, because A is not known to be well-formed at that point, thus Γ, x : A cannot be used as an input. The solution is to split the premise Γ ⊢ Π x : A.B : □ i into the equivalent Γ ⊢ A : □ j and Γ, x : A ⊢ B : □ j ′ . The former can become the first premise, ensuring that type inference for t is done in a well-formed context, and the latter can be simply dropped based upon our invariant that outputs -here the type B inferred for t -can be assumed to be well-formed.
Similarly, as the context is always supposed to be well-formed as an input to the conclusion, it is not useful to re-check it, and thus the premise to Var can be dropped, and undirected rules Var and Weak can be fused into one single Var. This is in line with implementations, where the context is not re-checked at leaves of a derivation tree, with performance issues in mind. The well-formedness invariants ensure that any derivation starting with the empty context will only use well-formed contexts.

Computation rules.
We are now left with the non-structural conversion rule. As we observed, there are two ways to mode computation: if both sides are inputs, conversion can be used, but if only one is known one must resort to conversion, and the other side becomes an output instead. Rule Check corresponds to the first case, while rules Prod-Inf and Sort-Inf both are in the second case. This difference in turn introduces the need to separate between checking, that calls for the first rule, and constrained inference, that requires the others.

23:6 Complete Bidirectional Typing for the Calculus of Inductive Constructions
To the best of our knowledge, this difference in modding of conversion and the resulting introduction of constrained inference have never been described on paper, although they appear in the typing and elaboration algorithms of proof assistants based upon dependent type theory, such as Coq, Lean or Agda. Instead, in presentations in print, constrained inference has been inlined in some way, as is also often the case for checking, so that Γ ⊢ t : T is used where we use Γ ⊢ t ▷ T , the bidirectional structure being left implicit. This is sensible since in Figure 2 there is only one rule to derive checking and constrained inference. However, as soon as typing features appear that complicate conversion, such as unification [3], coercions [3,16] or graduality [8], having singled out those judgements makes the structure clearer and explains the choices made for the modification of typing that could appear ad-hoc otherwise. We come back to this more in length in Section 5.1.

Properties
Let us now state the two main properties relating the bidirectional system to the undirected one: it is both correct (terms typable in the bidirectional system are typable in the undirected system) and complete (all terms typable in the undirected system are also typable in the bidirectional system).

Correctness
A bidirectional derivation can be seen as a refinement of an undirected derivation. Indeed, the bidirectional structure can be erased -replacing each bidirectional rule with the corresponding undirected rule -to obtain an undirected derivation, but for missing sub-derivations, which can be retrieved using the invariants on well-formedness of inputs and outputs. Thus, we get the following correctness theorem -note how McBride's discipline manifests as well-formedness hypothesis on inputs.
▶ Theorem 2 (Correctness of bidirectional typing for CCω). If Γ is well-formed and Proof. The proof is by mutual induction on the bidirectional typing derivation.
Each rule of the bidirectional system can be replaced by the corresponding rule of the undirected system, with all three Check, Prod-Inf and Sort-Inf replaced by Conv, Abs using an extra Prod rule, and Var using a succession of Weak and a final Var. In all cases, the induction hypothesis can be used on sub-derivations of the bidirectional judgment because the context is extended using types that are known to be well-formed, and similarly checking is done against a type that is known to be well-formed by previous premises.
Some sub-derivations of the undirected rules that have no counterpart in the bidirectional ones are however missing. In rules Sort and Var the hypothesis that ⊢ Γ is enough to get the required premise. For rule Check, the well-formedness hypothesis on the type is needed to get the second premise of rule Conv. As for Prod-Inf and Sort-Inf, that second premise is obtained by subject reduction. Finally, the missing premise on the codomain of the product type in rule Abs is obtained by validity of the undirected system, but could be instead handled by strengthening the theorem to incorporate the well-formedness of types when they are outputs.

Completeness
Let us now state the most important property of our bidirectional system: it does not miss any undirected derivation.
Proof. The proof is by induction on the undirected typing derivation.
Rules Sort and Var are base cases, and can be replaced by the corresponding rules in the bidirectional world. Rules Weak and Conv are both direct consequences of the induction hypothesis on their first premise, together with transitivity of conversion for the latter.
For rule Prod, we need the intermediate lemma that if T is a term such that T ≡ □ i , then also T → * □ i . This is a consequence of confluence of reduction. In turn, it implies that if Γ ⊢ t ▷ T and T ≡ □ i then Γ ⊢ t ▷ □ □ i , and is enough to conclude for that rule.
In rule Abs, the induction hypothesis gives Γ ⊢ Π x : A.B ▷ T for some T , and an inversion on this gives Γ ⊢ A ▷ □ □ i for some i. Combined with the second induction hypothesis, it gives We are finally left with the App rule. We know that But by induction hypothesis we also know that Γ ⊢ u ▷ A ′′ with A ′′ ≡ A and so by transitivity of conversion Γ ⊢ u ◁ A ′ . We can thus apply App to conclude. ◀ Contrarily to correctness, which kept a similar derivation structure, completeness is of a different nature. Because in bidirectional derivations the conversion rules are much less liberal than in undirected derivations, the bulk of the proof is to ensure that conversions can be permuted with structural rules, in order to concentrate them in the places where they are authorized in the bidirectional derivation. In a way, composing completeness with conversion gives a kind of normalization procedure that produces a canonical undirected derivation by pushing all conversions down as much as possible.

Reduction strategies
The judgements of Figure 2 are syntax-directed, in the sense that there is always at most one rule that can be used to derive a certain typing judgements. But with the rules as given there is still some indeterminacy. Indeed when appealing to reduction no strategy is fixed, thus two different reducts give different uses of the rule, resulting in different inferred types -although those are still convertible. However, a reduction strategy can be imposed to completely eliminate indeterminacy in typing, leading to the following.
▶ Proposition 4 (Reduction strategy). If → * is replaced by weak-head reduction in rules Sort-Inf and Prod-Inf, then given a well-formed context Γ and a term t there is at most one derivation of Γ ⊢ t ▷ T and Γ ⊢ t ▷ h T , and so in particular such a T is unique. Similarly, given well-formed Γ and T and a term t there is at most one derivation of Γ ⊢ t◁T . Moreover, the existence of those derivations is decidable.
The algorithm for deciding the existence of the derivations is straightforward from the modded rules, it amounts to structural recursion on the subject.

From CCω to PCUIC
CCω is already a powerful system, but today's proof assistants rely on much more complex features. The Predicative Calculus of Cumulative Inductive Constructions (PCUIC), the type theory nowadays behind the Coq proof assistant, for instance features the impredicative sort Prop, the sort SProp of irrelevant propositions, algebraic universes, cumulativity, polymorphic and mutual inductive and co-inductive types, (co-)fixpoints, primitive projections. . . This is a good stress test for the bidirectional approach: being able to adapt seamlessly to those features is a good sign that the methodology we presented should be able to handle other extensions. In this section, we present some modifications and additions to the system of Section 2 needed to treat the most usual features of PCUIC. Bidirectional judgments incorporating the elements described is this section have been formally proven correct 5 and complete 6 with respect to the description of PCUIC in the MetaCoq project [17]. While working on this, we were able to uncover an incompleteness bug in the current kernel of Coq regarding pattern-matching of cumulative inductive types. This bug had gone unnoticed until our formalization, but was causing subject reduction failures in corner cases with inductive types 7 .
As a demonstration of the use of bidirectionality for reasoning, the formalization also contains a proof of the uniqueness of inferred types and of the existence of principal types as a direct corollary. 8

Cumulativity
PCUIC incorporates a limited form of subtyping. Conversion ≡ is replaced by cumulativity ⪯, a very similar relation, but with the difference that it relaxes the constraint on universes: for conversions □ i ≡ □ j only when i = j, but for cumulativity □ i ⪯ □ j whenever i ≤ j. The conversion rule is accordingly replaced by the following cumulativity rule This reflects the view that universes □ i should be included one in the next when going up in the hierarchy. In CCω, all types for a given term t in a fixed context Γ are equally good, as they are all convertible. This is not the case any more in presence of cumulativity, as we can have T ⪯ T ′ but not T ≡ T ′ . Of particular interest are principal types, defined as follows.
▶ Definition 5 (Principal type). The term T is called a principal type for term t in context Γ if it is a least type for t in Γ, that is if Γ ⊢ t : T and for any T ′ such that Γ ⊢ t : The existence of such principal types is no so easy to prove directly but quite useful, as they are in a sense the best types for any terms. Indeed, if T is a principal type for t in Γ and T ′ is any other type for t, the Cumul rule can be used to deduce Γ ⊢ t : T ′ from Γ ⊢ t : T , which in general is not the case if T is not principal. Similarly, if T and T ′ are two types for a term t, then they are not directly related, but the existence of principal types 5 The formalized theorem is at line 419 and following of BDToPCUIC.v. 6 The formalized theorem is at line 387 and following of BDFromPCUIC.v. 7 The precise technical problem is described in the following git issue: https://github.com/coq/coq/ issues/13495. 8 The corresponding theorems are respectively at line 347 and 355 of BDUnique.v.
ensures that there exists some T ′′ that is a type for t and such that T ⪯ T ′ and T ⪯ T ′′ , indirectly relating T ′ and T ′′ .
Reflecting this modification in the bidirectional system of course calls for an update to the computation rules. The change to the Check rule is direct: simply replace conversion with cumulativity: As to the constrained inference rules, there is no need to modify them. Intuitively, this is because there is no reason to degrade a type to a larger one when it is not needed. We only resort to cumulativity when it is forced by a given input. In that setting, completeness becomes the following: ▶ Theorem 6 (Completeness with cumulativity). If Γ ⊢ t : T using rules of Figure 1 replacing Conv with Cumul, then Γ ⊢ t ▷ T ′ is derivable with rules of Figure 2 replacing Check with Cumul for some T ′ such that T ′ ⪯ T .
In that setting, even without fixing a reduction strategy as in Proposition 4, there is a weaker uniqueness property for inference types, that is vacuous in a setting without cumulativity, where all types are convertible.

▶ Proposition 7 (Uniqueness of inferred type). If Γ is well-formed, Γ ⊢ t ▷ T and Γ ⊢ t ▷ T
Proof. Mutual induction on the first derivation. It is key that constrained inference rules only reduce a type, so that the type in the conclusion is convertible to the type in the premise, rather than merely in cumulativity relation. ◀ In particular, those two properties with a correctness property akin to Theorem 2, we can prove that any inferred type is principal, and so that they both exist and are computable since the bidirectional judgement can still be turned into an algorithm in the spirit of Proposition 4.

▶ Proposition 8 (Principal types). If Γ is well-formed and Γ ⊢ t ▷ T then T is a principal type for t in Γ.
Proof. If Γ ⊢ t : T ′ , then by completeness there exists some T ′′ such that Γ ⊢ t ▷ T ′′ and moreover T ′′ ⪯ T ′ . But by uniqueness T ≡ T ′′ ⪯ T ′ and thus T ⪯ T ′ , and T is indeed a principal type for t in Γ. ◀ Reasoning on the bidirectional derivation thus makes proofs easier, with the correctness and completeness properties ensure they can be carried to the undirected system. Another way to understand this is that seeing completeness followed by correction as a normalization procedure on derivations, the produced canonical derivation is more structured and thus more amenable to proofs. Here for instance the uniqueness of the inferred type translates to the existence of principal types via completeness, and the normalization of the derivations optimizes it to derive a principal type.

Inductive Types
Sum type. Before we turn to the general case of inductive types of the formalization, let us present a simple inductive type: dependent sums. The undirected rules are given in Figure 3, and are inspired from the theoretical presentation of such dependent sums, such at the one C V I T 2 0 1 6 of the Homotopy Type Theory book [19]. In particular, we use the same convention to write y.P when variable y is bound in P . Note however that contrarily to [19], some typing information is kept on the pair constructor. Exactly as for the abstraction, this is to be able to infer a unique, most general type in the bidirectional system. Indeed, without that information a pair (a, b) could inhabit multiple types Σ To obtain the bidirectional rules of Figure 4, first notice that all undirected rules are structural and must thus become inference rules if we want the resulting system to be complete, just as in Section 2. Thus the question is which modes to choose for the premises. For Σ-type and Σ-cons this is straightforward: when the type appears in the conclusion, use checking, otherwise (constrained) inference. The case of the destructors is somewhat more complex. Handling the subterms of the the destructor in the order in which they usually appear (predicate, branches and finally scrutinee) is not possible, as the context parameters of the inductive type are needed to construct the context for the predicate. However those can be inferred from the scrutinee. Thus, a type for the scrutinee is obtained first using a new constrained inference judgment, forcing the inferred type to be a Σ-type, but leaving its parameters free. Next, the obtained arguments can be used to construct the context to type the predicate. Finally, once the predicate is known to be well-formed, it can be used to type-check the branch.

23:10 Complete Bidirectional Typing for the Calculus of Inductive Constructions
This same approach can be readily extended to other usual inductive types, with recursion or indices posing no specific problems, see Figure 5.
Polymorphic, Cumulative Inductive Types. The account of inductive types in PCUIC is quite different from the one we just gave. On the theoretical side, the main addition is universe polymorphism [18], which means that inductive types and constructors come with explicit universe levels. The Σ-type of the previous paragraph, for instance, would contain an explicit universe level i, and both A and B would be checked against □ i rather than having their level inferred. This makes the treatment of general inductive types easier, at the cost of possibly needless annotations, as here with Σ-types. To make that polymorphism more seamless, those polymorphic inductive types are also cumulative [20]: in much the same way as □ i ⪯ □ j if i ≤ j, also N @i ⪯ N @j , where @i and @j are two different universe levels of the polymorphic inductive N. This enables lifting from a lower inductive type to a higher one, so Apart from that difference, PCUIC as presented in MetaCoq has constructors and inductive types as functions, rather than requiring them to be fully applied. It also separates recursors into a pattern-matching and a fixpoint construct, the latter coming with a specific guard condition to keep the normalization property enjoyed by a system with recursors.
All those choices aim at making the system more flexible and practically usable, but they come with a price: the complexity of the structure of terms is much higher. In particular, contrarily to what happens in Σ-rec, the information needed to type the predicate P and branch b cannot be simply inferred from the scrutinee s -thinking erroneously that this was the case led to the incompleteness bug we mentioned. Instead the case constructor must contain the universe instance and parameters that are used to type the predicate and scrutinee.
A sketch of the resulting rules is given in Figure 6, for a generic inductive I. We use bold characters to denote lists -for instance a is a list of terms -and indexes to denote a specific element -so that a k is the k-th element of the previous. The considered inductive I has parameters of type X, indices of typeY and inhabits some universe □ l . Its constructors c k are of types Π(x : X)(y : Y k ), I x u. Because we are considering a cumulative inductive type, all of those actually have to be instantiate with universe levels, an operation we denote with @i ,. Apart from the extra checking that the parameters given in the match construct have the correct type, and the extra cumulativity check to compare the parameters obtained from the scrutinee and the ones in the node, the structure of the match construct is quite similar to that of the sum type. Concerning the fixpoint construct, the most important part there is the guard condition, but as the bidirectional approach has nothing to add here we leave it out. C V I T 2 0 1 6 Figure 5 Other bidirectional inductive types

Beyond PCUIC: bidirectional extensions to CIC
The use of our bidirectional structure is not limited to CIC or PCUIC. On the contrary, it forms a solid basis for extensions, as we illustrate now.

Localized computation
The free-standing conversion rule Conv is very powerful, but sometimes too much. Indeed, the ability to stack as many conversion rules as desired at any place in an undirected derivation is reasonable only when types are compared using a transitive relation. When this is not the case, for instance when conversion is replaced by a unification-flavoured relation, the undirected system becomes inadequate, because repeated uses of Conv can drastically change a type in an undesired fashion. In such a setting, the equivalence between the undirected and the bidirectional system is lost. In such a setting, contrarily to the undirected system, the bidirectional system is still viable, as it enforces a localized use of conversion: only once, at the interface between inference and checking. This is exactly what happens in [8]. In that paper, the conversion relation is relaxed to accommodate for an additional term ? that behaves as a wildcard and should be considered convertible to any term. Conversion is therefore completely non-transitive, and the extension needs to be based on the bidirectional type system rather than the undirected one in order to ensure that the conversion rule is used in a meaningful way.
More generally, since the equivalence between the undirected and directed variants relies Γ ⊢ t ▷ I I a b Figure 6 Bidirectional inductive type -PCIC style on all properties of Proposition 1, when one of those fails the equivalence between the undirected and bidirectional systems is endangered. This can be a sign that the bidirectional system should be adapted, but it can also signal that the undirected system has become meaningless and that the bidirectional version should be studied instead.

Modding the conversion rule
The fact that the unique conversion rule gives rise to multiple bidirectional ones is important: it signals that there are in fact two ways to consider conversion, although the difference between both is invisible in undirected presentations. But this difference might not be so easily overlooked in extensions of CIC, which then need different treatment for them.
Taking again the example of [8], the Check can be kept as such, because the conversion relation is directly modified in the new system. But this is not the case for partial inference. In fact, rule Sort-Inf has to be supplemented by another rule to treat the case when the inferred type reduces to the wildcard ?, because such a term can be used as a type -with some care taken. The same happens for all constrained inference rules.
Thus, the bidirectional structure clarifies a fact that might be overlooked by those who do not dwell in the implementation of proof assistants: reduction does not only serve as a subroutine of conversion checking, it is also directly needed to determine if a given type is a sort, a product, an inductive. . . Which is quite different from checking that it is convertible to a given sort or product type. Of course one could replace reduction by another machinery to accomplish this task, but if one wishes to modify conversion, this specific role of reduction must be accounted for. Otherwise, rules for ◁ and ▷ h would come out of sync, bringing troubles down the road.

Bidirectional elaboration
In works such as [15,3,8], the procedure described is not typing but rather elaboration: the subject of the derivation t is in a kind of source syntax and the aim is not only to inspect t, but also to output a correspond t ′ in some kind of target syntax. The term t ′ is a more precise account of term t, for instance with solved meta-variables, inserted coercions, and so on. The structure we describe readily adapts to those settings, the extra term t ′ is simply considered as an output of all judgements. Since it is an output, McBride's discipline as described in Section 2.2 demands that when Γ ⊢ t ⇝ t ′ ▷ T (with input context Γ, the subject t elaborates to t ′ and infers type T ) we must ensure that Γ ⊢ t ′ : T , and similarly for all other typing judgements. Having all rules locally preserve this invariant ensures that elaborated terms are always well-typed.

5
Related work

Constrained inference
Although explicit and systematic description of constrained inference in a bidirectional setting is new, traces of it in diverse seemingly ad-hoc workarounds can be found in various works around typing for CIC, illustrating that this notion, although overlooked, is of interest.
In [14], Γ ⊢ t : T is used for what we write Γ ⊢ t ▷ T , but another judgment written Γ ⊢ t :≥ T and denoting type inference followed by reduction is used to effectively inline the two hypothesis of our constrained inference rules. Checking is similarly inlined.
Saïbi [15] describes an elaboration mechanism inserting coercions between types. Those are inserted primarily in checking, when both types are known. However he acknowledges the presence of two special classes to handle the need to cast a term to a sort or a function type without more informations, exactly in the places where we resort to constrained inference rather than checking.
More recently, Sozeau [16] describes a system where conversion is augmented to handle coercion between subset types. Again, Γ ⊢ t : T is used for inference, and the other judgments are inlined. Of interest is the fact that reduction is not enough to perform constrained inference, because type head constructors can be hidden by the subset construction: a term of subset type such as {f : N → N | f 0 = 0} should be usable as a function of type N → N. An erasure procedure is therefore required on top of reduction to remove subset types in the places where we use constrained inference.
These traces can also be found in the description of Matita's elaboration algorithm [3]. Indeed, the presence of meta-variables on top of coercions as in the two previous works makes it even clearer that specific treatment of what we identified as constrained inference is required. The authors introduce a special judgement they call type-level enforcing corresponding exactly to our ▷ □ judgement. As for ▷ Π , they have two rules to apply a function, one where its inferred type reduces to a product, corresponding to Prod-Inf, and another one to handle the case when the inferred type instead reduces to a meta-variable. As Saïbi, they also need a special case for coercions of terms in function and type position. However, their solution is different. They rely on unification, which is available in their setting, to introduce new meta-variables for the domain and codomain of a product type whenever needed. For ▷ □ though this solution is not viable, as one would need a kind of universe meta-variable. Instead, they rely on backtracking to test multiple possible universe choices.
Finally, we have already mentioned [8] in Section 4, where the bidirectional structure is crucial in describing a gradual extension to CIC. In particular, and similarly to what happens with meta-variables in [3], all constrained inference rules are duplicated: there is one rule when the head constructor is the desired one, and a second one to handle the gradual wildcard.

Completeness
Quite a few articles tackle the problem of bidirectional typing in a setting with an untyped -so called Curry-style -abstraction. This is the case of early work by Coquand [7], the type system of Agda as described in [12], the systems considered by Abel for instance [1], and much of the work of McBride [11,9,10] on the topic. In such systems, λ-abstractions can only be checked against a given type, but cannot infer one, so that only terms with no β-redexes are typable. Norell argues in [12] that such β-redexes are uncommon in real-life programs, so that being unable to type them is not a strong limitation in practice. To circumvent this problem, McBride also adds the possibility of typing annotations to retain the typability of a term during reduction. While this approach is adapted to programming languages, where the emphasis is on lightweight syntax, it is not tenable for a proof assistant kernel, where all valid terms should be accepted. Indeed, debugging a proof that is rejected because the kernel fails to accept a perfectly well-typed term the user never wrote -as most proofs are generated rather than written directly -is simply not an option.
In a setting with typed -Church-style -abstraction, if one wishes to give the possibility for seemingly untyped abstraction, another mechanism has to be resorted to, typically meta-variables. This is what is done in Matita [3], where the authors combine a rule similar to Abs -where the type of the abstraction is inferred -with another one, similar to the Curry-style one -where abstraction is checked -looking like this: While such a rule would make a simple system such as that of Section 2 "over-complete", it is a useful addition to enable information from checking to be propagated upwards in the derivation. This is crucial in extensions where completeness is lost, such as Matita's elaboration. Similar rules are described in [3] for let-bindings and constructors of inductive types. Although only few authors consider the problem of a complete bidirectional algorithm for type-checking dependent types, we are not the first to attack it. Already Pollack [14] does, and the completeness proof for CCω of Section 2 is very close to one given in his article. Another proof of completeness for a more complex CIC-like system can be found in [16]. None of those however tackle as we do the whole complexity of PCUIC.

Inputs and outputs
We already credited the discipline we adopt on well-formedness of inputs and outputs to McBride [9,10]. A similar idea has also appeared independently in [5]. Bauer and his co-authors introduce the notions of a (weakly) presuppositive type theory [5, Def. 5.6] and of well-presented premise-family and rule-boundary [5, Def. 6.16 and 6.17] to describe a discipline similar to ours, using what they call the boundary of a judgment as the equivalent of our inputs and outputs. Due to their setting being undirected, this is however more restrictive, because they are not able to distinguish inputs from outputs and thus cannot relax their condition to only demand inputs to be well-formed but not outputs.

Conclusion
We have described a judgmental presentation of the bidirectional structure of typing algorithms in the setting of dependent types. In particular, we identified a new family of judgements we called constrained inference. Those have no counterpart in the non-dependent setting, as they result from a choice of modding for the conversion rule, which is specific to the dependent setting. We proved our bidirectional presentation equivalent to an undirected one, both on paper on the simple case of CCω, and formally in the much more complex and realistic setting of PCUIC. Finally, we gave various arguments for the usefulness of our presentation as a way to ease proofs, an intermediate between undirected type-systems and typing algorithms, a solid basis to design extensions, and a tool to re-interpret previous work on type systems in a clearer way.
Regarding future work, a type-checking algorithm is already part of MetaCoq, and we should be able to use our bidirectional type system to give a pleasant completeness proof by separating the concerns pertaining to bidirectionality from the algorithmic problems, such as implementation of an efficient conversion check or proof of termination. More broadly, our bidirectional type system should be an interesting tool in the feat of incorporating in a proof assistant features that have been satisfactorily investigated on the theoretical level while keeping a complete and correct kernel, avoiding the pitfall of cumulative inductive type's incomplete implementation in Coq. A first step would be to investigate the discrepancies between the presentations of Section 3, and in particular if all informations currently stored in the case node are really needed, or if a more concise presentation can be given. But we could go further and study how to handle cubical type theory [21], rewrite rules [6], setoid type theory [2], exceptional type theory [13], η-conversion. . . Finally, we hope that our methodology will be adapted as a base for other theoretical investigations. As a way to ease this adoption, studying it in a general setting such as that of [5] might be a strong argument for adoption.