Widget for visualizing typeclass instances?

Stream: mathlib4

[Jon Bannon]

I was thinking it might be nice for many purposes to have a widget that allows one to visualize a graph of the instances within a file in a way that can be expanded by clicking on nodes. Does such a thing exist anywhere?

[Eric Wieser]

Can you give an example of an instance and what you'd want to visualize about it?

[Jon Bannon]

I'm asking mostly because I've wanted some way to quickly visualize typeclasses in introductory talks, but recently found myself looking to reduce an overly strong typeclass inference in a file, and so unpacked this instance into its constituent parts and started sorting the various results I was proving according to the minimal assumptions necessary.

For a primitive example, we might have OrderedSemiring α that extends Semiring α and OrderedAddCommMonoid α. If we only take the extends keyword to indicate adjacency, we would get a pretty simple directed graph. One could then click on the individual notes to extend them further. This is probably too primitive, though. It may be a good idea to include more than just the extends keyword...maybe one would want to link to all instances that appear in the declaration of [OrderedSemiring α]...I am not sure what I am saying here is clear, though, sorry.

I was kind of wondering if there was a well-known tool that allowed one to look at the interdependencies of instances to aid in "pruning" and reorganizing assumptions. If this was doable, I figured something was bound to exist.

[Jon Bannon]

I just found this old post: https://leanprover-community.github.io/archive/stream/270676-lean4/topic/Visualization.20of.20typeclass.20inference.html

[Jon Bannon]

I thought I had seen something like this before. There is an example of the kind of thing I'm looking for in this paper : https://arxiv.org/pdf/2001.04301