Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone





isType :: Expr -> Sort -> TCM Type Source #

Check that an expression is a type.

isType_ :: Expr -> TCM Type Source #

Check that an expression is a type without knowing the sort.

ptsRule :: (LensSort a, LensSort b) => a -> b -> TCM Sort Source #

noFunctionsIntoSize :: Type -> Type -> TCM () Source #

Ensure that a (freshly created) function type does not inhabit SizeUniv. Precondition: When noFunctionsIntoSize t tBlame is called, we are in the context of tBlame in order to print it correctly. Not being in context of t should not matter, as we are only checking whether its sort reduces to SizeUniv.

isTypeEqualTo :: Expr -> Type -> TCM Type Source #

Check that an expression is a type which is equal to a given type.


checkTelescope :: Telescope -> (Telescope -> TCM a) -> TCM a Source #

Type check a (module) telescope. Binds the variables defined by the telescope.

checkPiTelescope :: Telescope -> (Telescope -> TCM a) -> TCM a Source #

Type check the telescope of a dependent function type. Binds the resurrected variables defined by the telescope. The returned telescope is unmodified (not resurrected).

data LamOrPi Source #

Flag to control resurrection on domains.



We are checking a module telescope. We pass into the type world to check the domain type. This resurrects the whole context.


We are checking a telescope in a Pi-type. We stay in the term world, but add resurrected domains to the context to check the remaining domains and codomain of the Pi-type.

checkTelescope' :: LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a Source #

Type check a telescope. Binds the variables defined by the telescope.

checkTypedBindings :: LamOrPi -> TypedBindings -> (Telescope -> TCM a) -> TCM a Source #

Check a typed binding and extends the context with the bound variables. The telescope passed to the continuation is valid in the original context.

Parametrized by a flag wether we check a typed lambda or a Pi. This flag is needed for irrelevance.

Lambda abstractions

checkLambda :: Arg TypedBinding -> Expr -> Type -> TCM Term Source #

Type check a lambda expression.

checkPostponedLambda :: Arg ([WithHiding Name], Maybe Type) -> Expr -> Type -> TCM Term Source #

Checking a lambda whose domain type has already been checked.

insertHiddenLambdas Source #


:: Hiding

Expected hiding.

-> Type

Expected to be a function type.

-> (MetaId -> Type -> TCM Term)

Continuation on blocked type.

-> (Type -> TCM Term)

Continuation when expected hiding found. The continuation may assume that the Type is of the form (El _ (Pi _ _)).

-> TCM Term

Term with hidden lambda inserted.

Insert hidden lambda until the hiding info of the domain type matches the expected hiding info. Throws WrongHidingInLambda

checkAbsurdLambda :: ExprInfo -> Hiding -> Expr -> Type -> TCM Term Source #

checkAbsurdLambda i h e t checks absurd lambda against type t. Precondition: e = AbsurdLam i h

checkExtendedLambda :: ExprInfo -> DefInfo -> QName -> [Clause] -> Expr -> Type -> TCM Term Source #

checkExtendedLambda i di qname cs e t check pattern matching lambda. Precondition: e = ExtendedLam i di qname cs

catchIlltypedPatternBlockedOnMeta :: TCM () -> TCM (Maybe (TCErr, MetaId)) Source #

Run a computation.

  • If successful, return Nothing.
  • If IlltypedPattern p a is thrown and type a is blocked on some meta x return Just x. Note that the returned meta might only exists in the state where the error was thrown, thus, be an invalid MetaId in the current state.
  • If another error was thrown or the type a is not blocked, reraise the error.


checkRecordExpression :: RecordAssigns -> Expr -> Type -> TCM Term Source #

checkRecordExpression fs e t checks record construction against type t. Precondition e = Rec _ fs.

checkRecordUpdate :: ExprInfo -> Expr -> Assigns -> Expr -> Type -> TCM Term Source #

checkRecordUpdate ei recexpr fs e t Precondition e = RecUpdate ei recexpr fs.



checkArguments' :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> (Args -> Type -> TCM Term) -> TCM Term Source #

checkArguments' exph r args t0 t k tries checkArguments exph args t0 t. If it succeeds, it continues k with the returned results. If it fails, it registers a postponed typechecking problem and returns the resulting new meta variable.

Checks e := ((_ : t0) args) : t.

checkExpr :: Expr -> Type -> TCM Term Source #

Type check an expression.

checkApplication :: Expr -> Args -> Expr -> Type -> TCM Term Source #

checkApplication hd args e t checks an application. Precondition: Application hs args = appView e

checkApplication disambiguates constructors (and continues to checkConstructorApplication) and resolves pattern synonyms.

unquoteM :: Expr -> Term -> Type -> TCM Term -> TCM Term Source #

Unquote a TCM computation in a given hole.

domainFree :: ArgInfo -> Name -> LamBinding Source #

Turn a domain-free binding (e.g. lambda) into a domain-full one, by inserting an underscore for the missing type.

Meta variables

checkOrInferMeta :: (Type -> TCM Term) -> Maybe Type -> MetaInfo -> TCM (Term, Type) Source #

Type check a meta variable. If its type is not given, we return its type, or a fresh one, if it is a new meta. If its type is given, we check that the meta has this type, and we return the same type.


inferHead :: Expr -> TCM (Args -> Term, Type) Source #

Infer the type of a head thing (variable, function symbol, or constructor). We return a function that applies the head to arguments. This is because in case of a constructor we want to drop the parameters.

checkConstructorApplication :: Expr -> Type -> ConHead -> [NamedArg Expr] -> TCM Term Source #

Check the type of a constructor application. This is easier than a general application since the implicit arguments can be inserted without looking at the arguments to the constructor.

checkHeadApplication :: Expr -> Type -> Expr -> [NamedArg Expr] -> TCM Term Source #

checkHeadApplication e t hd args checks that e has type t, assuming that e has the form hd args. The corresponding type-checked term is returned.

If the head term hd is a coinductive constructor, then a top-level definition fresh tel = hd args (where the clause is delayed) is added, where tel corresponds to the current telescope. The returned term is fresh tel.

Precondition: The head hd has to be unambiguous, and there should not be any need to insert hidden lambdas.

checkArguments :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> ExceptT (Args, [NamedArg Expr], Type) TCM (Args, Type) Source #

Check a list of arguments: checkArgs args t0 t1 checks that t0 = Delta -> t0' and args : Delta. Inserts hidden arguments to make this happen. Returns the evaluated arguments vs, the remaining type t0' (which should be a subtype of t1) and any constraints cs that have to be solved for everything to be well-formed.

checkArguments_ Source #


:: ExpandHidden

Eagerly insert trailing hidden arguments?

-> Range

Range of application.

-> [NamedArg Expr]

Arguments to check.

-> Telescope

Telescope to check arguments against.

-> TCM (Args, Telescope)

Checked arguments and remaining telescope if successful.

Check that a list of arguments fits a telescope. Inserts hidden arguments as necessary. Returns the type-checked arguments and the remaining telescope.

inferExpr :: Expr -> TCM (Term, Type) Source #

Infer the type of an expression. Implemented by checking against a meta variable. Except for neutrals, for them a polymorphic type is inferred.

checkDontExpandLast :: Expr -> Type -> TCM Term Source #

Used to check aliases f = e. Switches off ExpandLast for the checking of top-level application.

isModuleFreeVar :: Int -> TCM Bool Source #

Check whether a de Bruijn index is bound by a module telescope.

inferExprForWith :: Expr -> TCM (Term, Type) Source #

Infer the type of an expression, and if it is of the form {tel} -> D vs for some datatype D then insert the hidden arguments. Otherwise, leave the type polymorphic.

Let bindings