diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index a86c1e2dd1..747df33281 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -262,7 +262,11 @@ match type with
 
 private def removeUnused (ref : Syntax) (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo)
     : TermElabM (LocalContext × LocalInstances × Array Expr) := do
-used ← params.foldlM (Term.collectUsedFVars ref) {};
+used ← params.foldlM
+   (fun (used : CollectFVars.State) p => do
+     type ← Term.inferType ref p;
+     Term.collectUsedFVars ref used type)
+   {};
 used ← fieldInfos.foldlM
   (fun (used : CollectFVars.State) info => do
     fvarType ← Term.inferType ref info.fvar;