Agda.TypeChecking.Irrelevance

Compile-time irrelevance.

In type theory with compile-time irrelevance à la Pfenning (LiCS 2001), variables in the context are annotated with relevance attributes. @ Γ = r₁x₁:A₁, ..., rⱼxⱼ:Aⱼ To handle irrelevant projections, we also record the current relevance attribute in the judgement. For instance, this attribute is equal to to Irrelevant if we are in an irrelevant position, like an irrelevant argument. Γ ⊢r t : A Only relevant variables can be used: @

(Relevant x : A) ∈ Γ -------------------- Γ ⊢r x : A @ Irrelevant global declarations can only be used if r = Irrelevant@.

When we enter a r'-relevant function argument, we compose the r with r' and (left-)divide the attributes in the context by r'. @ Γ ⊢r t : (r' x : A) → B r' Γ ⊢(r'·r) u : A --------------------------------------------------------- Γ ⊢r t u : B[u/x] No surprises for abstraction: @

Γ, (r' x : A) ⊢r : B ----------------------------- Γ ⊢r λxt : (r' x : A) → B @@

This is different for runtime irrelevance (erasure) which is `flat', meaning that once one is in an irrelevant context, all new assumptions will be usable, since they are turned relevant once entering the context. See Conor McBride (WadlerFest 2016), for a type system in this spirit:

We use such a rule for runtime-irrelevance: @ Γ, (q q') x : A ⊢q t : B ------------------------------ Γ ⊢q λxt : (q' x : A) → B @

Conor's system is however set up differently, with a very different variable rule:

@@

(q x : A) ∈ Γ -------------- Γ ⊢q x : A

Γ, (q·p) x : A ⊢q t : B ----------------------------- Γ ⊢q λxt : (p x : A) → B

Γ ⊢q t : (p x : A) → B Γ' ⊢qp u : A ------------------------------------------------- Γ + Γ' ⊢q t u : B[u/x] @@

Documentation

class UsableRelevance a where

Check whether something can be used in a position of the given relevance.

This is a substitute for double-checking that only makes sure relevances are correct. See issue #2640.

Used in unifier ( unifyStep Solution{}).

At the moment, this implements McBride-style irrelevance, where Pfenning-style would be the most accurate thing. However, these two notions only differ how they handle bound variables in a term. Here, we are only concerned in the free variables, used meta-variables, and used (irrelevant) definitions.

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> a -> m Bool

Instances

UsableRelevance Level

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Level -> m Bool

UsableRelevance PlusLevel

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> PlusLevel -> m Bool

UsableRelevance Sort

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Sort -> m Bool

UsableRelevance Term

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Term -> m Bool

UsableRelevance a => UsableRelevance (Arg a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Arg a -> m Bool

(Subst a, UsableRelevance a) => UsableRelevance (Abs a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Abs a -> m Bool

UsableRelevance a => UsableRelevance (Dom a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Dom a -> m Bool

UsableRelevance a => UsableRelevance (Type' a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Type' a -> m Bool

UsableRelevance a => UsableRelevance (Elim' a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Elim' a -> m Bool

UsableRelevance a => UsableRelevance [a]

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> [a] -> m Bool

(UsableRelevance a, UsableRelevance b) => UsableRelevance (a, b)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> (a, b) -> m Bool

(UsableRelevance a, UsableRelevance b, UsableRelevance c) => UsableRelevance (a, b, c)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> (a, b, c) -> m Bool

class UsableModality a where

Check whether something can be used in a position of the given modality.

This is a substitute for double-checking that only makes sure modalities are correct. See issue #2640.

Used in unifier ( unifyStep Solution{}).

This uses McBride-style modality checking. It does not differ from Pfenning-style if we are only interested in the modality of the free variables, used meta-variables, and used definitions.

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> a -> m Bool

Instances

UsableModality Level

Defined in Agda.TypeChecking.Irrelevance

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Level -> m Bool

UsableModality Sort

Defined in Agda.TypeChecking.Irrelevance

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Sort -> m Bool

UsableModality Term

Defined in Agda.TypeChecking.Irrelevance

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Term -> m Bool

UsableModality a => UsableModality (Arg a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Arg a -> m Bool

UsableModality a => UsableModality (Dom a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Dom a -> m Bool

UsableRelevance a => UsableModality (Type' a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Type' a -> m Bool

UsableModality a => UsableModality (Elim' a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Elim' a -> m Bool

UsableModality a => UsableModality [a]

Defined in Agda.TypeChecking.Irrelevance

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> [a] -> m Bool

(UsableModality a, UsableModality b) => UsableModality (a, b)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> (a, b) -> m Bool

usableModAbs :: (Subst a, MonadAddContext m, UsableModality a, ReadTCState m, HasConstInfo m, MonadReduce m, MonadError Blocker m) => ArgInfo -> Modality -> Abs a -> m Bool

usableAtModality' :: MonadConstraint TCM => Maybe Sort -> WhyCheckModality -> Modality -> Term -> TCM ()

usableAtModality :: MonadConstraint TCM => WhyCheckModality -> Modality -> Term -> TCM ()

Propositions

isPropM :: (LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) => a -> m Bool

Is a type a proposition? (Needs reduction.)

isIrrelevantOrPropM :: (LensRelevance a, LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) => a -> m Bool

Fibrant types

isFibrant :: (LensSort a, PureTCM m, MonadBlock m) => a -> m Bool

Is a type fibrant (i.e. Type, Prop)?

isCoFibrantSort :: (LensSort a, PureTCM m, MonadBlock m) => a -> m Bool

Cofibrant types are those that could be the domain of a fibrant pi type. (Notion by C. Sattler).