lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard
verified publisher icon leanprover

chore: clean up TC inference implementation

Open JovanGerb opened this issue 1 year ago • 1 comments

This PR optimizes the type class search algorithm

  • We don't want trace messages to slow down type class search when trace is not enabled, so I made sure none of these computations are executed unnecessarily. #4282

  • For any new goal, instantiateMVars (← inferType mvar) is computed at least twice in the current implementation. This is fixed. #4284

  • When passing around metavariable contexts, the current implementation uses a lot of withMCtx, which is unnecessary. I fixed it so that each MetavarContext only needs to be set once at a time. Additionally, I removed the explicit returning of MetavarContext in tryResolve and tryAnswer, because these can instead be passed more naturally through the MetaM state. #4286

  • The trace messages for Meta.synthInstance.tryResolve and Meta.synthInstance.resume and the main/outer trace message have the problem that they have instantiated metavariables in their message that have been assigned during the tryResolve or the tryAnswer or instantiating outParams. In isDefEq the same problem arises (you want to see the unification problem before the unification has happened) and there it is solved using withTraceNodeBefore. This has also been fixed, using either withTraceNodeBefore, or an explicit withMCtx. - one of the tests shows this change. #4285

  • mkTableKey has a redundant call to setMCtx, which I removed. #4281

  • Calls to instantiateMVars in trace messages are redundant, so I removed them. #4283

  • The unused function MapMetaM has been removed. #4287

The result is a noticeable improvement of TC search speed in Mathlib: 2.8%

JovanGerb avatar May 25 '24 12:05 JovanGerb

Mathlib CI status (docs):

leanprover-community-mathlib4-bot avatar May 25 '24 13:05 leanprover-community-mathlib4-bot

Closing as per reasoning in #4379

Kha avatar Aug 26 '24 08:08 Kha