fix: uncacheable syntax stack access in doIf

src/Lean/Parser/Do.lean

@@ -114,7 +114,9 @@ def doIfProp    := leading_parser (withAnonymousAntiquot := false)
 def doIfCond    :=
   withAntiquot (mkAntiquot "doIfCond" decl_name% (anonymous := false) (isPseudoKind := true)) <|
     doIfLet <|> doIfProp
-@[builtin_doElem_parser] def doIf := leading_parser withPositionAfterLinebreak <| ppRealGroup <|
+-- must reset cache as `withPositionAfterLinebreak` will look at syntax not produced by this parser (or even
+-- current category call)
+@[builtin_doElem_parser] def doIf := leading_parser withResetCache <| withPositionAfterLinebreak <| ppRealGroup <|
   ppRealFill (ppIndent ("if " >> doIfCond >> " then") >> ppSpace >> doSeq) >>
   many (checkColGe "'else if' in 'do' must be indented" >>
     group (ppDedent ppSpace >> ppRealFill (elseIf >> doIfCond >> " then " >> doSeq))) >>

src/Lean/Parser/Extra.lean

@@ -16,7 +16,7 @@ namespace Parser
 attribute [run_builtin_parser_attribute_hooks]
   leadingNode termParser commandParser mkAntiquot nodeWithAntiquot sepBy sepBy1
   unicodeSymbol nonReservedSymbol
-  withCache withPosition withPositionAfterLinebreak withoutPosition withForbidden withoutForbidden setExpected
+  withCache withResetCache withPosition withPositionAfterLinebreak withoutPosition withForbidden withoutForbidden setExpected
   incQuotDepth decQuotDepth suppressInsideQuot evalInsideQuot
   withOpen withOpenDecl
   dbgTraceState

src/Lean/Parser/Types.lean

@@ -357,12 +357,27 @@ def adaptCacheableContextFn (f : CacheableParserContext → CacheableParserConte
 def adaptCacheableContext (f : CacheableParserContext → CacheableParserContext) : Parser → Parser :=
   withFn (adaptCacheableContextFn f)
 
-/-- Run `p` under the given context transformation with a fresh cache, restore outer cache afterwards. -/
-def adaptUncacheableContextFn (f : ParserContextCore → ParserContextCore) (p : ParserFn) : ParserFn := fun c s =>
+private def withStackDrop (drop : Nat) (p : ParserFn) : ParserFn := fun c s =>
+  let initDrop := s.stxStack.drop
+  let s := p c { s with stxStack.drop := drop }
+  { s with stxStack.drop := initDrop }
+
+/--
+Run `p` with a fresh cache, restore outer cache afterwards.
+`p` may access the entire syntax stack.
+-/
+def withResetCacheFn (p : ParserFn) : ParserFn := withStackDrop 0 fun c s =>
   let parserCache := s.cache.parserCache
-  let s' := p ⟨f c.toParserContextCore⟩ { s with cache.parserCache := {} }
+  let s' := p c { s with cache.parserCache := {} }
   { s' with cache.parserCache := parserCache }
 
+@[inherit_doc withResetCacheFn]
+def withResetCache : Parser → Parser := withFn withResetCacheFn
+
+/-- Run `p` under the given context transformation with a fresh cache (see also `withResetCacheFn`). -/
+def adaptUncacheableContextFn (f : ParserContextCore → ParserContextCore) (p : ParserFn) : ParserFn :=
+  withResetCacheFn (fun c s => p ⟨f c.toParserContextCore⟩ s)
+
 /--
 Run `p` and record result in parser cache for any further invocation with this `parserName`, parser context, and parser state.
 `p` cannot access syntax stack elements pushed before the invocation in order to make caching independent of parser history.
@@ -376,10 +391,8 @@ def withCacheFn (parserName : Name) (p : ParserFn) : ParserFn := fun c s => Id.r
     -- TODO: turn this into a proper trace once we have these in the parser
     --dbg_trace "parser cache hit: {parserName}:{s.pos} -> {r.stx}"
     return ⟨s.stxStack.push r.stx, r.lhsPrec, r.newPos, s.cache, r.errorMsg⟩
-  let initDrop := s.stxStack.drop
   let initStackSz := s.stxStack.raw.size
-  let s := p c { s with stxStack.drop := initStackSz, lhsPrec := 0, errorMsg := none }
-  let s := { s with stxStack.drop := initDrop }
+  let s := withStackDrop initStackSz (fun c s => p c { s with lhsPrec := 0, errorMsg := none }) c s
   if s.stxStack.raw.size != initStackSz + 1 then
     panic! s!"withCacheFn: unexpected stack growth {s.stxStack.raw}"
   { s with cache.parserCache := s.cache.parserCache.insert key ⟨s.stxStack.back, s.lhsPrec, s.pos, s.errorMsg⟩ }