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, 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 the type of i is already defeq to I', return i; otherwise wrap it in an auxiliary definition of type I' and return it (controlled by backward.inferInstanceAs.wrap.instances).
5. Otherwise, for i = ctor a₁ ... aₙ with ctor : C ?p₁ ... ?pₙ:
   • Unify C ?p₁ ... ?pₙ with I'.
   • Return a new application ctor a₁' ... aₙ' : I' where each aᵢ' is constructed as:
     • If the field type is a proposition: assign directly if types are defeq, otherwise wrap in an auxiliary theorem.
     • If the field type is a class: first try to reuse an existing synthesized instance for the target type (controlled by backward.inferInstanceAs.wrap.reuseSubInstances); if that fails, recurse with source instance aᵢ and expected type ?pᵢ.
     • Otherwise (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.

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