Possible issue in the implementation of takeWhileExists

[emmatigakis]

In chapter 11.1, in the section on erased existentials, I believe there may be an issue with the implementation of takeWhileExists.

To make takeWhileExists consistent with the earlier definitions (and with the usual semantics of takeWhile), shouldn’t it be implemented as follows?

takeWhileExists : (a -> Bool) -> Vect m a -> Exists (\n => Vect n a)
takeWhileExists f []        = Evidence _ []
takeWhileExists f (x :: xs) = case f x of
  True  => let Evidence _ ys = takeWhileExists f xs
            in Evidence _ (x :: ys)
  False => Evidence _ [] -- in the book this is `takeWhileExists f xs`

In the book, however, the False branch recursively calls takeWhileExists f xs. This appears to produce incorrect results, as it allows elements after the first failing predicate to be included.

For example:

Main> takeWhile3 (< 5) $ [0,1,2,3,5,6,7,8,9,4]
(4 ** [0, 1, 2, 3])

Main> takeWhileExists (< 5) $ [0,1,2,3,5,6,7,8,9,4]
Evidence 5 [0, 1, 2, 3, 4]

Here, takeWhileExists includes the trailing 4, even though the predicate fails earlier at 5. This behavior differs from both takeWhile3 and the standard definition of takeWhile, which suggests that the implementation in the book may be incorrect.

PS. I used ChatGPT to write this report a bit nicer than I could on my own. Sorry :)