Compile-time modalities

[intsuc]

Let 𝒞 be a compile-time modality. All types are indexed by either 𝒞 or ¬𝒞.

• 𝒸 a : (α @ 𝒞) is guaranteed to be evaluated to its canonical form of α at compile-time.
• a : (α @ ¬𝒞) is not guaranteed to be evaluated to its canonical form of α at compile-time.

The constructor 𝒸 - are hidden from the surface syntax. If a : α, then a ⇐ (α @ 𝒞) elaborates to 𝒸 a by subtyping coercion. 𝒸 a works as a marker to normalize a without type-directedness.

Definitions are indexed by compile-time modalities as follows:

{builtin}
def + [a : (int @ 𝒜), b : (int @ ℬ)] : (int @ (𝒜 ∧ ℬ)) ≔ _

Compile-time modalities can be elided as Rust's lifetime elision. The following definition elaborates to the above definition.

{builtin}
def + [a : int, b : int] : int ≔ _

For example, the following definitional equalities hold:

((𝒸 1) + (𝒸 2)) : (int @ 𝒞) = (𝒸 3) : (int @ 𝒞)
((𝒸 1) + 2) : (int @ ¬𝒞) = (1 + 2) : (int @ ¬𝒞)
(1 + (𝒸 2)) : (int @ ¬𝒞) = (1 + 2) : (int @ ¬𝒞)
(1 + 2) : (int @ ¬𝒞) = (1 + 2) : (int @ ¬𝒞)

Runtime-only definitions are represented by ¬𝒞 as follows:

def seed [] : (int @ ¬𝒞)

A type with 𝒞 must not contain types with ¬𝒞. Since its inhabitant cannot evaluate to its canonical form, the following type is ill-formed:

(list (int @ ¬𝒞) @ 𝒞)