feat: expand invalid projection type inference error (#5556)

hopefully this will make debugging meta code a bit easier
leanprover · Oct 1, 2024 · d0ee9d0 · d0ee9d0
1 parent 3e2bca7
commit d0ee9d0
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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