Agda.TypeChecking.InstanceArguments

Documentation

findInstance :: MetaId -> Maybe [Candidate] -> TCM ()

findInstance 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. The list of candidates is equal to Nothing when the type of the meta wasn't known when the constraint was generated. In that case, try to find its type again.

isInstanceConstraint :: Constraint -> Bool

solveAwakeInstanceConstraints :: TCM ()

shouldPostponeInstanceSearch :: (ReadTCState m, HasOptions m) => m Bool

postponeInstanceConstraints :: TCM a -> TCM a

getInstanceCandidates :: MetaId -> TCM (Either Blocker [Candidate])

Entry point for tcGetInstances primitive

getInstanceDefs :: TCM InstanceTable

Try to solve the instance definitions whose type is not yet known, report an error if it doesn't work and return the instance table otherwise.

data OutputTypeName

Constructors

OutputTypeName QName

OutputTypeVar

OutputTypeVisiblePi

OutputTypeNameNotYetKnown Blocker

NoOutputTypeName

getOutputTypeName :: Type -> TCM (Telescope, Term, OutputTypeName)

Strips all hidden and instance Pi's and return the argument telescope, the head term, and its name, if possible.

addTypedInstance

Arguments

:: QName

Name of instance.

-> Type

Type of instance.

-> TCM ()

Register the definition with the given type as an instance. Issue warnings if instance is unusable.

addTypedInstance'

Arguments

:: Bool

Should we print warnings for unusable instance declarations?

-> Maybe InstanceInfo

Is this instance a copy?

-> QName

Name of instance.

-> Type

Type of instance.

-> TCM ()

Register the definition with the given type as an instance.

pruneTemporaryInstances :: Interface -> TCM Interface

Prune an Interface to remove any instances that would be inapplicable in child modules.

While in a section with visible arguments, we add any instances defined locally to the instance table: you have to be able to find them, after all! Conservatively, all of the local variables are turned into FlexKs, i.e., wildcards.

But when we leave such a section, these instances have no more value: even though they might technically be in scope, their types are malformed, since they have visible pis.

This function deletes these instances from the instance tree in the given signature to save on serialisation time *and* time spent checking for candidate validity in client modules. It can't do this directly in the TC state to prevent these instances from going out of scope before interaction (see #7196).

resolveInstanceHead :: QName -> TCM ()