Safe Haskell | None |
---|---|

Language | Haskell2010 |

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 :: (MonadReduce m, MonadConstraint m, HasOptions m) => Sort -> m Sort
- sortFitsIn :: MonadConversion m => Sort -> Sort -> m ()
- hasBiggerSort :: Sort -> TCM ()
- inferPiSort :: (MonadReduce m, MonadAddContext m, MonadDebug 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 => Type -> (Sort -> m a) -> m a -> m a
- shouldBeSort :: (MonadReduce m, MonadTCEnv m, ReadTCState m, MonadError TCErr m) => Type -> m Sort
- sortOf :: forall m. (MonadReduce m, MonadTCEnv m, MonadAddContext m, HasBuiltins m, HasConstInfo m) => Term -> m Sort

# Documentation

inferUnivSort :: (MonadReduce m, MonadConstraint m, HasOptions 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 :: (MonadReduce m, MonadAddContext m, MonadDebug 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.

checkTelePiSort :: Type -> TCM () Source #

Recursively check that an iterated function type constructed by `telePi`

is well-sorted.

shouldBeSort :: (MonadReduce m, MonadTCEnv m, ReadTCState m, MonadError TCErr m) => Type -> m Sort Source #

Result is in reduced form.

sortOf :: forall m. (MonadReduce m, MonadTCEnv m, MonadAddContext m, HasBuiltins m, HasConstInfo m) => Term -> m Sort Source #

Reconstruct the sort of a type.

Precondition: given term is a well-sorted type.