simproc patterns tries to synth instances

Stream: metaprogramming / tactics

[Robin Carlier]

Consider

import Lean.Elab.Tactic.Simproc

class TestCompStruct (obj : Type u) : Type (max u (v + 1)) where
  Hom : obj → obj → Type v
  comp : ∀ {X Y Z : obj}, Hom X Y → Hom Y Z → Hom X Z

/--
error: failed to synthesize instance of type class
  TestCompStruct ?m.1

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
simproc sp_test (TestCompStruct.comp _ _) := fun _ => return .continue

/--
error: failed to synthesize instance of type class
  TestCompStruct ?m.1

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
simproc sp_test' (@TestCompStruct.comp _ _ _ _ _ _ _) := fun _ => return .continue

Am I doing something wrong here? Since the "obj" remains uninfered, no instance can be synthesized for it of course, but is it normal that the simproc pattern tries to synth instances
at this stage?

[Robin Carlier]

Ah, nevermind, found it!

simproc single_simproc_explicit'' (TestCompStruct.comp (self := _) _ _) := fun _ => return .continue

works (and seems to fire on the right pattern)

[Robin Arnez]

Yeah this seems like a bug since this doesn't occur for other type classes. One fix is the one you said, another one is:

simproc sp_test' (@TestCompStruct.comp _ (_) _ _ _ _ _) := fun _ => return .continue

(i.e. marking instance arguments as (_) to avoid triggering the special instance synthesis behavior)

[Robin Carlier]

I will file an issue during the weekend then