why `dbg_trace` needs `ToString` instance?

Stream: lean4

[Asei Inoue]

Why do we need ToString instances for debugging?

[Chris Bailey]

Is the question why it specifically needs to be the ToString class, or why there needs to be a class instance at all? dbg_trace just prints stuff, so it needs to know how to print the elements being traced. It would be possible to just fall back to printing the Expr representation and not require any further direction, but always getting the pp.all version of terms is frequently going to be more noisy than helpful.

[Asei Inoue]

inductive Foo where
  | intro

def zero (f : Foo) : Nat :=
  -- failed to synth ToString
  dbg_trace f
  0

[Asei Inoue]

My thought is that if the instance for debugging is a ToString, you have to manually create a ToString instance every time you want to debug.
If you can use Repr, I think there are situations where that would be fine, and you could automatically create ToString instances from Repr.

[Edward van de Meent]

this could be a default instance:

instance [Repr Foo] : ToString Foo := {
  toString := reprStr
}

[Asei Inoue]

It would be good if deriving ToString could be done.
Since deriving Repr can be done, it should be possible to generate it with reprStr from Repr.

[Chris Bailey]

I see. Apparently some kind of "try X then fall back to Y" behavior was recently added for the way eval is printed (https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Repr.20vs.20ToString/near/479062655), maybe it would be desirable to add that to dbg_trace, in this case locally doing "try to use ToString, if you can't' find an instance of it, look for Repr and use reprStr instead" since it doesn't have the parsing/round-trip concerns of eval.

[Kyle Miller]

One difference between dbg_trace and #eval is that #eval is able to fully elaborate its argument before doing its instance synthesis logic. With dbg_trace, it might need to postpone things, which makes things tricker.

However, it would be nice to not have to worry about synthesizing ToString/Repr instances just to debug. Sebastian and I have talked a little bit about this, and there's no obvious obstruction (other than compiler performance impacts).

Relatedly, something that I've wondered with #eval is whether it would be desirable to have it print unprintable subterms using syntax like (⋯ : Nat -> Bool). On one hand, this is a lot better since often there can be terms you want to understand but not all of it is printable. On the other, it might get in the way of auto-derive feature of #eval (it currently has logic to do one level of trying to derive a Repr instance automatically).

[Asei Inoue]

However, it would be nice to not have to worry about synthesizing ToString/Repr instances just to debug.

Yes!