Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Irrelevance

Contents

- Propositions
- Fibrant types

Description

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] @@

Synopsis

- class UsableRelevance a where
  - usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> a -> m Bool
- class UsableModality a where
  - usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> a -> 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 ()
- isPropM :: (LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) => a -> m Bool
- isIrrelevantOrPropM :: (LensRelevance a, LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) => a -> m Bool
- allIrrelevantOrPropTel :: (PureTCM m, MonadBlock m) => Telescope -> m Bool
- isFibrant :: (LensSort a, PureTCM m, MonadBlock m) => a -> m Bool
- isFibrant' :: (LensSort a, PureTCM m) => a -> m (Either Blocker Bool)
- isCoFibrantSort :: (LensSort a, PureTCM m) => a -> m (Either Blocker Bool)

# Documentation

class UsableRelevance a where Source #

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 Source #

#### Instances

Instances details

UsableRelevance Level Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Level -> m Bool Source #
UsableRelevance PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> PlusLevel -> m Bool Source #
UsableRelevance Sort Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Sort -> m Bool Source #
UsableRelevance Term Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Term -> m Bool Source #
UsableRelevance a => UsableRelevance (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Arg a -> m Bool Source #
(Subst a, UsableRelevance a) => UsableRelevance (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Abs a -> m Bool Source #
UsableRelevance a => UsableRelevance (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Dom a -> m Bool Source #
UsableRelevance a => UsableRelevance (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Type' a -> m Bool Source #
UsableRelevance a => UsableRelevance (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Elim' a -> m Bool Source #
UsableRelevance a => UsableRelevance [a] Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> [a] -> m Bool Source #
(UsableRelevance a, UsableRelevance b) => UsableRelevance (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> (a, b) -> m Bool Source #
(UsableRelevance a, UsableRelevance b, UsableRelevance c) => UsableRelevance (a, b, c) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> (a, b, c) -> m Bool Source #

class UsableModality a where Source #

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 Source #

#### Instances

Instances details

UsableModality Level Source # |
Instance details 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 Source #
UsableModality Sort Source # |
Instance details 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 Source #
UsableModality Term Source # |
Instance details 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 Source #
UsableModality a => UsableModality (Arg a) Source # |
Instance details 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 Source #
UsableModality a => UsableModality (Dom a) Source # |
Instance details 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 Source #
UsableRelevance a => UsableModality (Type' a) Source # |
Instance details 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 Source #
UsableModality a => UsableModality (Elim' a) Source # |
Instance details 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 Source #
UsableModality a => UsableModality [a] Source # |
Instance details 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 Source #
(UsableModality a, UsableModality b) => UsableModality (a, b) Source # |
Instance details 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 Source #

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

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

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

# Propositions

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

Is a type a proposition? (Needs reduction.)

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

allIrrelevantOrPropTel :: (PureTCM m, MonadBlock m) => Telescope -> m Bool Source #

# Fibrant types

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

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

isFibrant' :: (LensSort a, PureTCM m) => a -> m (Either Blocker Bool) Source #

isCoFibrantSort :: (LensSort a, PureTCM m) => a -> m (Either Blocker Bool) Source #

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