perf: cache for isDefEqI in Sym

This PR caches `isDefEqI` results in `Sym`. During symbolic
computation (e.g., VC generators), we find the same instances over and over again.

Performance numbers before/after fr the benchmark
`tests/bench/mvcgen/sym/vcgen_deep_add_sub_cancel.lean`.

| Benchmark | Before (ms) | After (ms) | Speedup |
|-----------|------------|------------|---------|
| goal_100  | 192.1      | 134.1      | 30%     |
| goal_200  | 325.6      | 225.4      | 31%     |
| goal_300  | 490.2      | 333.5      | 32%     |
| goal_400  | 655.6      | 441.9      | 33%     |
| goal_500  | 861.9      | 553.1      | 36%     |
| goal_600  | 1060.6     | 664.5      | 37%     |
| goal_700  | 1166.8     | 818.7      | 30%     |
| goal_800  | 1393.3     | 919.0      | 34%     |
| goal_900  | 1524.2     | 1025.0     | 33%     |
| goal_1000 | 1663.1     | 1141.9     | 31%     |

The time does not include the kernel type checking time. The
optimization does not affect it.

src/Init/Notation.lean

@@ -654,33 +654,11 @@ syntax (name := suggest_for) "suggest_for" (ppSpace ident)+ : attr
 /--
 The attribute `@[univ_out_params ..]` on a class specifies the universe output parameters.
 
-* `@[univ_out_params]` means the class has no universe output parameters.
+* `@[univ_out_params]` means the class does not have universe output parameters.
 * `@[univ_out_params u v]` means the universes `u` and `v` are output parameters.
 
-If this attribute is not present, Lean assumes that any universe parameter which does not
-occur in any input parameter type is an output parameter.
-
-### Effect on typeclass resolution
-
-When typeclass resolution begins, output universe parameters are replaced with fresh universe
-metavariables, similar to what is done for regular output parameters. This means the search
-proceeds without being constrained by the specific output universes in the query, and the
-actual output universes are determined by the instance that is found.
-
-As a consequence, output universe parameters are erased from typeclass resolution cache keys.
-Two queries that differ only in output universe parameters will share a cache entry,
-and the first result found will be reused for subsequent queries.
-
-### When to use this attribute
-
-The default heuristic is wrong when the universe is
-part of the *question* being asked, rather than something determined by the answer.
-
-For example, in `class Foo.{u} (C : Type v)` where `u` specifies "how large" some auxiliary
-data is, different values of `u` give genuinely different conditions on `C`. By default `u`
-would be treated as output since it does not appear in `C : Type v`, and the cache would
-conflate `Foo.{0} C` with `Foo.{1} C`, returning the wrong instance.
-Use `@[univ_out_params]` to mark that no universe parameter is output.
+If the type declaration does not contain this attribute, then Lean assumes that universe
+parameter that does not occur in any input parameter is an output one.
 -/
 syntax (name := univ_out_params) "univ_out_params" (ppSpace ident)* : attr
 

src/Lean/Compiler/InitAttr.lean

@@ -161,9 +161,7 @@ def declareBuiltin (forDecl : Name) (value : Expr) : CoreM Unit :=
 @[export lean_run_init_attrs]
 private unsafe def runInitAttrs (env : Environment) (opts : Options) : IO Unit := do
   if (← isInitializerExecutionEnabled) then
-    -- **Note**: `ModuleIdx` is not an abbreviation, and we don't have instances for it.
-    -- Thus, we use `(modIdx : Nat)`
-    for mod in env.header.moduleNames, (modIdx : Nat) in 0...* do
+    for mod in env.header.moduleNames, modIdx in 0...* do
       -- any native Lean code reachable by the interpreter (i.e. from shared
       -- libraries with their corresponding module in the Environment) must
       -- first be initialized

src/Lean/Elab/Deriving/Basic.lean

@@ -124,24 +124,7 @@ private partial def mkInst (classExpr : Expr) (declName : Name) (declVal val : E
       -- Success
       trace[Elab.Deriving] "Argument {i} option succeeded{indentExpr classExpr}"
       -- Create the type for the declaration itself.
-      -- Construct the instance type using the target (alias) type's instances.
-      -- For each instance-implicit parameter, synthesize the instance for the target type
-      -- and verify it is defeq to the one synthesized for the underlying type.
-      -- This behaves as if the user wrote `instance : Cls T := inferInstanceAs (Cls T')`.
-      let mut xs' := xs.set! i declVal
-      for j in [:xs'.size], bi in bis do
-        if bi.isInstImplicit then
-          let origInst ← instantiateMVars xs[j]!
-          let argTy ← instantiateMVars (← inferType xs[j]!)
-          let targetArgTy := argTy.replace fun e =>
-            if e == val then declVal else none
-          if let some targetInst ← synthInstance? targetArgTy then
-            unless ← isDefEq origInst targetInst do
-              throwDeltaDeriveFailure className declName
-                (m!"instance diamond: the instance for the target type\
-                  {indentExpr targetInst}\nis not definitionally equal to the instance for the underlying type\
-                  {indentExpr origInst}\nfor{indentExpr targetArgTy}")
-            xs' := xs'.set! j targetInst
+      let xs' := xs.set! i declVal
       let instType := mkAppN cls xs'
       return { instType, instVal }
     try

src/Lean/Meta/SynthInstance.lean

@@ -6,6 +6,7 @@ Authors: Daniel Selsam, Leonardo de Moura
 Type class instance synthesizer using tabled resolution.
 -/
 module
+
 prelude
 public import Init.Data.Array.InsertionSort
 public import Lean.Meta.Instances
@@ -14,6 +15,7 @@ public import Lean.Meta.Check
 import Init.While
 
 public section
+
 namespace Lean.Meta
 
 register_builtin_option synthInstance.maxHeartbeats : Nat := {
@@ -186,7 +188,7 @@ structure State where
   result?        : Option AbstractMVarsResult    := none
   generatorStack : Array GeneratorNode           := #[]
   resumeStack    : Array (ConsumerNode × Answer) := #[]
-  tableEntries   : Std.HashMap Expr TableEntry   := {}
+  tableEntries   : Std.HashMap Expr TableEntry       := {}
 
 abbrev SynthM := ReaderT Context $ StateRefT State MetaM
 
@@ -659,120 +661,43 @@ If it succeeds, and metavariables ?m_i have been assigned, we try to unify
 the original type `C a_1 ... a_n` with the normalized one.
 -/
 
-/-- Result kind for `preprocess` -/
-private inductive PreprocessKind where
-  | /--
-    Target type does not have metavariables.
-    We use the type to construct the cache key even if the class has output parameters.
-    Reason: we want to avoid the normalization step in this case.
-    -/
-    noMVars
-  | /-- Target type has metavariables, and class does not have output parameters. -/
-    mvarsNoOutputParams
-  | /-- Target type has metavariables, and class has output parameters. -/
-    mvarsOutputParams
+private def preprocess (type : Expr) : MetaM Expr :=
+  forallTelescopeReducing type fun xs type => do
+    let type ← whnf type
+    mkForallFVars xs type
 
-/-- Return type for `preprocess` -/
-private structure PreprocessResult where
-  type         : Expr
-  cacheKeyType : Expr := type
-  kind         : PreprocessKind
+private partial def preprocessArgs (type : Expr) (i : Nat) (args : Array Expr) (outParamsPos : Array Nat) : MetaM (Array Expr) := do
+  if h : i < args.size then
+    let type ← whnf type
+    match type with
+    | .forallE _ d b _ => do
+      let arg := args[i]
+      /-
+      We should not simply check `d.isOutParam`. See `checkOutParam` and issue #1852.
+      If an instance implicit argument depends on an `outParam`, it is treated as an `outParam` too.
+      -/
+      let arg ← if outParamsPos.contains i then mkFreshExprMVar d else pure arg
+      let args := args.set i arg
+      preprocessArgs (b.instantiate1 arg) (i+1) args outParamsPos
+    | _ =>
+      throwError "type class resolution failed, insufficient number of arguments" -- TODO improve error message
+  else
+    return args
 
-/--
-Returns `{ type, cacheKeyType, hasOutParams }`, where `type` is the normalized type, and `cacheKeyType`
-is part of the key for the type class resolution cache. If the class associated with `type`
-does not have output parameters, then, `cacheKeyType` is `type`.
-If it has, we replace arguments corresponding with output parameters with wildcard terms.
-
-For example, the cache key for a query like
-`HAppend.{0, 0, ?u} (BitVec 8) (BitVec 8) ?m` should be independent of the specific
-metavariable IDs in output parameter positions. To achieve this, output parameter arguments
-are erased from the cache key. However, universe levels that only appear in output parameter
-types (e.g., `?u` corresponding to the result type's universe) must also be erased to avoid
-cache misses when the same query is issued with different universe metavariable IDs.
--/
-private def preprocess (type : Expr) : MetaM PreprocessResult :=
-  let keyExprWildcard := mkFVar { name := `__wild__  }
-  let keyLevelWildcard := mkLevelParam `__wild__
-  forallTelescopeReducing type fun xs typeBody => do
-    let typeBody ← whnf typeBody
-    let type ← mkForallFVars xs typeBody
-    if !type.hasMVar then return { type, kind := .noMVars }
-    /-
-    **Note**: Workaround for classes such as `class ToLevel.{u}`. They do not have any parameters,
-    the universe parameter inference engine at `Class.lean` assumes `u` is an output parameter,
-    but this is not correct. We can remove this check after we update `Class.lean` and perform an
-    update stage0
-    -/
-    if typeBody.isConst then return { type, kind := .mvarsNoOutputParams }
-    let c := typeBody.getAppFn
-    let .const declName us := c | return { type, kind := .mvarsNoOutputParams }
-    let env ← getEnv
-    let some outParamsPos := getOutParamPositions? env declName | return { type, kind := .mvarsNoOutputParams }
-    let some outLevelParamPos := getOutLevelParamPositions? env declName | unreachable!
-    if outParamsPos.isEmpty && outLevelParamPos.isEmpty then return { type, kind := .mvarsNoOutputParams }
-    let c := if outLevelParamPos.isEmpty then c else
-      let rec normLevels (us : List Level) (i : Nat) : List Level :=
-        match us with
-        | [] => []
-        | u :: us =>
-          let u := if i ∈ outLevelParamPos then keyLevelWildcard else u
-          u :: normLevels us (i+1)
-      mkConst declName (normLevels us 0)
-    let rec norm (e : Expr) (i : Nat) : Expr :=
-      match e with
-      | .app f a =>
-        let a := if i ∈ outParamsPos then keyExprWildcard else a
-        mkApp (norm f (i-1)) a
-      | _ => c
-    let typeBody := norm typeBody (typeBody.getAppNumArgs - 1)
-    let cacheKeyType ← mkForallFVars xs typeBody
-    return { type, cacheKeyType, kind := .mvarsOutputParams }
-
-private partial def preprocessOutParam (type : Expr) : MetaM Expr :=
+private def preprocessOutParam (type : Expr) : MetaM Expr :=
   forallTelescope type fun xs typeBody => do
-    /- **Note**: See similar test at preprocess. -/
-    if typeBody.isConst then return type
-    let c := typeBody.getAppFn
-    let .const declName us := c | return type
-    let env ← getEnv
-    let some outParamsPos := getOutParamPositions? env declName | return type
-    let some outLevelParamPos := getOutLevelParamPositions? env declName | unreachable!
-    if outParamsPos.isEmpty && outLevelParamPos.isEmpty then return type
-    let c ← if outLevelParamPos.isEmpty then pure c else
-      -- Replace universe parameters corresponding to output parameters with fresh universe metavariables.
-      let rec preprocessLevels (us : List Level) (i : Nat) : MetaM (List Level) := do
-        match us with
-        | [] => return []
-        | u :: us =>
-          let u ← if i ∈ outLevelParamPos then mkFreshLevelMVar else pure u
-          let us ← preprocessLevels us (i+1)
-          return u :: us
-      pure <| mkConst declName (← preprocessLevels us 0)
-    let rec preprocessArgs (type : Expr) (i : Nat) (args : Array Expr) : MetaM (Array Expr) := do
-      if h : i < args.size then
-        let type ← whnf type
-        match type with
-        | .forallE _ d b _ => do
-          let arg := args[i]
-          /-
-          We should not simply check `d.isOutParam`. See `checkOutParam` and issue #1852.
-          If an instance implicit argument depends on an `outParam`, it is treated as an `outParam` too.
-          -/
-          let arg ← if outParamsPos.contains i then mkFreshExprMVar d else pure arg
-          let args := args.set i arg
-          preprocessArgs (b.instantiate1 arg) (i+1) args
-        | _ =>
-          throwError "type class resolution failed, insufficient number of arguments" -- TODO improve error message
-      else
-        return args
-    let args := typeBody.getAppArgs
-    if outParamsPos.isEmpty then
-      mkForallFVars xs (mkAppN c args)
-    else
-      let cType ← inferType c
-      let args ← preprocessArgs cType 0 args
-      mkForallFVars xs (mkAppN c args)
+    match typeBody.getAppFn with
+    | c@(.const declName _) =>
+      let env ← getEnv
+      if let some outParamsPos := getOutParamPositions? env declName then
+        unless outParamsPos.isEmpty do
+          let args := typeBody.getAppArgs
+          let cType ← inferType c
+          let args ← preprocessArgs cType 0 args outParamsPos
+          return (← mkForallFVars xs (mkAppN c args))
+      return type
+    | _ =>
+      return type
 
 /-!
   Remark: when `maxResultSize? == none`, the configuration option `synthInstance.maxResultSize` is used.
@@ -781,21 +706,9 @@ private partial def preprocessOutParam (type : Expr) : MetaM Expr :=
 
 private def assignOutParams (type : Expr) (result : Expr) : MetaM Bool := do
   let resultType ← inferType result
-  /-
-  Output parameters of local instances may be marked as `syntheticOpaque` by the application-elaborator.
-  We use `withAssignableSyntheticOpaque` to make sure this kind of parameter can be assigned by the following `isDefEq`.
-  TODO: rewrite this check to avoid `withAssignableSyntheticOpaque`.
-
-  **Note**: We tried to remove `withDefault` at the following `isDefEq` because it was a potential performance footgun. TC is supposed to unfold only `reducible` definitions and `instances`.
-  We reverted the change because it triggered thousands of failures related to the `OrderDual` type. Example:
-  ```
-  variable {ι : Type}
-  def OrderDual (α : Type) : Type := α
-  instance [I : DecidableEq ι] : DecidableEq (OrderDual ι) := inferInstance -- Failure
-  ```
-  Mathlib developers are currently trying to refactor the `OrderDual` declaration,
-  but it will take time. We will try to remove the `withDefault` again after the refactoring.
-  -/
+  /- Output parameters of local instances may be marked as `syntheticOpaque` by the application-elaborator.
+      We use `withAssignableSyntheticOpaque` to make sure this kind of parameter can be assigned by the following `isDefEq`.
+      TODO: rewrite this check to avoid `withAssignableSyntheticOpaque`. -/
   let defEq ← withDefault <| withAssignableSyntheticOpaque <| isDefEq type resultType
   unless defEq do
     trace[Meta.synthInstance] "{crossEmoji} result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
@@ -856,18 +769,15 @@ private def applyCachedAbstractResult? (type : Expr) (abstResult? : Option Abstr
     applyAbstractResult? type abstResult?
 
 /-- Helper function for caching synthesized type class instances. -/
-private def cacheResult (cacheKey : SynthInstanceCacheKey) (kind : PreprocessKind) (abstResult? : Option AbstractMVarsResult) (result? : Option Expr) : MetaM Unit := do
-  -- **TODO**: simplify this function.
-  match abstResult? with
+private def cacheResult (cacheKey : SynthInstanceCacheKey) (abstResult? : Option AbstractMVarsResult) (result? : Option Expr) : MetaM Unit := do
+  match result? with
   | none => modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey none }
-  | some abstResult =>
-    if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty && kind matches .noMVars | .mvarsNoOutputParams then
-      match result? with
-      | none => modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey none }
-      | some result =>
-        -- See `applyCachedAbstractResult?` If new metavariables have **not** been introduced,
-        -- we don't need to perform extra checks again when reusing result.
-        modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some { expr := result, paramNames := #[], mvars := #[] }) }
+  | some result =>
+    let some abstResult := abstResult? | return ()
+    if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty then
+      -- See `applyCachedAbstractResult?` If new metavariables have **not** been introduced,
+      -- we don't need to perform extra checks again when reusing result.
+      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some { expr := result, paramNames := #[], mvars := #[] }) }
     else
       modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some abstResult) }
 
@@ -881,44 +791,20 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met
   withInTypeClassResolution do
     let localInsts ← getLocalInstances
     let type ← instantiateMVars type
-    let { type, cacheKeyType, kind } ← preprocess type
-    let cacheKey := { localInsts, type := cacheKeyType, synthPendingDepth := (← read).synthPendingDepth }
+    let type ← preprocess type
+    let cacheKey := { localInsts, type, synthPendingDepth := (← read).synthPendingDepth }
     match (← get).cache.synthInstance.find? cacheKey with
     | some abstResult? =>
-      trace[Meta.synthInstance.cache] "cached: {type}"
       let result? ← applyCachedAbstractResult? type abstResult?
       trace[Meta.synthInstance] "result {result?} (cached)"
       return result?
     | none =>
-      trace[Meta.synthInstance.cache] "new: {type}"
       let abstResult? ← withNewMCtxDepth (allowLevelAssignments := true) do
-        match kind with
-        | .noMVars =>
-          /-
-          **Note**: The expensive `preprocessOutParam` step is morally **not** needed here because
-          the output params should be uniquely determined by the input params. During type class
-          resolution, definitional equality only unfolds `[reducible]` and `[instance_reducible]`
-          declarations. This is a contract with our users to ensure performance is reasonable.
-          However, the same `OrderDual` declaration that creates problems for `assignOutParams`
-          also prevents us from using this optimization. As an example, suppose we are trying to
-          synthesize
-          ```
-          FunLike F (OrderDual α) (OrderDual β)
-          ```
-          where the last two arguments of `FunLike` are output parameters. This term has no
-          metavariables, and it seems natural to skip `preprocessOutParam`, which would replace
-          the last two arguments with metavariables. However, if we don't replace them,
-          TC resolution fails because it cannot unfold `OrderDual` since it is semireducible.
-
-          **Note**: We should remove `preprocessOutParam` from the following line as soon as
-          Mathlib refactors `OrderDual`.
-          -/
-          SynthInstance.main (← preprocessOutParam type) maxResultSize
-        | .mvarsNoOutputParams => SynthInstance.main type maxResultSize
-        | .mvarsOutputParams => SynthInstance.main (← preprocessOutParam type) maxResultSize
+        let normType ← preprocessOutParam type
+        SynthInstance.main normType maxResultSize
       let result? ← applyAbstractResult? type abstResult?
       trace[Meta.synthInstance] "result {result?}"
-      cacheResult cacheKey kind abstResult? result?
+      cacheResult cacheKey abstResult? result?
       return result?
 
 def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) (decl := type.getAppFn.constName?.getD .anonymous) do
@@ -988,6 +874,5 @@ builtin_initialize
   registerTraceClass `Meta.synthInstance.resume (inherited := true)
   registerTraceClass `Meta.synthInstance.unusedArgs
   registerTraceClass `Meta.synthInstance.newAnswer
-  registerTraceClass `Meta.synthInstance.cache
 
 end Lean.Meta

src/include/lean/lean.h

@@ -1945,16 +1945,8 @@ static inline uint64_t lean_uint64_log2(uint64_t a) {
 static inline uint8_t lean_uint64_dec_eq(uint64_t a1, uint64_t a2) { return a1 == a2; }
 static inline uint8_t lean_uint64_dec_lt(uint64_t a1, uint64_t a2) { return a1 < a2; }
 static inline uint8_t lean_uint64_dec_le(uint64_t a1, uint64_t a2) { return a1 <= a2; }
-static inline uint64_t lean_uint64_mix_hash(uint64_t h, uint64_t k) {
-    uint64_t m = 0xc6a4a7935bd1e995;
-    uint64_t r = 47;
-    k *= m;
-    k ^= k >> r;
-    k ^= m;
-    h ^= k;
-    h *= m;
-    return h;
-}
+LEAN_EXPORT uint64_t lean_uint64_mix_hash(uint64_t a1, uint64_t a2);
+
 
 /* UInt64 -> other */
 static inline uint8_t lean_uint64_to_uint8(uint64_t a) { return ((uint8_t)a); }

src/lake/Lake/Build/Fetch.lean

@@ -25,7 +25,7 @@ using the `fetch` function defined in this module.
 namespace Lake
 
 /-- A type alias for `Option Package` that assists monad type class synthesis. -/
-@[expose] public abbrev CurrPackage := Option Package
+@[expose] public def CurrPackage := Option Package
 
 /-- Run the action `x` with `pkg?` as the current package or no package if `none`. -/
 @[inline] public def withCurrPackage? [MonadWithReader CurrPackage m] (pkg? : Option Package) (x : m α): m α :=

src/lake/Lake/CLI/Shake.lean

@@ -257,7 +257,7 @@ def calcNeeds (s : State) (i : ModuleIdx) : Needs := Id.run do
       needs := visitExpr k e needs
 
   for use in getExtraModUses env i do
-    let j : Nat := env.getModuleIdx? use.module |>.get!
+    let j := env.getModuleIdx? use.module |>.get!
     needs := needs.union { use with } {j}
 
   return needs
@@ -268,11 +268,11 @@ where
     Lean.Expr.foldConsts e deps fun c deps => Id.run do
       let mut deps := deps
       if let some c := getDepConstName? s c then
-        if let some (j : Nat) := env.getModuleIdxFor? c then
+        if let some j := env.getModuleIdxFor? c then
           let k := { k with isMeta := k.isMeta && !isDeclMeta' env c }
           if j != i then
             deps := deps.union k {j}
-            for (indMod : Nat) in s.indirectModUses[c]?.getD #[] do
+            for indMod in s.indirectModUses[c]?.getD #[] do
               if s.transDeps[i]!.has k indMod then
                 deps := deps.union k {indMod}
       return deps
@@ -427,7 +427,7 @@ def visitModule (pkgs : Array Name) (srcSearchPath : SearchPath)
   -- Add additional preserved imports
   for impStx in imports do
     let imp := decodeImport impStx
-    let j : Nat := s.env.getModuleIdx? imp.module |>.get!
+    let j := s.env.getModuleIdx? imp.module |>.get!
     let k := NeedsKind.ofImport imp
     if addOnly ||
         -- TODO: allow per-library configuration instead of hardcoding `Init`
@@ -456,14 +456,13 @@ def visitModule (pkgs : Array Name) (srcSearchPath : SearchPath)
             deps := deps.sub k' (transDeps.sub k' {j} |>.get k')
 
   if prelude?.isNone then
-    let j : Nat := s.env.getModuleIdx? `Init |>.get!
-    deps := deps.union .pub {j}
+    deps := deps.union .pub {s.env.getModuleIdx? `Init |>.get!}
 
   -- Accumulate `transDeps` which is the non-reflexive transitive closure of the still-live imports
   let mut transDeps := Needs.empty
   let mut alwaysAdd : Array Import := #[]  -- to be added even if implied by other imports
   for imp in s.mods[i]!.imports do
-    let j : Nat := s.env.getModuleIdx? imp.module |>.get!
+    let j := s.env.getModuleIdx? imp.module |>.get!
     let k := NeedsKind.ofImport imp
     if deps.has k j || imp.importAll then
       transDeps := addTransitiveImps transDeps imp j s.transDeps[j]!

src/lake/Lake/Util/Cli.lean

@@ -17,7 +17,8 @@ Defines the abstract CLI interface for Lake.
 
 /-! # Types -/
 
-public abbrev ArgList := List String
+@[expose]  -- for codegen
+public def ArgList := List String
 
 @[inline] public def ArgList.mk (args : List String) : ArgList :=
   args