fix: disable implicit-lambdas when elaborating patterns

@Kha, Jason's example on issue #337 suggests that injecting
implicit-lambdas while elaborating patterns is problematic.
The elaborator was injecting `fun {Γ} =>` before the
pattern variable `ftm`.
So, I disabled the implicit-lambda during pattern elaboration. I
didn't find an example where it would be useful.

see #337

cc @JasonGross

src/Lean/Elab/Match.lean

@@ -528,18 +528,19 @@ private partial def withPatternVars {α} (pVars : Array PatternVar) (k : Array P
       k decls
   loop 0 #[]
 
-private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : TermElabM (Array Expr × Expr) := do
-  let mut patterns  := #[]
-  let mut matchType := matchType
-  for patternStx in patternStxs do
-    matchType ← whnf matchType
-    match matchType with
-    | Expr.forallE _ d b _ =>
-      let pattern ← elabTermEnsuringType patternStx d
-      matchType := b.instantiate1 pattern
-      patterns  := patterns.push pattern
-    | _ => throwError "unexpected match type"
-  return (patterns, matchType)
+private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : TermElabM (Array Expr × Expr) :=
+  withReader (fun ctx => { ctx with implicitLambda := false }) do
+    let mut patterns  := #[]
+    let mut matchType := matchType
+    for patternStx in patternStxs do
+      matchType ← whnf matchType
+      match matchType with
+      | Expr.forallE _ d b _ =>
+        let pattern ← elabTermEnsuringType patternStx d
+        matchType := b.instantiate1 pattern
+        patterns  := patterns.push pattern
+      | _ => throwError "unexpected match type"
+    return (patterns, matchType)
 
 def finalizePatternDecls (patternVarDecls : Array PatternVarDecl) : TermElabM (Array LocalDecl) := do
   let mut decls := #[]

src/Lean/Elab/Term.lean

@@ -101,6 +101,8 @@ structure Context where
   sectionVars        : NameMap Name    := {}
   /-- Map from internal name to fvar -/
   sectionFVars       : NameMap Expr    := {}
+  /-- Enable/disable implicit lambdas feature. -/
+  implicitLambda     : Bool             := true
 
 /-- We use synthetic metavariables as placeholders for pending elaboration steps. -/
 inductive SyntheticMVarKind where
@@ -995,7 +997,7 @@ private partial def elabImplicitLambda (stx : Syntax) (catchExPostpone : Bool) :
 
 /- Main loop for `elabTerm` -/
 private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone : Bool) (implicitLambda : Bool) : Syntax → TermElabM Expr
-  | stx => withFreshMacroScope $ withIncRecDepth do
+  | stx => withFreshMacroScope <| withIncRecDepth do
     trace[Elab.step]! "expected type: {expectedType?}, term\n{stx}"
     checkMaxHeartbeats "elaborator"
     withNestedTraces do
@@ -1006,7 +1008,7 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
     match stxNew? with
     | some stxNew => withMacroExpansion stx stxNew $ elabTermAux expectedType? catchExPostpone implicitLambda stxNew
     | _ =>
-      let implicit? ← if implicitLambda then useImplicitLambda? stx expectedType? else pure none
+      let implicit? ← if implicitLambda && (← read).implicitLambda then useImplicitLambda? stx expectedType? else pure none
       match implicit? with
       | some expectedType => elabImplicitLambda stx catchExPostpone expectedType #[]
       | none              => elabUsingElabFns stx expectedType? catchExPostpone
@@ -1041,7 +1043,11 @@ def mkTermInfo (stx : Syntax) (e : Expr) : TermElabM (Sum Info MVarId) := do
   a new synthetic metavariable of kind `SyntheticMVarKind.postponed` is created, registered,
   and returned.
   The option `catchExPostpone == false` is used to implement `resumeElabTerm`
-  to prevent the creation of another synthetic metavariable when resuming the elaboration. -/
+  to prevent the creation of another synthetic metavariable when resuming the elaboration.
+
+  If `implicitLambda == true`, then disable implicit lambdas feature for the given syntax, but not for its subterms.
+  We use this flag to implement, for example, the `@` modifier. If `Context.implicitLambda == false`, then this parameter has no effect.
+  -/
 def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) : TermElabM Expr :=
   withInfoContext' (withRef stx <| elabTermAux expectedType? catchExPostpone implicitLambda stx) (mkTermInfo stx)
 

tests/lean/run/337.lean

@@ -0,0 +1,39 @@
+section
+  variable (G : Type 1) (T : Type 1)
+           (EG : G → G → Type)
+           (getCtx : T → G)
+  inductive CtxSyntaxLayer where
+  inductive TySyntaxLayer where
+  | arrow : {Γ : G} → (A B : T) → EG Γ (getCtx A) → EG Γ (getCtx B) → TySyntaxLayer
+end
+section
+  variable (G : Type 1) (T : Type 1) (Tm : Type 1)
+           (EG : G → G → Type) (ET : T → T → Type)
+           (getCtx : T → G) (getTy : Tm → T)
+           (TAlgebra : TySyntaxLayer G T EG getCtx → T)
+
+  inductive TmSyntaxLayer where
+    | app : {Γ : G} → (A B : T) → (Actx : EG Γ (getCtx A)) → (Bctx : EG Γ (getCtx B))
+        → (f x : Tm)
+        → ET (getTy f) (TAlgebra (TySyntaxLayer.arrow A B Actx Bctx))
+        → ET (getTy x) A
+        → TmSyntaxLayer
+end
+
+structure Ty where
+  ctx : Type
+  ty : ctx → Type
+structure Tm where
+  ty : Ty
+  tm : ∀ {Γ}, ty.ty Γ
+
+def ECtx : Type → Type → Type := (PLift $ · = ·)
+def ETy  : Ty  → Ty  → Type := (PLift $ · = ·)
+def ETm  : Tm  → Tm  → Type := (PLift $ · = ·)
+
+def interpTyStep : TySyntaxLayer Type Ty ECtx Ty.ctx → Ty
+  | TySyntaxLayer.arrow (Γ:=Γ) A B (PLift.up Actx) (PLift.up Bctx) => Ty.mk Γ (λ γ => A.ty (cast Actx γ) → B.ty (cast Bctx γ))
+
+def interpTmStep : TmSyntaxLayer Type Ty Tm ECtx ETy Ty.ctx Tm.ty interpTyStep → Tm
+  | TmSyntaxLayer.app (Γ:=Γ1) A B (PLift.up Actx) (PLift.up Bctx) { ty := fty , tm := ftm } x (PLift.up fTy) (PLift.up xTy)
+    => sorry