pub fn resolve_instance(
ctx: &Context,
mctx: &mut MetaCtx,
required: &Term,
) -> Option<Term>Expand description
Search the Context’s instance database for an instance proving required,
returning the (metavariable-instantiated) instance term. Handles POLYMORPHIC /
RECURSIVE instances (instance {A} [Inhabited A] : Inhabited (List A)): the instance’s
parameter telescope is freshened to metavariables, its conclusion is unified against
required (solving the type parameters), and each PREMISE parameter is then resolved
RECURSIVELY. The first instance that fully resolves wins; failed trials never pollute
mctx (each runs on a clone, committed only on success).