From cf8315ed962b989f7d3b5da0a0d85fef49c460ac Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 11 Jun 2025 09:35:46 +0200
Subject: [PATCH] fix: restrict the `IteratorLoop` instance on `DropWhile`,
 which was accidentally more general (#8703)

This PR corrects the `IteratorLoop` instance in `DropWhile`, which
previously triggered for arbitrary iterator types.
---
 src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 β]