Reduce during typeclass search

Stream: metaprogramming / tactics

[Markus de Medeiros]

Is there some way to make Lean reduce terms while doing typeclass search? I was doing some logic programming using typeclasses, for no real reason aside from seeing if it was possible, and was wondering if there was some hidden option somewhere which might make the typechecker reduce before it looks for matching instances?

class Reflect (b : outParam Bool) where is_true : b
instance : Reflect true := ⟨ rfl ⟩
#synth Reflect (5 == 5) -- It can synthesize an instance for Reflect (5 == 5) when it reduces first

class ReflectClient (n1 n2 : Nat) where
instance {n1 n2 : Nat} [Reflect (n1 == n2)] : ReflectClient n1 n2 where

-- set_option trace.Meta.synthInstance true
-- check #synth ReflectClient 5 5
-- [Meta.synthInstance] ❌️ ReflectClient 5 5
--   [Meta.synthInstance] new goal ReflectClient 5 5
--     [Meta.synthInstance.instances] #[@instReflectClientOfReflectBeqNat]
--   [Meta.synthInstance] ✅️ apply @instReflectClientOfReflectBeqNat to ReflectClient 5 5
--     [Meta.synthInstance.tryResolve] ✅️ ReflectClient 5 5 ≟ ReflectClient 5 5
--     [Meta.synthInstance] no instances for Reflect (5 == 5)   -- Doesn't reduce so doesn't find an instance
--       [Meta.synthInstance.instances] #[]
--   [Meta.synthInstance] result <not-available>

[Robin Arnez]

Two things are needed here:

1. instance : Reflect (no_index true) := ⟨rfl⟩. Without no_index it will only consider this instance if it's already true before reduction
2. Use more reducible functions like n1.beq n2

I have honestly no clue why the first one succeeded lol

[Robin Arnez]

I think the first one succeeding is not typeclass search doing something but the #synth command doing something special

[Kyle Miller]

Gabriel Ebner pointed out this trick awhile ago:

class When (p : Prop) [Decidable p] : Prop where
  isTrue : p

instance : @When p (.isTrue h) := @When.mk p (.isTrue h) h

This allows adding [When (m < n)] instances for example.

This works because Lean does more reduction for implicit arguments. Maybe you can make use of this somehow?

[Robin Arnez]

This needs no_index as well though, no?

[Robin Arnez]

Hmm no? Weird

[Robin Arnez]

Oh it's an instance argument

[Robin Arnez]

Yeah, makes sense

[Edward van de Meent]

this seems similar to Fact for some reason...

[Edward van de Meent]

but i guess it's different (crucially for this topic) due to the instance argument in the type

[Markus de Medeiros]

The When trick seems to work! Super clever, thanks all :)