Exact instance_kind_json schema mirrors pinned ty/instance.rs. No shim or generic argument is collapsed to its definition ID.

def Miri.Input.CompilerInstance.decode (ctx : LowerContext) (tables : CompilerTables) (j : Lean.Json) : Except String (Interpreter.CallInstance × CompilerTables)

Thread all appended DefId/TypeConstId entries back into the shared bundle.

Equations

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