finding all possible instances of a type class on a type

Stream: new members

[Rado Kirov]

Inspired by a type class diamond in #**Analysis I> I have been poking around the diagnostics tools

class A (α: Type) where
  a: Nat

class B (α: Type) extends A α where
  b: Nat

def makeB (α: Type) : B α := {a := 0, b := 0}

def makeBFromA (α: Type) [A α] : B α := {b := 0}

instance ANat : A Nat where
  a := 1

-- change to makeBFromA and observe evals
instance BNat : B Nat := makeB Nat

-- trouble with makeB f will not equial g
def f {α: Type} [inst: B α]: Nat := inst.a
def g {α: Type} [inst: A α]: Nat := inst.a
#eval f (α := Nat)
#eval g (α := Nat)

set_option diagnostics true
set_option trace.Meta.synthInstance true
set_option trace.Meta.synthInstance.instances true in
#synth A Nat

What I can't seem to find is how to configure #synth to do a more exhaustive search (not just stop at the first instance), and hence predict the problem that there are two instances before I had to write f and g. Basically, I want something that shows 2 possible instances of A Nat when I use makeB, but 1 possible instance of A Nat when I use makeBfromA. Does such config exist?

[Aaron Liu]

probably not

[Aaron Liu]

maybe you can see what Qq does with assumeInstancesCommute