diff --git a/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean b/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean
index 3b6bf44e8a..1ce9df4516 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean
@@ -278,7 +278,7 @@ instance DropWhile.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m
   .defaultImplementation
 
 instance DropWhile.instIteratorLoop [Monad m] [Monad n] [Iterator α m β] :
-    IteratorLoop α m n :=
+    IteratorLoop (DropWhile α m β P) m n :=
   .defaultImplementation
 
 instance DropWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β]