From d0ee9d012774d4343ca2078b19adb11b10940fe0 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 1 Oct 2024 15:09:08 +0200
Subject: [PATCH] feat: expand `invalid projection` type inference error
 (#5556)

hopefully this will make debugging meta code a bit easier
---
 src/Lean/Meta/InferType.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean
index 753ca06b5270..c574220d3955 100644
--- a/src/Lean/Meta/InferType.lean
+++ b/src/Lean/Meta/InferType.lean
@@ -95,10 +95,10 @@ private def inferConstType (c : Name) (us : List Level) : MetaM Expr := do
     throwIncorrectNumberOfLevels c us
 
 private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Expr := do
-  let failed {α} : Unit → MetaM α := fun _ =>
-    throwError "invalid projection{indentExpr (mkProj structName idx e)}"
   let structType ← inferType e
   let structType ← whnf structType
+  let failed {α} : Unit → MetaM α := fun _ =>
+    throwError "invalid projection{indentExpr (mkProj structName idx e)} from type {structType}"
   matchConstStruct structType.getAppFn failed fun structVal structLvls ctorVal =>
     let n := structVal.numParams
     let structParams := structType.getAppArgs