Agda.TypeChecking.InstanceArguments

Documentation

initialIFSCandidates :: TCM [(Term, Type)]

initializeIFSMeta :: String -> Type -> TCM Term

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

findInScope :: MetaId -> [(Term, Type)] -> 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 -> [(Term, Type)] -> TCM (Maybe [(Term, Type)])

getMetaTypeInContext :: MetaId -> TCM Type

checkCandidates :: MetaId -> Type -> [(Term, Type)] -> TCM [(Term, Type)]

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.

solveIrrelevantMetas :: TCM ()

Attempt to solve irrelevant metas by instance search.

solveMetaIfIrrelevant :: MetaId -> TCM ()