Vanishing implicit binders in expected type

Stream: lean4

[Anand Rao Tadipatri]

I have noticed that when a type contains implicit binders, Lean automatically discards them, creating meta-variables in the remaining expression; this does not happen with the default binders. Here is an MWE demonstrating this:

import Lean

open Lean Elab Parser Term Meta Tactic

set_option autoImplicit false


syntax (name := expType) "expectedType?" : term

@[term_elab expType] def traceExpectedType : TermElab
  | _, some type => do
    logInfo <| ← ppExpr type
    mkSorry type false
  | _, none => panic! "Expected type not available"

example : ∀ (n), n + 1 = 1 + n := expectedType? -- Correct: ∀ (n : Nat), n + 1 = 1 + n
example : ∀ {n}, n + 1 = 1 + n := expectedType? -- Incorrect: n✝ + 1 = 1 + n✝

(However, the correct type is displayed in both examples when the part after the := is replaced by an underscore.)
I initially assumed that this had to do with auto-implicits, but the error remains after disabling this feature. Is the above behaviour expected, and if so, is there a way to disable it?

[Sebastian Ullrich]

You're looking at https://leanprover.github.io/lean4/doc/lean3changes.html#implicit-lambdas

[Anand Rao Tadipatri]

Thanks.

[Anand Rao Tadipatri]

Is there an option to disable the implicit lambda feature in a file? (just like for autoImplicits)
For context, I am trying to create a clone of Lean's by tactic to modify the tactic execution. The code below works for the most part, but for theorem statements involving implicit binders, a tactic proof that works with the original by does not work with the clone by'.

 import Lean

open Lean Elab Parser Term Meta Tactic

syntax (name := byTactic') "by' " tacticSeq : term

private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do
  let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
  let mvarId := mvar.mvarId!
  let ref ← getRef
  registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext)
  return mvar

@[term_elab byTactic'] def elabByTactic' : TermElab := fun stx expectedType? => do
  match expectedType? with
  | some expectedType =>
    dbg_trace (← ppExpr expectedType)
    mkTacticMVar expectedType stx
  | none =>
    tryPostpone
    throwError ("invalid 'by\'' tactic, expected type has not been provided")

-- macro_rules
--   | `(by $tacs) => `(by' $tacs)

example : ∀ {n}, n + 0 = 0 + n := by
  intro -- works
  simp

example : ∀ {n}, n + 0 = 0 + n := by'
  intro -- error
  simp

(I am actually planning to take a different approach now, but would like to know for future reference.)

[Mario Carneiro]

there is a macro no_implicit_lambda% which disables implicit lambda, and a corresponding mdata node noImplicitLambda

[Mario Carneiro]

I'm pretty sure by is using something like that

[Mario Carneiro]

actually there is some special casing of byTactic here:

private def shouldPropagateExpectedTypeFor (nextArg : Arg) : Bool :=
  match nextArg with
  | .expr _  => false -- it has already been elaborated
  | .stx stx =>
    -- TODO: make this configurable?
    stx.getKind != ``Lean.Parser.Term.hole &&
    stx.getKind != ``Lean.Parser.Term.syntheticHole &&
    stx.getKind != ``Lean.Parser.Term.byTactic

[Anand Rao Tadipatri]

Thanks a lot. I will look into this.

[Anand Rao Tadipatri]

So if I understand correctly, the shouldPropagateExpectedTypeFor function is what I would need to modify to correct by'.