Function leaks out of background

[isovector]

In the following, I am asking for only laws about rewardThen:

== Functions ==
      win :: Game
     lose :: Game
   reward :: Reward -> Game
  subgame :: Game -> Game -> Game -> Game
  eitherW :: Game -> Game -> Game
     both :: Game -> Game -> Game
     race :: Game -> Game -> Game
multigate :: [(EventFilter, Game)] -> Game
  andThen :: Game -> Game -> Game

== Functions ==                      
rewardThen :: Reward -> Game -> Game

WARNING: The following types have no 'Ord' or 'Observe' instance declared.
You will not get any equations about the following types:
  [(Int, Game)]
  [(EventFilter, Game)]

== Laws ==
  1. rewardThen r win = reward r   
  2. rewardThen r g = andThen (reward r) g
  3. andThen (andThen g g2) g3 = andThen g (andThen g2 g3)
  4. both g (rewardThen r g2) = both g2 (rewardThen r g)
  5. eitherW g (rewardThen r g2) = eitherW g2 (rewardThen r g)
  6. race g (rewardThen r g) = rewardThen r g
  7. race (rewardThen r g) g2 = race g (rewardThen r g2)
  8. rewardThen r (both g g2) = both g (rewardThen r g2)
  9. rewardThen r (race g g2) = race g (rewardThen r g2)

Look at law 3! It doesn't mention rewardThen at all!

Produced via:

quickSpec $ background [withMaxTermSize 5 <> sig_types <> without sig_games_core ["rewardThen"] ] <> con "rewardThen" rewardThen

[isovector]

Repro:

{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module Workflow.WIP2 where

import qualified Data.Set as S
import Data.Set (Set)
import Data.Data
import Data.Word
import GHC.Generics
import Test.QuickCheck hiding (Result)
import Control.Monad.Writer
import Data.Tuple (swap)
import Data.List
import QuickSpec

data Event = Event Word8
  deriving stock (Eq, Ord, Show, Data, Generic)

-- # ArbitraryEvent
instance Arbitrary Event where
  arbitrary = Event <$> arbitrary
  shrink    = genericShrink

data EventFilter
  = Always
  | Never
  | Exactly Word8  -- ! 1
  deriving stock (Eq, Ord, Show, Data, Generic)

-- # ArbitraryEventFilter
instance Arbitrary EventFilter where
  arbitrary = frequency
    [ (3, pure Always)
    , (1, pure Never)
    , (5, Exactly <$> arbitrary)
    ]
  shrink = genericShrink

always :: EventFilter
always = Always

never :: EventFilter
never = Never

sig_filters :: Sig
sig_filters = signature
  [ con "always" always
  , con  "never" never
  ]

data Reward = Reward Word8
  deriving stock (Eq, Ord, Show, Data, Generic)

-- # ArbitraryReward
instance Arbitrary Reward where
  arbitrary = Reward <$> arbitrary
  shrink    = genericShrink

data Result
  = Victory
  | Defeat
  deriving stock (Eq, Ord, Show, Data, Generic)

-- # ArbitraryResult
instance Arbitrary Result where
  arbitrary = elements [ victory, defeat ]
  shrink    = genericShrink

victory :: Result
victory = Victory

defeat :: Result
defeat = Defeat

sig_results :: Sig
sig_results = signature
  [ con "victory" victory
  , con "defeat"  defeat
  ]

------------------------------------------------------------------------------
--                         constructors
------------------------------------------------------------------------------

data Game
  = Win
  | Lose
  | RewardThen Reward Game
  | Subgame Game Game Game
  | EitherW Game Game
  | Both Game Game
  | Race Game Game
  | Multigate [(EventFilter, Game)]
  deriving stock (Eq, Ord, Show, Data, Generic)

-- # ArbitraryGame
instance Arbitrary Game where
  arbitrary = sized $ \n ->
    case n <= 1 of
      True -> elements [win, lose]
      False -> frequency
        [ (3, pure win)
        , (3, pure lose)
        , (3, reward  <$> arbitrary)
        , (5, rewardThen <$> arbitrary
                         <*> decayArbitrary 2)
        , (5, andThen <$> decayArbitrary 2
                      <*> decayArbitrary 2)
        , (5, subgame <$> decayArbitrary 3
                      <*> decayArbitrary 3
                      <*> decayArbitrary 3)
        , (5, both <$> decayArbitrary 2
                   <*> decayArbitrary 2)
        , (5, eitherW <$> decayArbitrary 2
                      <*> decayArbitrary 2)
        , (5, race <$> decayArbitrary 2
                   <*> decayArbitrary 2)
        , (5, multigate <$> decayArbitrary 5)
        , (2, comeback  <$> arbitrary)
        , (1, pure bottom)
        , (5, gate <$> arbitrary <*> arbitrary)
        ]
  shrink = genericShrink

-- # ObserveGame
instance
    Observe [Event] (Set Reward, Maybe Result) Game
    where
  observe = runGame

decayArbitrary :: Arbitrary a => Int -> Gen a
decayArbitrary n = scale (`div` n) arbitrary

reward :: Reward -> Game
reward r = rewardThen r win

rewardThen :: Reward -> Game -> Game
rewardThen = RewardThen

win :: Game
win = Win

lose :: Game
lose = Lose

andThen :: Game -> Game -> Game
andThen g1 g2 = subgame g1 g2 lose

subgame :: Game -> Game -> Game -> Game
subgame (RewardThen r g) g1 g2 =
  rewardThen r (subgame g g1 g2)
subgame Win  g1 _  = g1
subgame Lose _  g2 = g2
subgame g    g1 g2 = Subgame g g1 g2

eitherW :: Game -> Game -> Game
eitherW (RewardThen r g1) g2 =
  rewardThen r (eitherW g1 g2)
eitherW g1 (RewardThen r g2) =
  rewardThen r (eitherW g1 g2)
eitherW Lose Lose = lose
eitherW Win  _    = win
eitherW _    Win  = win
eitherW a    b    = EitherW a b

both :: Game -> Game -> Game
both (RewardThen r g1) g2 = rewardThen r (both g1 g2)
both g1 (RewardThen r g2) = rewardThen r (both g1 g2)
both Win  Win  = win
both Lose _    = lose
both _    Lose = lose
both a    b    = Both a b

race :: Game -> Game -> Game
race (RewardThen r g1) g2 = rewardThen r (race g1 g2)
race g1 (RewardThen r g2) = rewardThen r (race g1 g2)
race Win  _ = win
race Lose _ = lose
race _ Win  = win
race _ Lose = lose
race a b    = Race a b

multigate :: [(EventFilter, Game)] -> Game
multigate cs = Multigate cs

sig_games_core :: Sig
sig_games_core = signature
  [ con        "win" win
  , con       "lose" lose
  , con     "reward" reward
  , con    "subgame" subgame
  , con    "eitherW" eitherW
  , con       "both" both
  , con       "race" race
  , con  "multigate" multigate
  , con    "andThen" andThen
  , con "rewardThen" rewardThen
  ]

------------------------------------------------------------------------------
--                         extensions
------------------------------------------------------------------------------

comeback :: Game -> Game
comeback g = subgame g lose win

bottom :: Game
bottom = multigate []

gate :: EventFilter -> Game -> Game
gate ef g = multigate [(ef, g)]

sig_games_ext :: Sig
sig_games_ext = signature
  [ con "comeback" comeback
  , con   "bottom" bottom
  , con     "gate" gate
  ]

bingo :: [[Game]] -> Reward -> Game
bingo squares r
  = let subgames = squares
                ++ transpose squares  -- ! 1
        allOf :: [Game] -> Game
        allOf = foldr both    win
        anyOf :: [Game] -> Game
        anyOf = foldr eitherW lose
     in subgame (anyOf (fmap allOf subgames)) (reward r) lose

------------------------------------------------------------------------------
--                           tests
------------------------------------------------------------------------------

bingo_game :: Game
bingo_game = flip bingo (Reward 100) $ do
  x <- [0..2]
  pure $ do
    y <- [0..2]
    pure $ gate (Exactly $ x * 10 + y) win

------------------------------------------------------------------------------
--                         observations
------------------------------------------------------------------------------

runGame :: [Event] -> Game -> (Set Reward, Maybe Result)
runGame evs g =
  swap $ runWriter $ fmap _toResult $ _runGame g evs

_toResult :: Game -> Maybe Result
_toResult Win  = Just Victory
_toResult Lose = Just Defeat
_toResult _    = Nothing

_runGame :: Game -> [Event] -> Writer (Set Reward) Game
_runGame g (e : es) = do
  g' <- _stepGame g (Just e)
  _runGame g' es
_runGame g [] = do
  g' <- _stepGame g Nothing
  case g == g' of  -- ! 1
    True  -> pure g'
    False -> _runGame g' []

_stepGame :: Game -> Maybe Event -> Writer (Set Reward) Game
_stepGame Win  _ = pure win
_stepGame Lose _ = pure lose
_stepGame (RewardThen r g) e =
  tell (S.singleton r) >> _stepGame g e
_stepGame (Subgame g g1 g2) e =  -- ! 1
  subgame <$> _stepGame g e      -- ! 2
          <*> pure g1
          <*> pure g2
_stepGame (EitherW g1 g2) e =
  eitherW <$> _stepGame g1 e
          <*> _stepGame g2 e
_stepGame (Both g1 g2) e =
  both <$> _stepGame g1 e
       <*> _stepGame g2 e
_stepGame (Race g1 g2) e =
  race <$> _stepGame g1 e
       <*> _stepGame g2 e
_stepGame (Multigate cs) (Just e)
  | Just (_, g) <- find (\(ef, _) -> matches ef e) cs
  = pure g
_stepGame x@Multigate{} _ = pure x

matches :: EventFilter -> Event -> Bool
matches Never  _ = False
matches Always _ = True
matches (Exactly e) (Event ev) = e == ev

------------------------------------------------------------------------------
--                         specifications
------------------------------------------------------------------------------

sig_types :: Sig
sig_types = signature
  [ monoType        $ Proxy @Event
  , monoType        $ Proxy @EventFilter
  , monoType        $ Proxy @Reward
  , monoType        $ Proxy @Result
  , monoTypeObserve $ Proxy @Game
  , vars ["e"]      $ Proxy @Event
  , vars ["ef"]     $ Proxy @EventFilter
  , vars ["r"]      $ Proxy @Reward
  , vars ["res"]    $ Proxy @Result
  , vars ["g"]      $ Proxy @Game
  ]

sig_options :: Sig
sig_options = signature
  [ withMaxTermSize 5
  ]

[isovector]

Hit this again, this time without without.

 quickSpec $ background [sig_types, sig_games_interest] <> con "gate" gate
== Functions ==
   subgame :: Game -> Game -> Game -> Game
   eitherW :: Game -> Game -> Game
      both :: Game -> Game -> Game
      race :: Game -> Game -> Game
       win :: Game
      lose :: Game
rewardThen :: Reward -> Game -> Game
     gate2 :: EventFilter -> Game -> EventFilter -> Game -> Game

== Functions ==                        
gate :: EventFilter -> Game -> Game

== Laws ==
  1. gate2 ef g ef g2 = gate ef g  
  2. subgame (gate ef g) g2 win = gate ef (subgame g g2 win)
  3. subgame (gate ef g) lose g2 = gate ef (subgame g lose g2)
  4. subgame (gate ef lose) g g2 = gate ef g2
  5. both g (gate2 ef win ef2 g2) = both g (gate2 ef g ef2 g2)
  6. eitherW g (gate2 ef lose ef2 g2) = eitherW g (gate2 ef g ef2 g2)
  7. subgame (subgame g lose g2) g3 g4 = subgame g g4 (subgame g2 g3 g4)

the last three rules don't mention gate at all.

requires this definition in scope:

sig_games_interest :: Sig
sig_games_interest = signature
  [ con    "subgame" subgame
  , con    "eitherW" eitherW
  , con       "both" both
  , con       "race" race
  , con        "win" win
  , con       "lose" lose
  , con "rewardThen" rewardThen
  , con "gate2" $ \ef1 g1 ef2 g2 -> multigate [(ef1, g1), (ef2, g2)]
  ]

[isovector]

IMO this, along with #46 and #40 suggest there is a bug somewhere in the background codepath.