Get goal type in `Grind.GoalM`

Stream: lean4

[Marcus Rossel]

The grind tactic provides a way of hooking into failing invocations with the on_failure syntax. There, one can specify a definition of type Grind.GoalM Unit to be run if grind fails. Is there a way to obtain the original proof goal in such a function (i.e. in Grind.GoalM)? I tried the following:

import Lean
open Lean Meta Grind

def logGoalType : GoalM Unit := do
  let goal ← get
  let goalType ← goal.mvarId.getType
  logInfo m!"Goal Type: {goalType}"

example : 1 = 2 := by
  grind on_failure logGoalType

... but that always prints Goal Type: False, as grind tries to prove False assuming the negation of the actual proof goal. Thus, I don't see a way to obtain the original proof goal from Grind.GoalM.

[Henrik Böving]

Is there a particular reason you're trying to get the original goal? Maybe #xy?

[Marcus Rossel]

I want to try to extract the smallest (AST-size) term equivalent to original proof goal from grind's e-graph.