Safe Haskell | None |
---|---|
Language | Haskell98 |
Functions for inserting implicit arguments at the right places.
- implicitArgs :: Int -> (Hiding -> Bool) -> Type -> TCM (Args, Type)
- implicitNamedArgs :: Int -> (Hiding -> ArgName -> Bool) -> Type -> TCM (NamedArgs, Type)
- data ImplicitInsertion
- impInsert :: [Hiding] -> ImplicitInsertion
- insertImplicit :: NamedArg e -> [Arg ArgName] -> ImplicitInsertion
Documentation
implicitArgs :: Int -> (Hiding -> Bool) -> Type -> TCM (Args, Type) Source
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) Source
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 Source
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 |
impInsert :: [Hiding] -> ImplicitInsertion Source
insertImplicit :: NamedArg e -> [Arg ArgName] -> ImplicitInsertion Source
The list should be non-empty.