Simulating the scope of an inductive declaration in MetaM

Stream: metaprogramming / tactics

[nrs]

I'm trying to debug why info view and trace.Elab and trace.Meta are reporting a different metavariable context (full context is available here: #lean4 > Elab doesn't match infoview?), and for that reason I'm trying to simulate the partially elaborated context when my cursor is located at ... (inj... in the following inductive declaration:

inductive IArithExprSymbols {sig : Signature} [inst : SubSig NatTyE sig] : W sig -> Type _
| val : Nat -> IArithExprSymbols (inject _)

There are a couple of approaches I've tried so far:

inductive test [SubSig NatTyE sig]: W sig -> Type _
| val : Nat -> by run_tac do
  let lctx <- getLCtx
  lctx.forM (fun ldecl => do
    if ldecl.isImplementationDetail then pure _
    else dbg_trace ldecl)
  let mctx <- getMCtx
  Lean.Elab.Tactic.evalTactic (<- `(tactic|exact test (inject ⟨_, _⟩)))

The above isn't ideal because the run_tac sequence messes up the metavariable context. Multiple of the trace.Meta.isDefEq reports from the vanilla trace get jumbled up and it seems to me that so does the evaluation order.

Attempting to use the following will fail because the declaration must be equivalent to a totally elaborated term in order to add it to the environment, and we're interested in a partial context.

run_meta do
    let newdecl := Lean.Declaration.inductDecl
      ( lparams := [] )
      ( nparams := 0 )
      [
      { name := `testInductiveType,
        type := .sort (.succ .zero),
        ctors := [
          .mk `mk (.forallE `x (.const `Nat []) (.const `testb []) .default),
          .mk `nil (.const `testInductiveType [])
        ]}]
        .false
    discard <| compileDecl newdecl

Any suggestions? My next attempt will involve declaring a scope with axioms and seeing how I can bind a goal to simulate the partial target (strictly speaking we're not in TacticM but withLocalDecl is maybe how to do it?), something starting like:

axiom IArithExprSymbols {sig : Signature} [inst : SubSig NatTyE sig] : W sig -> Type _
example : W sig := by _

[nrs]

I'll also be testing out

inductive IArithExprSymbols {sig : Signature} [inst : SubSig NatTyE sig] : W sig -> Type _
| val : Nat -> by_elab do ...

[nrs]

my worry with the axiom ...; example ... method is that the reports from the infoview and trace actually come from trying to elaborate and typecheck the recursor, can anyone confirm?

[nrs]

wrt this last comment, evidence that this could be true is that the following definition will actually report a type mismatch at the recursor level instead of complaining with what I think would usually be `(kernel) arg #n of ... contains a non valid occurrence of the datatypes being declared

structure Signature where
  symbols : Type
  arity : symbols -> Nat

inductive Ext' (sig : Signature) (α : Type _)
| mk : (s : sig.symbols) -> Vector3 α (sig.arity s) -> Ext' sig α

inductive W' (sig : Signature)
| sup : Ext' sig (W' sig) -> (W' sig)

edit: in the above example, elab info trace suggests that the the following two terms are elaborated first before the recursor is constructed, so the desired scope to simulate is the one happening during the elaboration of exactly these (ofc with the adequate changes to model the declaration of IArithExprSymbols)

Wc (isBinder := true) : Signature → Type
@Wc.sup (isBinder := true) : {sig : Signature} → Ext' sig (Wc sig) → Wc sig

[nrs]

update: the code and traces in the following explain what's going on. the term in the inductive scope goes through a second round of elaboration, in this case Lean.Term.elabAnonymousCtor. so using axiom ...; example ... alone are not enough to simulate an inductive declaration, unless your term is fully explicit!

this explains the difference seen in the original topic: below the first declaration typechecks while the second doesn't, and one would be mystified at why looking only at trace.Elab.step (or the beginning of trace.Elab.info) because it does not report the additional elaboration undergone by the term in the inductive scope! the entirety oftrace.Elab.info however will

structure Signature where
  symbols : Type
  arity : symbols -> Nat

inductive Ext (sig : Signature) (α : Type _)
| mk : (s : sig.symbols) -> (Fin2 (sig.arity s) -> α) -> Ext sig α

class SubSig' (siga : Signature) (sigb : outParam Signature) where
  inj : Ext siga α -> Ext sigb α

set_option pp.explicit true
set_option trace.Elab.step.result true

inductive IArithExprSymbols' {sig : Signature} [inst : SubSig' NatTyE sig] : W sig -> Type _
| val : Nat -> @IArithExprSymbols' sig inst ⟨_, _⟩
-- [Elab.step.result] Nat → @IArithExprSymbols' sig inst (@W.sup sig (@Ext.mk sig (W sig) ?m.1941 ?m.1942))

#print IArithExprSymbols'.val
/-
constructor myNamespace.IArithExprSymbols'.val.{u_1} : {sig : Signature} →
  [inst : SubSig' NatTyE sig] →
    {x : sig.symbols} →
      {x_1 : Fin2 (sig.arity x) → W sig} → Nat → @IArithExprSymbols' sig inst (@W.sup sig (@Ext.mk sig (W sig) x x_1))
-/

axiom IArithExprSymbols'' {sig : Signature} [inst : SubSig' NatTyE sig] : W sig -> Type _
def val {sig : Signature} [inst : SubSig' NatTyE sig] : Type _ := Nat -> @IArithExprSymbols'' sig inst ⟨_, _⟩
-- [Elab.step.result] Nat → @IArithExprSymbols'' sig inst (@W.sup sig (@Ext.mk sig (W sig) ?m.2405 ?m.2406))

#print val
/-
def myNamespace.val.{u_1, u_2} : {sig : Signature} → [inst : SubSig' NatTyE sig] → Type u_2 :=
@sorryAx ({sig : Signature} → [inst : SubSig' NatTyE sig] → Type u_2) true
-/

[nrs]

furthermore, knowing this is important to debug typeclass synthesis (as was our initial interest) because in the inductive declaration, the synthesis only succeeds after the second round of elaboration!