leanprover/lean4

Instance search continues even when an instance was found after a later instance could not be found

Closed this issue · 1 comments

MichaelStollBayreuth commented

Prerequisites

  • Put an X between the brackets on this line if you have done all of the following:
    • Check that your issue is not already filed.
    • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

When an instance of the form instance [A] [B] : C is applied in the course of searching an instance C and an instance A is found, but then no instance B is found, instance search for A is resumed.

Context

This causes many failing instance searches in Mathlib to take a long time (because it has the effect of exploring the full search tree even for instances that could be found quickly).

See here, here and here on Zulip.

Steps to Reproduce

class A where

class B (n : Nat) where

class C where

instance test [B 10000] [C] : A where

instance Bsucc {n : Nat} [B n] : B n.succ where

instance instB0 : B 0 where

instance instB10000 : B 10000 where

set_option trace.Meta.synthInstance true

#synth A

The trace shows that

  • test is applied to find an instance for A
  • instB10000 is applied to find an instance for B 10000
  • then no instance for C is found
  • then the search for B 10000 is resumed, causing the recursive application of 10000 versions of Bsucc

Expected behavior:

I expect that in the example the typeclass search would fail immediately after no instance for C is found.
Rationale: We know an instance for B 10000 exists, so further search is unncecessary and cannot possibly make an instance for C appear.

Actual behavior:

After failing to find an instance of C, the search for B 10000 is resumed, leading to a long and useless computation.

Versions

4.7.0 / Linux

Impact

Typeclass search accounts for over 1/3 of Mathlib building time. The behavior described here is likely responsible for a large part of this time. Fixing it would therefore speed up Mathlib considerably.

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

MichaelStollBayreuth commented

Here is an example where instance synthesis fails while it should succeed.

class A where
class B (n : Nat) where
class C where

instance test' [B 10] : A where
instance test [B 0] [C] : A where
instance foo {n : Nat} [B n.succ] : B n where
instance instB (n : Nat) : B n where

set_option trace.Meta.synthInstance true
#synth A

It gets stuck trying (and infinitely often failing) to establish A via test and never gets to trying test'.