Searching for type class instances

Stream: new members

[J. Ryan Stinnett]

Is there a way to see a list of instances for a given type class...? Maybe some way in Loogle or the standard library docs? It would be helpful as someone new to the language to see a list of type class instances, as that would make it clear that they have so many different applications.

[Yaël Dillies]

Hey :wave: yes there is. Any specific typeclass you would like to know instances of?

[J. Ryan Stinnett]

Ah great! Not particularly, feel free to use any type class as an example... I am still quite new to the language, so I only really know about the "foundational" ones like Monad and such that are mentioned in the FP in Lean book so far.

[Yaël Dillies]

If you click on docs#Monad, you can uncollapse "Instances" at the bottow, which contains the info you want

[J. Ryan Stinnett]

Ah okay, thanks! :smile: I guess the related "Instances For" list that some other items have in the docs shows all instances of different type classes that might be implemented for that item.

[Kyle Miller]

If you import Batteries.Tactic.Instances, it gives the #instances command, which you can use to print out every instance that could potentially apply, given enough additional instances. For example:

import Mathlib
import Batteries.Tactic.Instances -- optional, implied by Mathlib

#instances Monad Option
/-
4 instances:

instMonadOption.{u_1} : Monad Option
AlternativeMonad.toMonad.{u_1, u_2} {m : Type u_1 → Type u_2} [self : AlternativeMonad m] : Monad m
Std.Internal.IO.Async.MonadAsync.toMonad (t : Type → Type) {m : Type → Type}
  [self : Std.Internal.IO.Async.MonadAsync t m] : Monad m
Std.Internal.IO.Async.MonadAwait.toMonad (t : Type → Type) {m : Type → Type}
  [self : Std.Internal.IO.Async.MonadAwait t m] : Monad m
-/

(The last two are probably irrelevant!)

If you do #instances Monad, it's the same as #instances Monad _, and that shows all instances, like in docs#Monad.

The #synth command can also be useful. It tries to actually synthesize an instance, but if it fails to fully synthesize an instance it fails to report anything. (It'd be neat if it would try diagnosing why not. Maybe one day!)

The difference between #instances and #synth is that #instances is "one-step" of #synth. It reports all the instances that instance synthesis would use of for the given instance.

[Kyle Miller]

The #instances command is sort of a convenience, since the information is all available if you enable the right trace class and know where to look:

import Mathlib

set_option trace.Meta.synthInstance true

#synth Monad Option
/-
[Meta.synthInstance] ✅️ Monad Option ▼
  [] new goal Monad Option ▼
    [instances] #[Std.Internal.IO.Async.MonadAwait.toMonad, Std.Internal.IO.Async.MonadAsync.toMonad, @AlternativeMonad.toMonad, instMonadOption]
  [] ✅️ apply instMonadOption to Monad Option ▶
  [] result instMonadOption
-/

Instead of #instances Monad, you have to write #synth Monad _.

[J. Ryan Stinnett]

Ah okay, thanks for those additional tips! :smile: I wonder what other helpful commands similar to #instances are out there...