Documentation

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.

Entry point for tcGetInstances primitive

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.

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

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

Register the definition with the given type as an instance.

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).