All instances satisfied by a type

Stream: mathlib4

[David Loeffler]

Is there a way of getting a list of all the typeclass instances that Lean is able to synthesize for a given type? (This is for a mini-course lecture about Lean's algebra hierarchy.)

E.g. if I have {R : Type} [CommRing R], then R obviously satisfies all of the simpler typeclasses that CommRing inherits from, and one can assemble a list of these by inspecting the definitions (there are 37 of them, including CommRing itself, if I'm not mistaken). But that isn't everything: there are some typeclasses (such as NonUnitalCommRing or AddCancelMonoid) that aren't direct ancestors of CommRing but can still be synthesised from it via explicitly-declared instances. Is there a way to assemble a list of these?

[Edward van de Meent]

should this count Module R R as an instance? how about Algebra R R?

[David Loeffler]

Edward van de Meent said:

should this count Module R R as an instance? how about Algebra R R?

Good point; let me say I'm only interested in typeclasses taking a single type argument.

[Edward van de Meent]

i think this should be doable... go through all names available in the environment, filter to those who have a single type argument and are classes, try to synthesise an instance when having specified only the argument to the command, if that succeeds put it on the list?

[Edward van de Meent]

not sure if it would be performant tho

[David Loeffler]

Edward van de Meent said:

i think this should be doable... go through all names available in the environment, filter to those who have a single type argument and are classes, try to synthesise an instance when having specified only the argument to the command, if that succeeds put it on the list?

I tried doing something like that myself, but I'm not sufficiently familiar with Lean metaprogramming to get it to work.

[Daniel Weber]

This works:

import Mathlib
import Lean

open Lean Elab Command Meta Term

variable {α : Type u} [CommRing α]

elab "#list_instances" var:term : command => runTermElabM fun xs => do
  let vvar ← elabTerm var none
  let ce := classExtension.getState (← getEnv)
  let mut answers := #[]
  for (a, _) in ce.outParamMap do
    let const ← getConstInfo a
    match const.type with
    | .forallE _ (.sort _) (.sort _) _ =>
      let mut exp : Expr := default
      try
        exp ← mkAppM a #[vvar]
      catch _ => continue
      let some synthed ← synthInstance? exp | continue
      answers := answers.push (a, synthed, exp)
    | _ => pure ()
  answers := answers.qsort (·.1.lt ·.1)
  for (_, synthed, exp) in answers do
    logInfo m!"{synthed} : {exp}"

#list_instances α

[Damiano Testa]

If you use

elab "#list_instances" var:term : command => runTermElabM fun xs => do
  let vvar ← elabTerm var none
  let ce := classExtension.getState (← getEnv)
  let mut insts := #[]
  for (a, _) in ce.outParamMap do
    let const ← getConstInfo a
    match const.type with
    | .forallE _ (.sort _) (.sort _) _ =>
      let mut exp : Expr := default
      try
        exp ← mkAppM a #[vvar]
      catch _ => continue
      let some synthed ← synthInstance? exp | continue
      insts := insts.push (synthed, exp)
    | _ => pure ()
  let (_, sorted) := ((← insts.mapM fun e => return (← ppExpr e.2).pretty).zip insts).qsort (·.1 < ·.1) |>.unzip
  logInfo <| MessageData.joinSep (sorted.toList.map fun (synthed, expr) => m!"'{expr}' (via '{synthed}')") "\n"

then you can sort them by the name of the class, which may be useful.

[Edward van de Meent]

fwiw, this seems like a nice thing to PR to batteries or something, perhaps under the moniker of #print instances or #help instances?