From be014b1fc9931277fc4535e504ad1ced721118fb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 1 Apr 2022 18:20:36 -0700
Subject: [PATCH] fix: dotted notation corner case

---
 src/Lean/Elab/App.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index b79136b6b7..9150eb5442 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -866,9 +866,9 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
       let some expectedType := expectedType?
         | throwError "invalid dotted identifier notation, expected type must be known"
       forallTelescopeReducing expectedType fun _ resultType => do
-        let resultTypeFn := (← instantiateMVars resultType).getAppFn
+        let resultTypeFn := (← instantiateMVars resultType).consumeMData.getAppFn
         tryPostponeIfMVar resultTypeFn
-        let .const declName .. := resultTypeFn
+        let .const declName .. := resultTypeFn.consumeMData
           | throwError "invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant{indentExpr expectedType}"
         let idNew := declName ++ id.getId.eraseMacroScopes
         unless (← getEnv).contains idNew do