Difference in behaviour between Kernel.whnf and whnf

Stream: lean4

[Yann Herklotz]

In the following, it seems like Kernel.whnf gets stuck and doesn't reduce the instance for Nat of ToString (instToStringNat) and the result therefore isn't in whnf form. whnf on the other hand reduces it fine.

import Lean
open Lean Meta Elab
#eval show Term.TermElabM Unit from do
  let expr ← (Term.elabTerm (← `(toString (1 : Nat))) none)
  let res ← Lean.ofExceptKernelException <| Kernel.whnf (← getEnv) {} expr
  -- let res ← whnf expr
  Lean.logInfo m!"{res}"

Is this behaviour/difference expected?

I'm a bit surprised that the following works though, meaning the kernel can type check the following and the Kernel.isDefEq can at least look through toString and the instance. This suggests that Kernel.isDefEq might not use Kernel.whnf.

example : toString (1 : Nat) = "1" := by rfl

There is a comment saying that Kernel.whnf is mostly available for debugging, but it has been useful for us to reduce terms much more efficiently. Should it not be relied on?

[Mario Carneiro]

If you print the full expression expr you will see it has instantiated mvars:

#eval show Term.TermElabM Unit from do
  let expr ← (Term.elabTerm (← `(toString (1 : Nat))) none)
  Lean.logInfo m!"{repr expr}"
-- Lean.Expr.app
--   (Lean.Expr.app
--     (Lean.Expr.app
--       (Lean.Expr.const `ToString.toString [Lean.Level.mvar (Lean.Name.mkNum `_uniq 1)])
--       (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 2)))
--     (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 3)))
--   (Lean.Expr.app
--     (Lean.Expr.app
--       (Lean.Expr.app (Lean.Expr.const `OfNat.ofNat [Lean.Level.zero]) (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 6)))
--       (Lean.Expr.lit (Lean.Literal.natVal 1)))
--     (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 7)))

You need to call instantiateMVars to get rid of these mvars.

#eval show Term.TermElabM Unit from do
  let expr ← (Term.elabTerm (← `(toString (1 : Nat))) none)
  let expr ← instantiateMVars expr
  let expr ← Lean.ofExceptKernelException <| Kernel.whnf (← getEnv) {} expr
  Lean.logInfo m!"{expr}"
  -- { data := Nat.toDigits 10 1 }

[Kyle Miller]

Just to be safe, probably should synthesize pending metavariables too.

#eval show Term.TermElabM Unit from do
  let expr ← (Term.elabTerm (← `(toString (1 : Nat))) none)
  Term.synthesizeSyntheticMVarsUsingDefault
  let expr ← instantiateMVars expr
  let expr ← Lean.ofExceptKernelException <| Kernel.whnf (← getEnv) {} expr
  Lean.logInfo m!"{expr}"

[Yann Herklotz]

Ahh thank you! I need to be more careful with checking for mvars in the expression.