List of instances

Stream: lean4

[Henrik Böving]

Is it possible to, for a given type class Name, figure out a list of all instance declarations that can possibly result in an instance of it? I've tried:

let insts <- SynthInstance.getInstances (mkConst v.name (v.levelParams.map mkLevelParam))

so far, but this always results in an empty list of instances so I suspect I'm doing something wrong here...

[Gabriel Ebner]

You need to add metavariables:

import Lean
open Lean Meta

#eval show MetaM _ from do
  let fn ← mkConstWithFreshMVarLevels ``Inhabited
  let (xs, _, _) ← forallMetaTelescopeReducing (← inferType fn)
  SynthInstance.getInstances (mkAppN fn xs)

[Gabriel Ebner]

The argument to getInstances should be Inhabited.{?u} ?ty.

[Henrik Böving]

That did indeed work out, thanks!

Another question in this case, I've seen this Telescope thing being mentioned in a few functions while reading parts of the compiler code and I don't really know what a telescope is supposed to be in this context? Is there somewhere where I could read about that?

[Jannis Limperg]

A telescope is a list of terms (here often local constants) where the types of later terms may refer to earlier terms. E.g. x : Nat, y : Fin x, z : x > 0. When you open a type starting with n quantifiers, or a term starting with n lambdas, you get a telescope with n arguments plus the body, which may refer to each term in the telescope.

[Henrik Böving]

Ah and the reducing functions take a telescope and produce some sort of value from it?

[Gabriel Ebner]

No, "reducing" here means unfold definitions etc. That is, id (Type → Type → Type) would get you two terms with reducing, but zero terms without reducing.

[Henrik Böving]

Whenever I feel like I finally understood what's going on something new comes around :stuck_out_tongue:.

[Kevin Buzzard]

that happens in math too

[Sebastian Reichelt]

Now that I learned that getInstances exists, I have a question about it as well. Since getInstances returns raw constants without arguments, is there a convenient way to add arguments to each result? Or, in other words, is it possible to have a version of synthInstance that returns multiple results? I'm not sure if the question even makes sense because I suppose the resulting list isn't guaranteed to be finite... What I'm really trying to achieve is to have a tactic look at multiple candidates of instances and select one of them, and I'm wondering about the best way to achieve this. I guess the pedestrian solution would be to introduce a chaining mechanism into the type class itself, but if I can just query all instances, I'd prefer that.