How to read a private definition

Stream: lean4

[Mario Carneiro]

Recently Jeremy asked me what the automatically generated definition for this type was. It turned out to be harder than anticipated to find out.

import Lean

inductive FOTerm
  | var : String → FOTerm
  | app : String → List FOTerm → FOTerm
  deriving BEq

#synth BEq FOTerm -- instBEqFOTerm

#print instBEqFOTerm
-- def instBEqFOTerm : BEq FOTerm :=
-- { beq := [anonymous] }

-- ..what?

section
set_option pp.all true
#print instBEqFOTerm
end

-- def instBEqFOTerm : BEq.{0} FOTerm :=
-- @BEq.mk.{0} FOTerm _private.0.beqFOTerm✝

#print _private.0.beqFOTerm✝ -- syntax fail

open Lean Elab Term Eval

#eval show TermElabM Unit from do
  let env ← getEnv
  logInfo (← env.find? `instBEqFOTerm).get!.value!.appArg!.constName!
-- _private.0.beqFOTerm._@._hyg.2488

#print _private.0.beqFOTerm._@._hyg.2488 -- more syntax fail

#eval show TermElabM Unit from do
  let env ← getEnv
  let n := (← env.find? `instBEqFOTerm).get!.value!.appArg!.constName!
  logInfo (← env.find? n).get!.value!
-- #0

-- The definition has no value?

#eval show TermElabM Unit from do
  let env ← getEnv
  let n := (← env.find? `instBEqFOTerm).get!.value!.appArg!.constName!
  let ConstantInfo.opaqueInfo d ← (← env.find? n).get! | panic! ""

-- it's opaque.. because it's a partial def
-- The actual definition isn't there, it's in an implementedBy that the compiler generated

#eval show TermElabM Unit from do
  let env ← getEnv
  let ci := Compiler.mkUnsafeRecName (← env.find? `instBEqFOTerm).get!.value!.appArg!.constName!
  let e := (← env.find? ci).get!.value!
  logInfo e

-- fun (x x_1 : FOTerm) =>
--   let localinst : BEq FOTerm := { beq := _unsafe_rec };
--   match x, x_1 with
--   | FOTerm.var a, FOTerm.var b => true && a == b
--   | FOTerm.app a a_1, FOTerm.app b b_1 => true && a == b && a_1 == b_1
--   | x, x_2 => false

-- success!

[Gabriel Ebner]

Do we need a sudo #print?

[Daniel Fabian]

I vote for #print_dammit :P

[Sebastian Ullrich]

Maybe not the answer you wanted, but I always use tracing instead of #printing a helper definition after the fact.

set_option trace.Elab.command true

Doesn't work from a different file of course.

[Mario Carneiro]

I think this story would have ended better if the name of the definition generated by the deriving instance was instBEqFOTerm.impl instead of _private.0.beqFOTerm._@._hyg.2488. Then I could have just written #print instBEqFOTerm.impl._unsafe_rec

[Mario Carneiro]

Here's the version pulled from trace.Elab.command:

[Elab.command] mutual
  set_option match.ignoreUnusedAlts✝ true
  private partial def beqFOTerm✝ (x✝ : @FOTerm) (x✝¹ : @FOTerm) : Bool✝ :=
    let localinst✝ : BEq (@FOTerm) := ⟨beqFOTerm✝⟩;
    match x✝, x✝¹ with
    | @FOTerm.var a✝, @FOTerm.var b✝ => true✝ && a✝ == b✝
    | @FOTerm.app a✝¹ a✝², @FOTerm.app b✝¹ b✝² => true✝ && a✝¹ == b✝¹ && a✝² == b✝²
    | _, _ => false✝
end

It's private and hygienic. That's like double private

[Mario Carneiro]

apparently there's even a hygienic set_option option?

[Mario Carneiro]

wait, even Bool✝ has a tombstone, that looks fishy

[Sebastian Ullrich]

This is before elaboration, so there is no telling whether Bool will be a global reference

[Sebastian Ullrich]

And yes, all idents in a quotation are hygiened. The set_option elaborator will remove the scopes again.