copilot-language - Unable to drop as many elements from Stream as prepended #607

Activity

1. strikef

   changed the title [-]`copilot-language` - unable to drop as many element as prepended[/-] [+]`copilot-language` - Unable to drop as many elements from Stream as prepended[/+] on Mar 11, 2025
2. strikef commented on Mar 12, 2025

   

   strikef

   on Mar 12, 2025

   Last edited by strikef

   Author

   More actions

   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

   copilot/copilot-language/src/Copilot/Language/Analyze.hs

   Line 191 in e042933

   | k >= length xs = throw DropIndexOverflow

   
   It appears that analyzeDrop is throwing DropIndexOverflow even when |drop| == |append|. Could this be the culprit?

   👍React with 👍1Reacted by Andreas Ländle
3. RyanGlScott commented on Feb 13, 2026

   

   RyanGlScott

   on Feb 13, 2026

   Collaborator

   More actions

   Description

   The documentation for copilot-language's drop function claims that one can drop a number of elements from a stream equal to the number of elements prepended to the stream. In practice, this is not the case, and copilot-language's analysis will reject such uses of drop.

   Type

   • Bug: implementation does not match the documented behavior.

   Additional context

   None.

   Requester

   • Ryan Scott (Galois)

   Method to check presence of bug

   Run the following Copilot specification:

   {-# LANGUAGE NoImplicitPrelude #-}
   module Main (main) where
   
   import Language.Copilot
   
   spec :: Spec
   spec = do
     let s :: Stream Bool
         s = drop 2 ([False, False] ++ true)
     trigger "example" s [arg s]
   
   main :: IO ()
   main = interpret 5 spec

   This specification will be rejected with the following error message:

   $ runghc Bug.hs
   Bug.hs: Copilot error: Drop index overflow!
   CallStack (from HasCallStack):
     error, called at src/Copilot/Language/Error.hs:24:16 in copilot-language-4.3-inplace:Copilot.Language.Error
   

   Expected result

   Running the Copilot specification above should succeed, and the Copilot interpreter should print five true samples.

   Desired result

   Running the Copilot specification above should succeed, and the Copilot interpreter should print five true samples.

   Proposed solution

   Modify the implementation of drop to add a special case for when the drop length equals the number of elements prepended to a stream with an Append, which will return the underlying stream.

   Further notes

   None.
4. philphauler

   added a commit that references this issue on Sep 24, 2026

   copilot-language: Report exceptions as failures in drop tests. Refs C…

   ...

   966e0d7