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 :: Sort -> TCM Sort
- sortFitsIn :: Sort -> Sort -> TCM ()
- hasBiggerSort :: Sort -> TCM ()
- inferPiSort :: Sort -> Abs Sort -> TCM Sort
- inferFunSort :: Sort -> Sort -> TCM Sort
- ptsRule :: Sort -> Abs Sort -> Sort -> TCM ()
- ptsRule' :: Sort -> Sort -> Sort -> TCM ()
- hasPTSRule :: Sort -> Abs Sort -> TCM ()
- checkTelePiSort :: Type -> TCM ()

# Documentation

inferUnivSort :: Sort -> TCM 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.

hasBiggerSort :: Sort -> TCM () Source #

inferPiSort :: Sort -> Abs Sort -> TCM Sort Source #

Infer the sort of a pi type. If we can compute the sort straight away,
return that. Otherwise, return `PiSort s1 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.