Agda.TypeChecking.Implicit

Functions for inserting implicit arguments at the right places.

Documentation

implicitArgs :: Int -> (Hiding -> Bool) -> Type -> TCM (Args, Type)

implicitArgs n expand eti t generates up to n implicit arguments metas (unbounded if n<0), as long as t is a function type and expand holds on the hiding info of its domain. If eti is ExplicitToInstance, then explicit arguments are considered as instance arguments.

implicitNamedArgs :: Int -> (Hiding -> ArgName -> Bool) -> Type -> TCM (NamedArgs, Type)

implicitNamedArgs n expand eti t generates up to n named implicit arguments metas (unbounded if n<0), as long as t is a function type and expand holds on the hiding and name info of its domain. If eti is ExplicitToInstance, then explicit arguments are considered as instance arguments.

data ImplicitInsertion

Constructors

ImpInsert [Hiding]

this many implicits have to be inserted

BadImplicits

hidden argument where there should have been a non-hidden arg

NoSuchName ArgName

bad named argument

NoInsertNeeded

Instances

Show ImplicitInsertion

Methods

showsPrec :: Int -> ImplicitInsertion -> ShowS

show :: ImplicitInsertion -> String

showList :: [ImplicitInsertion] -> ShowS

impInsert :: [Hiding] -> ImplicitInsertion

insertImplicit :: NamedArg e -> [Arg ArgName] -> ImplicitInsertion

The list should be non-empty.