`copilot-language` - Unable to drop as many elements from Stream as prepended
https://hackage.haskell.org/package/copilot-language-4.3/docs/Copilot-Language-Operators-Temporal.html#v:drop
The elements must be realizable at the present time to be able to drop elements. For most kinds of streams, you cannot drop elements without prepending an equal or greater number of elements to them first, as it could result in undefined samples.
Since the document states that prepending 'equal' number of elements suffices, I expected the following code to compile
prependedStream :: Stream Bool
prependedStream = [True, True] ++ false
droppedStream :: Stream Bool
droppedStream = drop 2 prependedStream
However, it fails to compile with the following error:
Copilot error: Drop index overflow!
Why is it that I'm not able to drop the exact same number of elements as I prepended? Could it be a documentation issue or a bug?
analyzeDrop :: Int -> Stream a -> IO ()
analyzeDrop k (Append xs _ _)
| k >= length xs = throw DropIndexOverflow
| k > fromIntegral (maxBound :: DropIdx) = throw DropMaxViolation
| otherwise = return ()
analyzeDrop _ _ = throw DropAppliedToNonAppend
https://github.com/Copilot-Language/copilot/blob/e0429336689613f7e7788e3c8589414e2ab43608/copilot-language/src/Copilot/Language/Analyze.hs#L191
It appears that analyzeDrop is throwing DropIndexOverflow even when |drop| == |append|. Could this be the culprit?