Agda.TypeChecking.Monad.Modality

Prepare parts of a parameter telescope for abstraction in constructors and projections.

Modify the context whenever going from the l.h.s. (term side) of the typing judgement to the r.h.s. (type side).

Internal workhorse, expects value of --experimental-irrelevance flag as argument.

(Conditionally) wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.

Also allow the use of irrelevant definitions.

(Conditionally) wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.

Precondition: Relevance /= Relevant

Apply relevance rel the the relevance annotation of the (typing/equality) judgement. This is part of the work done when going into a rel-context.

Precondition: Relevance /= Relevant

Like applyRelevanceToContext, but only act on context if --irrelevant-projections. See issue #2170.

Apply the quantity to the quantity annotation of the (typing/equality) judgement.

Precondition: The quantity must not be Quantity1 something.

Apply inverse composition with the given cohesion to the typing context.

Can we split on arguments of the given cohesion?

(Conditionally) wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.

Also allow the use of irrelevant definitions.

This function might also do something for other modalities.

(Conditionally) wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.

This function might also do something for other modalities, but not for quantities.

Precondition: Modality /= Relevant

Apply the relevance and quantity components of the modality to the modality annotation of the (typing/equality) judgement.

Precondition: The relevance component must not be Relevant.

Like applyModalityToContext, but only act on context (for Relevance) if --irrelevant-projections. See issue #2170.

Wake up irrelevant variables and make them relevant. This is used when type checking terms in a hole, in which case you want to be able to (for instance) infer the type of an irrelevant variable. In the course of type checking an irrelevant function argument applyRelevanceToContext is used instead, which also sets the context relevance to Irrelevant. This is not the right thing to do when type checking interactively in a hole since it also marks all metas created during type checking as irrelevant (issue #2568).

Also set the current quantity to 0.