Meta.isDefEq vs. Kernel.whnf

Stream: lean4

[Joachim Breitner]

(deleted)

[Joachim Breitner]

Is this a bug or expected behaviour: I have an expression that isn’t Meta.isDefEq to it’s Kernel.whnf, even though I am running at transparency .all. Is there something else I have to so that Meta.isDefEq accepts this?

import Lean

open Lean Meta

/--
info: Reduced ⏎
  List.range.loop n []  o
  (Nat.rec
        ⟨(fun x f x_1 =>
              (match (motive := (x : Nat) → List Nat → Nat.below (motive := fun x => List Nat → List Nat) x → List Nat)
                  x, x_1 with
                | 0, ns => fun x => ns
                | n.succ, ns => fun x => x.1 (n :: ns))
                f)
            Nat.zero PUnit.unit,
          PUnit.unit⟩
        (fun n n_ih =>
          ⟨(fun x f x_1 =>
                (match (motive :=
                    (x : Nat) → List Nat → Nat.below (motive := fun x => List Nat → List Nat) x → List Nat) x, x_1 with
                  | 0, ns => fun x => ns
                  | n.succ, ns => fun x => x.1 (n :: ns))
                  f)
              n.succ n_ih,
            n_ih⟩)
        n).1
    []
---
info: But not defeq (kernel says true)
-/
#guard_msgs in
run_meta
  withLocalDeclD `n (.const ``Nat []) fun n => do
    let e := mkApp2 (.const ``List.range.loop []) n (.app (.const ``List.nil [0]) (.const ``Nat []))
    check e
    let .ok e' := Kernel.whnf (← getEnv) (← getLCtx) e
      | throwError "faild to whnf"
    -- let e' ← withTransparency .all (Meta.whnf e)
    logInfo m!"Reduced {indentExpr e}\to{indentExpr e'}"
    check e'
    let eq ← withTransparency .all (isDefEq e e')
    let .ok keq := Kernel.isDefEq (← getEnv) (← getLCtx) e e'
      | throwError "failed to Kernel.isDefEq"
    unless eq do
      logInfo m!"But not defeq (kernel says {keq})"

[Sebastian Ullrich]

This is likely expected. Smart unfolding, which the kernel knows nothing about, can block Meta reduction.

[Joachim Breitner]

I see, I thought it must be a corner like this. I'll see if I can disable smart unfolding

Indeed, at least in this example withOptions (smartUnfolding.set · false) helps.

And in my actual use case as well. That cost me more time than it should have, turns out my evaluator was type-correct after all :man_facepalming: But good to know that before the weekend starts properly.