Redundant `=?=` in elabTermEnsuringType

[nomeata]

Not sure how relevant that is, but maybe there is a worthwhile performance improvement to be found here.

Consider

import Lean
set_option autoImplicit false

open Lean Meta Elab Term

syntax (name := asNat) "as_nat " term : term

@[term_elab asNat] def evalAsNat : TermElab := fun stx _expectedType? => do
  let `(as_nat $t) := stx | throwUnsupportedSyntax
  elabTermEnsuringType t (mkConst ``Nat)

def Foo := Nat
example (n : Foo) (P : Nat → Prop ): 
  P (set_option trace.Meta.isDefEq true in
    set_option trace.Meta.isDefEq.cache true in
    (as_nat n))
  := sorry

This will show

[Meta.isDefEq] ✅ Nat =?= Foo ▼
  [] ✅ Nat =?= Nat 
  [cache] cache true for Nat =?= Foo 

[Meta.isDefEq] ✅ Foo =?= Nat ▼
  [] ✅ Nat =?= Nat 
  [cache] cache true for Foo =?= Nat 

so the expected type is unified with the actual type twice.

The first comes from this code in Lean/Elab/App.lean:

/-- This method executes after all application arguments have been processed. -/
private def finalize : M Expr := do
…
  if let some expectedType := s.expectedType? then
    trySynthesizeAppInstMVars
    -- Try to propagate expected type. Ignore if types are not definitionally equal, caller must handle it.
    trace[Elab.app.finalize] "expected type: {expectedType}"
    discard <| isDefEq expectedType eType
  synthesizeAppInstMVars
  return e

And the second comes from the ensureHasType in elabTermEnsuringType.

Both checks are certainly necessary, but it seems wasteful to do the same defeq twice here, so I wonder if it is a bug that we do not get a defeq cache here, or if that is unavoidable (different contexts or so)?

(NB: The DefEq cache is set up so that you get a cache hit independent of the orientation, so that is not the problem.)

Versions

1630d9b

Impact

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

[nomeata]

Both checks are certainly necessary, but it seems wasteful to do the same defeq twice here, so I wonder if it is a bug that we do not get a defeq cache here, or if that is unavoidable (different contexts or so)?

Ah, yes, we simply do not cache across distinct calls to isExprDefEq; see the use of resetDefEqPermCaches here:

/-- See `isDefEq`. -/
def isExprDefEq (t s : Expr) : MetaM Bool :=
  withReader (fun ctx => { ctx with defEqCtx? := some { lhs := t, rhs := s, lctx := ctx.lctx, localInstances := ctx.localInstances } }) do
    /-
    The following `resetDefEqPermCaches` is a workaround. Without it the test suite fails, and we probably cannot compile complex libraries such as Mathlib.
    TODO: investigate why we need this reset.
    Some conjectures:
    - It is not enough to check whether `t` and `s` do not contain metavariables. We would need to check the type
      of all local variables `t` and `s` depend on. If the local variables contain metavariables, the result of `isDefEq` may change if these
      variables are instantiated.
    - Related to the previous one: the operation
      ```lean
      _root_.Lean.MVarId.replaceLocalDeclDefEq (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr)
      ```
      is probably being misused. We are probably using it to replace a `type` with `typeNew` where these two types
      are definitionally equal IFF we can assign the metavariables in `type`.

    Possible fix: always generate new `FVarId`s when update the type of local variables.
    Drawback: this operation can be quite expensive, and we must evaluate whether it is worth doing to remove the following `reset`.

    Remark: the kernel does *not* update the type of variables in the local context.
    -/
    resetDefEqPermCaches
    checkpointDefEq (mayPostpone := true) <| Meta.isExprDefEqAux t s