Agda.TypeChecking.InstanceArguments

Documentation

type Candidates = [(Term, Type)]

A candidate solution for an instance meta is a term with its type.

initialIFSCandidates :: TCM Candidates

initializeIFSMeta :: String -> Type -> TCM Term

initializeIFSMeta s t generates an instance meta of type t with suggested name s.

findInScope :: MetaId -> Candidates -> TCM ()

findInScope m (v,a)s tries to instantiate on of the types as of the candidate terms vs to the type t of the metavariable m. If successful, meta m is solved with the instantiation of v. If unsuccessful, the constraint is regenerated, with possibly reduced candidate set.

findInScope' :: MetaId -> Candidates -> TCM (Maybe Candidates)

Result says whether we need to add constraint, and if so, the set of remaining candidates.

checkCandidates :: MetaId -> Type -> Candidates -> TCM Candidates

Given a meta m of type t and a list of candidates cands, checkCandidates m t cands returns a refined list of valid candidates.

applyDroppingParameters :: Term -> Args -> TCM Term

To preserve the invariant that a constructor is not applied to its parameter arguments, we explicitly check whether function term we are applying to arguments is a unapplied constructor. In this case we drop the first conPars arguments. See Issue670a. Andreas, 2013-11-07 Also do this for projections, see Issue670b.

solveIrrelevantMetas :: TCM ()

Attempt to solve irrelevant metas by instance search.

solveMetaIfIrrelevant :: MetaId -> TCM ()