Modification to type class resolution

[lecopivo]

I have modified the type class resolution a little bit to be able to synthesize instances of type (a : α) → C a bit better, see zulip discussion about it.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1ab739b.
There were no significant changes.

[Kha]

I think the bot got confused about your merge commit, the 1.5% TC resolution performance regression is statistically significant. Whether it is practically significant is a different question.

[lecopivo]

I see, I think I can make the modification a bit faster.

Currently, I'm making sure that certain keys are never added to the table. If such a key is queried over and over, it is modified every time and the modified key's answers are transformed back to non-modified form.

Caching out the key+answer modification can speed things up. Unfortunately, I'm not exactly sure how to do that.

[lecopivo]

Thanks a lot for adding this in. I can work with nightly builds again!

[lecopivo]

Inspecting some type class synthesis, I'm a bit unsure if the function hasUnusedArguments is doing the correct thing.

For example I'm getting unusedArgs here:

    [Meta.synthInstance.unusedArgs] ∀ (a : X), SciLean.IsSmooth fun h => G (h a) a✝
    has unused arguments, reduced type
      ∀ (a : X), SciLean.IsSmooth fun h => G (h a) a✝
    Transformer
      fun redf a => redf a

It does not look like that there is an unused argument. It does not break anything, it is just doing unnecessary work.

[leodemoura]

Inspecting some type class synthesis, I'm a bit unsure if the function hasUnusedArguments is doing the correct thing.

For example I'm getting unusedArgs here:

    [Meta.synthInstance.unusedArgs] ∀ (a : X), SciLean.IsSmooth fun h => G (h a) a✝
    has unused arguments, reduced type
      ∀ (a : X), SciLean.IsSmooth fun h => G (h a) a✝
    Transformer
      fun redf a => redf a

It does not look like that there is an unused argument. It does not break anything, it is just doing unnecessary work.

Could you please post the example that triggers the issue above?

[lecopivo]

mwe:

def is_smooth {α β} (f : α → β) : Prop := sorry

class IsSmooth {α β} (f : α → β) : Prop where
  (proof : is_smooth f)

instance identity : IsSmooth fun a : α => a := sorry
instance const (b : β) : IsSmooth fun a : α => b := sorry
instance swap (f : α → β → γ) [∀ a, IsSmooth (f a)] : IsSmooth (λ b a => f a b) := sorry
instance parm (f : α → β → γ) [IsSmooth f] (b : β) : IsSmooth (λ a => f a b) := sorry
instance comp (f : β → γ) (g : α → β) [IsSmooth f] [IsSmooth g] : IsSmooth (fun a => f (g a)) := sorry
instance diag (f : β → δ → γ) (g : α → β) (h : α → δ) [IsSmooth f] [∀ b, IsSmooth (f b)] [IsSmooth g] [IsSmooth h] : IsSmooth (λ a => f (g a) (h a)) := sorry

set_option trace.Meta.synthInstance true in
example (f : β → δ → γ) [IsSmooth f] (d : δ) : IsSmooth (λ (g : α → β) a => f (g a) d) := by infer_instance

[lecopivo]

The trace contains:

    [Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth fun g => f (g a) d
    has unused arguments, reduced type
      ∀ (a : α), IsSmooth fun g => f (g a) d
    Transformer
      fun redf a => redf a

[lecopivo]

Thanks a lot for fixing this!