Agda.TypeChecking.CheckInternal

A bidirectional type checker for internal syntax.

Performs checking on unreduced terms. With the exception that projection-like function applications have to be reduced since they break bidirectionality.

Documentation

type MonadCheckInternal m = MonadConversion m

checkType :: MonadCheckInternal m => Type -> m ()

Entry point for e.g. checking WithFunctionType.

checkType' :: MonadCheckInternal m => Type -> m Sort

Check a type and infer its sort.

Necessary because of PTS rule (SizeUniv, Set i, Set i) but SizeUniv is not included in any Set i.

This algorithm follows Abel, Coquand, Dybjer, MPC 08, Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory

checkSort :: MonadCheckInternal m => Action m -> Sort -> m Sort

Check if sort is well-formed.

checkInternal :: MonadCheckInternal m => Term -> Comparison -> Type -> m ()

Entry point for term checking.

checkInternal' :: MonadCheckInternal m => Action m -> Term -> Comparison -> Type -> m Term

data Action m

checkInternal traverses the whole Term, and we can use this traversal to modify the term.

Constructors

Action

Fields

• preAction :: Type -> Term -> m Term

  Called on each subterm before the checker runs.

• postAction :: Type -> Term -> m Term

  Called on each subterm after the type checking.

• relevanceAction :: Relevance -> Relevance -> Relevance

  Called for each ArgInfo. The first Relevance is from the type, the second from the term.

defaultAction :: Monad m => Action m

The default action is to not change the Term at all.

eraseUnusedAction :: Action TCM

infer :: MonadCheckInternal m => Term -> m Type

Infer type of a neutral term.

inferSort :: MonadCheckInternal m => Term -> m Sort

Compute the sort of a type.

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

Result is in reduced form.