Bidirectional typing for dependent types: Why are Sigma, Pi synthesized?

Question

According to the Pfenning philosphy of bidirectional typing, as also explained by Dunfield and Krishnaswamy 2013, constructors should be checked, while eliminators should be synthesized. Cconvention is followed for the most part in the tutorial Checking Dependent Types with Normalization by Evaluation: A Tutorial by David Christiansen. I cannot explain some choices in the tutorial according to the Pfenning philosophy:

The types Sigma x A B and Pi x A B, Nat, Eq A from to, Trivial, and Absurd are all checked in synthesis mode. However, these are kind constructors, as they let us construct values that live in Univ. Why are they checked in synthesis mode?

Can we view these as eliminators of some object that I am unaware of? As an example of what I mean by this, recall that identifiers such as x are also run in synthesis mode. With a bit of squinting, one can convince themselves that identifiers are projections on the context Γ , and thus deserve to be run in synthesis mode.

Is there a similar explanation for why Pi, Simga, Eq, Trivial, Absurd are typed in synthesis mode? what rule-of-thumb does one use to decide whether these should be typed in checking or synthesis mode?

Answer 1

IMHO, it's not like constructors are checked, but introduction rules (including tuples, lambdas, data constructors, etc.) are checked (while elimination rules are synthesized). The kind constructors you mentioned are called formation rules, which are not introduction rules. You can also think this way: if a constructor is checked, then it has a corresponding eliminator which is synthesized. If type constructors should be checked, there should be a corresponding thing synthesized. But there's no such thing (you can't pattern match on $\cal U$).

Answer 2

I don't have an answer for that question, I'm afraid. But I'll just point out that the rule you cite doesn't say that we should use Γ ⊢ e₁ e₂ ⇒ τ just because function application is an eliminator. Instead, it says that within the typing rule for function application, the part that checks the actual function should synthesize (i.e. should be Γ ⊢ e₁ ⇒ τ₁ → τ₂), and once you have this, then which of e₂ and e₁ e₂ are checked or synthesized are simple/obvious engineering choices.