Agda.TypeChecking.Monad.Modality

Modality.

Agda has support for several modalities, namely:

• Cohesion
• Quantity
• Relevance

In order to type check such modalities, we must store the current modality in the typing context. This module provides functions to update the context based on a given modality.

See Agda.TypeChecking.Irrelevance.

Operations on Dom.

hideAndRelParams :: (LensHiding a, LensRelevance a) => a -> a

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

Operations on Context.

workOnTypes :: (MonadTCEnv m, HasOptions m, MonadDebug m) => m a -> m a

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

workOnTypes' :: MonadTCEnv m => Bool -> m a -> m a

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

applyRelevanceToContext :: (MonadTCEnv tcm, LensRelevance r) => r -> tcm a -> tcm a

(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.

applyRelevanceToContextOnly :: MonadTCEnv tcm => Relevance -> tcm a -> tcm a

(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

applyRelevanceToJudgementOnly :: MonadTCEnv tcm => Relevance -> tcm a -> tcm a

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

applyRelevanceToContextFunBody :: (MonadTCM tcm, LensRelevance r) => r -> tcm a -> tcm a

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

applyQuantityToJudgement :: (MonadTCEnv tcm, LensQuantity q) => q -> tcm a -> tcm a

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

Precondition: The quantity must not be Quantity1 something.

applyCohesionToContext :: (MonadTCEnv tcm, LensCohesion m) => m -> tcm a -> tcm a

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

applyCohesionToContextOnly :: MonadTCEnv tcm => Cohesion -> tcm a -> tcm a

splittableCohesion :: (HasOptions m, LensCohesion a) => a -> m Bool

Can we split on arguments of the given cohesion?

applyModalityToContext :: (MonadTCEnv tcm, LensModality m) => m -> tcm a -> tcm a

(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.

applyModalityToContextOnly :: MonadTCEnv tcm => Modality -> tcm a -> tcm a

(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

applyModalityToJudgementOnly :: MonadTCEnv tcm => Modality -> tcm a -> tcm a

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.

applyModalityToContextFunBody :: (MonadTCM tcm, LensModality r) => r -> tcm a -> tcm a

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

wakeIrrelevantVars :: MonadTCEnv tcm => tcm a -> tcm a

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.