Visualization of typeclass inference

Stream: lean4

[Tomas Skrivan]

I would like to have some visual representation of typeclass inference. I find myself spending more and more time debugging order of class instances and it is getting really annoying. The main thing I want to see are large branches that do not lead to an answer and identify the instance that started it. This usually means a wrong order of instances. Also visually encode the order in which the graph is traversed.

I'm thinking about adding a tracing option set_option trace.Meta.synthInstanceVis that would generate some kind of string representation of a directed graph of goals/answers, consumer/generator nodes and then send it to some graph visualization tool, thinking about pyvis.

Any tips on doing this? Or different approach?

Would it be possible to invoke the graph visualization automatically when I compile with lake? Maybe a good idea only for the in version of set_option as I do not want to accidentally spawn thousands of graph visualizations.

[Henrik Böving]

There is a (I believe graphviz based) visualization of solving a simple type class resolution goal in the "Tabled Typeclass Resolution" paper here: https://arxiv.org/abs/2001.04301 (page 11) but I don't know whether this was auto generated, if it was though it seems to me like your goal should already be solved?

[Tomas Skrivan]

Yes some thing like that would be great just different visual of it. I want to immediately see that the branch A1 from N2 node is a dead end and this should scale if I have hundreds or thousands of nodes. To skip the dead branch you should declare the parameter C before B. I'm doing lots of debugging that leads to just reordering of parameters in instance declarations.

[James Gallicchio]

Wondering if this could be a widget a la https://www.edayers.com/thesis/widgets

A graph visualization directly in VS Code would be super useful for some collections stuff I'm working on...

[Henrik Böving]

Yes this widget type of stuff has been discussed about before but I don't know about it's current status, however people are very much aware of the possiblity

[Tomas Skrivan]

Currently, I'm again debugging a total tangle of messy typeclasses and it is driving me crazy. I think I will look into how to generate text representation of the graph and then we can try to figure out the best way to visualize it.

[Tomas Skrivan]

I see two approaches:

1. Add a new tracing message like trace.Meta.synthInstance.tcGraph which would be just reformating of current messages so it is easier to parse and build the TC graph out of.
2. After TC is done, inspect the TC tables and spit out the nodes and edges into a file. Not sure if this approach gives you the information in which order is the graph traversed.

Any thoughts? Another better approach?

[Tomas Skrivan]

The only way I see these two approaches is to modify Lean 4 code. Any idea how to avoid that?