disabling implicit lambda

Stream: lean4

[Scott Morrison]

I would like to have a tactic which does not use implicit lambdas when elaborating a term, but I'm failing to get it to work. Here's a #mwe

import Lean
open Lean Elab Meta

syntax "test" term : tactic
elab_rules : tactic | `(tactic| test $t:term) => do
  let t' ← Term.elabTerm t none (implicitLambda := false)
  logInfo (← inferType t')

example (t : {ι : Type} → ι → Unit) : True := by
  test @t -- `{ι : Type} → ι → Unit`
  test t  -- `?m.2087 → Unit`         <--- But I want `{ι : Type} → ι → Unit`
  trivial

Any advice on what I'm missing?

[Scott Morrison]

Even more upsetting is:

def α : Type 1 := {ι : Type} → ι → Unit

example (t : α) : True := by
  test @t -- `α`
  test t  -- `?m.2119 → Unit`
  trivial

[Wojciech Nawrocki]

Have you read docs#Lean.Elab.Term.elabTerm carefully? There is an extra negation :wink: But also, I am not sure that the thing you want actually has to do with implicit lambdas. Implicit lambdas let you write fun x => x : {a : Type) -> a -> a, but here the expected type is none(unknown) rather than specifically a function type with implicit arguments.

[Wojciech Nawrocki]

If you use the global setting

  let t' ←
    withTheReader Term.Context ({· with implicitLambda := false}) do
      Term.elabTerm t none

the output is the same.

[Scott Morrison]

I not only read the docs, but the source, and as far as I can see the doc is incorrect, and implicitLambda := false disables implicit lambdas.

[Scott Morrison]

Perhaps I do have the naming wrong, and this is not about implicit lambdas.

Nevertheless, I would like to know how to avoid having inferType fill in leading implicit arguments with metavariables!

[Wojciech Nawrocki]

Ah, we should fix the doc then! As to your issue, if we follow the chain of elaborators we find that processImplicitArg determines whether to insert an mvar based on explicit : Bool in its monad context. This is originally set in elabAppFn here, but note that this happens when the syntax is @$id. I am not immediately seeing a global option to turn it on when the syntax is not that.

[Wojciech Nawrocki]

What is the broader context? If you just have a single ident, you could simply wrap it in the @$id syntax.

[Scott Morrison]

Doc-string correction is at lean4#2378.

[Scott Morrison]

Thanks for the pointers into the relevant elaborators. Indeed for my use case simply prepending an @ before elaborating may suffice. I will try that now!

[Scott Morrison]

Ahha: elabTermForApply is what I'm looking for.