diff --git a/src/Lean/Compiler/LCNF/Closure.lean b/src/Lean/Compiler/LCNF/Closure.lean
index c17c2f9c13..de77803a2c 100644
--- a/src/Lean/Compiler/LCNF/Closure.lean
+++ b/src/Lean/Compiler/LCNF/Closure.lean
@@ -156,7 +156,8 @@ mutual
 
   /-- Collect dependencies of the given expression. -/
   partial def collectType (type : Expr) : ClosureM Unit := do
-    type.forEachWhere Expr.isFVar fun e => collectFVar e.fvarId!
+    if type.hasFVar then
+      type.forEachWhere Expr.isFVar fun e => collectFVar e.fvarId!
 
 end
 
diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean
index e1fd8cc809..d085c40a6f 100644
--- a/src/Lean/Meta/Tactic/Util.lean
+++ b/src/Lean/Meta/Tactic/Util.lean
@@ -99,7 +99,8 @@ def _root_.Lean.MVarId.getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId
   let removeDeps (e : Expr) (candidates : FVarIdHashSet) : MetaM FVarIdHashSet := do
     let e ← instantiateMVars e
     let visit : StateRefT FVarIdHashSet MetaM FVarIdHashSet := do
-      e.forEachWhere Expr.isFVar fun e => modify fun s => s.erase e.fvarId!
+      if e.hasFVar then
+        e.forEachWhere Expr.isFVar fun e => modify fun s => s.erase e.fvarId!
       get
     visit |>.run' candidates
   mvarId.withContext do