Instance Wrapping

Both inferInstanceAs and the default deriving handler wrap instance bodies to ensure that when deriving or inferring an instance for a semireducible type definition, the definition's RHS is not leaked when reduced at lower than semireducible transparency.

Algorithm

Given an instance i : I and expected type I' (where I' must be mvar-free), wrapInstance constructs a result instance as follows, executing all steps at instances transparency:

1. If I' is not a class application, return i unchanged.
2. If I' is a proposition, wrap i in an auxiliary theorem of type I' and return it (controlled by backward.inferInstanceAs.wrap.instances).
3. Reduce i to whnf.
4. If i is not a constructor application: if I is already defeq to I', return i; otherwise (if backward.inferInstanceAs.wrap.reuseSubInstances is set) try (recursive) eta-expansion and wrapping of i to see if any sub-instances can be reused; otherwise wrap i in an auxiliary definition of type I' and return it (controlled by backward.inferInstanceAs.wrap.instances).
5. Otherwise, if i is an application of ctor of class C:
   • Unify the conclusion of the type of ctor with I' to obtain adjusted field type Fᵢ' for each field.
   • Return a new application ctor ... : I' where the fields are adjusted as follows:
     • If the field type is a proposition: assign directly if types are defeq, otherwise wrap in an auxiliary theorem.
     • If the field is a parent field (subobject) p : P: first try to reuse an existing instance that can be synthesized for P (controlled by backward.inferInstanceAs.wrap.reuseSubInstances) in order to preserve defeqs; if that fails, recurse.
     • If it is a field of a flattened parent class C' and backward.inferInstanceAs.wrap.reuseSubInstances is true, try synthesizing an instance of C' for I' and if successful, use the corresponding projection of the found instance in order to preserve defeqs; otherwise, continue.
       • Specifically, construct the chain of base projections from C to C' applied to _ : I' and infer its type to obtain an appropriate application of C' for the instance search.
     • Otherwise (non-inherited data field): assign directly if types are defeq, otherwise wrap in an auxiliary definition to fix the type (controlled by backward.inferInstanceAs.wrap.data).

Options

• backward.inferInstanceAs.wrap: master switch for wrapping in both inferInstanceAs and the default deriving handler
• backward.inferInstanceAs.wrap.reuseSubInstances: reuse existing instances for sub-instance fields to avoid non-defeq instance diamonds
• backward.inferInstanceAs.wrap.instances: wrap non-reducible instances in auxiliary definitions
• backward.inferInstanceAs.wrap.data: wrap data fields in auxiliary definitions

opaque Lean.Meta.backward.inferInstanceAs.wrap : Lean.Option Bool

opaque Lean.Meta.backward.inferInstanceAs.wrap.reuseSubInstances : Lean.Option Bool

opaque Lean.Meta.backward.inferInstanceAs.wrap.instances : Lean.Option Bool

opaque Lean.Meta.backward.inferInstanceAs.wrap.data : Lean.Option Bool

def Lean.Meta.abstractInstImplicitArgs (type : Expr) : MetaM Expr

Rebuild a type application with fresh synthetic metavariables for instance-implicit arguments. Non-instance-implicit arguments are assigned from the original application's arguments. If the function is over-applied, extra arguments are preserved.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.wrapInstance (inst expectedType : Expr) (compile logCompileErrors : Bool := true) (isMeta : Bool := false) : MetaM Expr

Wrap an instance value so its type matches the expected type exactly. See the module docstring for the full algorithm specification.

Equations

• One or more equations did not get rendered due to their size.