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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Sort

Description

This module contains the rules for Agda's sort system viewed as a pure type system (pts). The specification of a pts consists of a set of axioms of the form `s1 : s2` specifying when a sort fits in another sort, and a set of rules of the form `(s1,s2,s3)` specifying that a pi type with domain in `s1` and codomain in `s2` itself fits into sort `s3`.

To ensure unique principal types, the axioms and rules of Agda's pts are given by two partial functions `univSort'` and `piSort'` (see `Agda.TypeChecking.Substitute`). If these functions return `Nothing`, a constraint is added to ensure that the sort will be computed eventually.

One `upgrade` over the standard definition of a pts is that in a rule `(s1,s2,s3)`, in Agda the sort `s2` can depend on a variable of some type in `s1`. This is needed to support Agda's universe polymorphism where we can have e.g. a function of type `∀ {ℓ} → Set ℓ`.

Synopsis

- inferUnivSort :: (PureTCM m, MonadConstraint m) => Sort -> m Sort
- sortFitsIn :: MonadConversion m => Sort -> Sort -> m ()
- hasBiggerSort :: Sort -> TCM ()
- inferPiSort :: PureTCM m => Dom Type -> Abs Sort -> m Sort
- inferFunSort :: Sort -> Sort -> TCM Sort
- ptsRule :: Dom Type -> Abs Sort -> Sort -> TCM ()
- ptsRule' :: Sort -> Sort -> Sort -> TCM ()
- hasPTSRule :: Dom Type -> Abs Sort -> TCM ()
- checkTelePiSort :: Type -> TCM ()
- ifIsSort :: (MonadReduce m, MonadBlock m) => Type -> (Sort -> m a) -> m a -> m a
- ifNotSort :: (MonadReduce m, MonadBlock m) => Type -> m a -> (Sort -> m a) -> m a
- shouldBeSort :: (PureTCM m, MonadBlock m, MonadError TCErr m) => Type -> m Sort
- sortOf :: forall m. (PureTCM m, MonadBlock m) => Term -> m Sort
- sortOfType :: forall m. (PureTCM m, MonadBlock m) => Type -> m Sort

# Documentation

inferUnivSort :: (PureTCM m, MonadConstraint m) => Sort -> m Sort Source #

Infer the sort of another sort. If we can compute the bigger sort straight away, return that. Otherwise, return `UnivSort s` and add a constraint to ensure we can compute the sort eventually.

sortFitsIn :: MonadConversion m => Sort -> Sort -> m () Source #

hasBiggerSort :: Sort -> TCM () Source #

inferPiSort :: PureTCM m => Dom Type -> Abs Sort -> m Sort Source #

Infer the sort of a pi type. If we can compute the sort straight away, return that. Otherwise, return `PiSort a s2` and add a constraint to ensure we can compute the sort eventually.

inferFunSort :: Sort -> Sort -> TCM Sort Source #

As `inferPiSort`, but for a nondependent function type.

ptsRule :: Dom Type -> Abs Sort -> Sort -> TCM () Source #

ptsRule' :: Sort -> Sort -> Sort -> TCM () Source #

Non-dependent version of ptsRule

hasPTSRule :: Dom Type -> Abs Sort -> TCM () Source #

checkTelePiSort :: Type -> TCM () Source #

Recursively check that an iterated function type constructed by `telePi` is well-sorted.

ifIsSort :: (MonadReduce m, MonadBlock m) => Type -> (Sort -> m a) -> m a -> m a Source #

ifNotSort :: (MonadReduce m, MonadBlock m) => Type -> m a -> (Sort -> m a) -> m a Source #

shouldBeSort :: (PureTCM m, MonadBlock m, MonadError TCErr m) => Type -> m Sort Source #

Result is in reduced form.

sortOf :: forall m. (PureTCM m, MonadBlock m) => Term -> m Sort Source #

Reconstruct the sort of a term.

Precondition: given term is a well-sorted type.

sortOfType :: forall m. (PureTCM m, MonadBlock m) => Type -> m Sort Source #

Reconstruct the minimal sort of a type (ignoring the sort annotation).