How to print shadowed declarations?

Stream: lean4

[Eric Rodriguez]

Take this code:

structure Box where
  a : Nat
  b : Nat
deriving BEq

#print instBEqBox -- { beq := beqBox✝ }

Turning on pp.sanitizeNames does let you access the underlying name of this, but this changes on the ngen and such like so we can't actually access it. It'd be really nice to print it so that I could modify the instance generated by deriving without having to rewrite the scaffolding.

[Eric Rodriguez]

I was told about open private here but I just can't get it to work. I am told that there is private declarations, but can't seem to figure out the syntax to actually do the opening.

[Mario Carneiro]

this is not a private declaration (well it is but that's not the problem because you are still in the same module as the declaration), it is a declaration with an inaccessible name. You can call #print if you construct the name manually:

import Lean
open Lean

structure Box where
  a : Nat
  b : Nat
deriving BEq

set_option pp.sanitizeNames false in
#print instBEqBox
-- def instBEqBox : BEq Box :=
-- { beq := beqBox.22 }

run_cmd Elab.Command.elabCommand <|←
  `(#print $(mkIdent (addMacroScope (← getMainModule) `beqBox 22)))
-- private def beqBox._@.Mathlib.Test._hyg.22 : Box → Box → Bool :=
-- fun x x_1 ↦
--   match x, x_1 with
--   | { a := a, b := a_1 }, { a := b, b := b_1 } => true && a == b && a_1 == b_1
--   | x, x_2 => false

[Mario Carneiro]

(The fact that several deriving instances produce global declarations with inaccessible names is a recurring source of issues, and I've been planning to write a PR to make them accessible for some time. For example this causes an issue if you want to prove that an autogenerated Ord or BEq instance is lawful.)

[Eric Rodriguez]

Thanks! This really does seem quite annoying. One thing I've been meaning to figure out is macro scopes - what are they and how should I use them?

[Robert Maxton]

They're the scope of a macro :p. That is, the 'jurisdiction' of a macro over names and definitions. When a new macro is begun (controlled I think primarily withNewMacroScope?), it gets to include its macro scope (which is apparently implemented as just a unique number, probably encoding nesting of macros?) into the name of all (parsing) variables it introduces; this enforces hygiene requirements.

[Robert Maxton]

ah, yeah, here: docs#Lean.MacroScope

[Robert Maxton]

So, in theory, you should introduce a new macro scope whenever there might be danger of name collision of parse variables. In practice I think it's not much used/handled for you when writing notation or simple macro_rules and elab_rules, but more involved elaborators pretty much all start with withNewMacroScope do, and also if you might collide with yourself (through a recursive call, for example) that should get a withNewMacroScope do as well.

[Eric Rodriguez]

Ahh, so that number 22 is a macro-scope in this case. It does seem odd to me because I feel like no macros have been involved here, but I guess (a) most things are macros in some way or another and (b) it's probably the macro scope of the deriving stuff. [Not sure whether multiple derivings would have same or different macro scopes, I guess it depends on the implementation...].

[Kyle Miller]

It's possible to make a command that prints the value after unfolding all inaccessible constants (i.e., the ones with macro scopes):

structure Box where
  a : Nat
  b : Nat
deriving BEq

open Lean Elab Command in
elab "#print_val " id:ident : command => do
  addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
  let c ← resolveGlobalConstNoOverloadWithInfo id
  let some d := (← getEnv).find? c | throwError "unknown identifier '{mkConst c}'"
  let some val := d.value? | throwError "no value for decl"
  let val ← liftTermElabM <| Meta.transform val
    (pre := fun e => do
      if let .const n .. := e.getAppFn' then
        if n.hasMacroScopes then
          if let some e' ← Meta.unfoldDefinition? e then
            return .visit e'
      return .continue)
  logInfo m!"{val}"

#print_val instBEqBox
/-
{
  beq := fun x x_1 ↦
    (fun motive x x_2 h_1 h_2 ↦ Box.casesOn x fun a b ↦ Box.casesOn x_2 fun a_1 b_1 ↦ h_1 a b a_1 b_1) (fun x x ↦ Bool)
      x x_1 (fun a a_1 b b_1 ↦ true && a == b && a_1 == b_1) fun x x ↦ false }
-/