Make apSubstMaybe return a Changed value (without Applicative/Monad instances)

[RyanGlScott]

A common pitfall when defining substitution-related functions with the Cryptol API is to do something like this:

data Foo = MkFoo Type Type

substFoo :: Subst -> Foo -> Foo
substFoo (MkFoo x y) = MkFoo <$> apSubstMaybe su x <*> apSubstMaybe su y

(Where apSubstMaybe :: Subst -> Type -> Maybe Type.)

This is subtly wrong, however. The Maybe in apSubstMaybe's return type is meant to be Nothing if applying the substitution did not change anything, and it is meant to be Just if applying the substituion did change something. However, due to the way the Applicative Maybe instance works, x <*> y = Nothing when x or y is Nothing, even if the other value is Just. This means that with the way substFoo is defined above, it could erroneously return Nothing, even if the substitution changes one of x or y!

The immediate problem can be fixed by rewriting the code to be in terms of anyJust2:

anyJust2 :: (a -> Maybe a) -> (b -> Maybe b) -> (a,b) -> Maybe (a,b)
anyJust2 f g (a,b) =
  case (f a, g b) of
    (Nothing, Nothing) -> Nothing
    (Just x , Nothing) -> Just (x, b)
    (Nothing, Just y ) -> Just (a, y)
    (Just x , Just y ) -> Just (x, y)

substFoo :: Subst -> Foo -> Foo
substFoo (MkFoo x y) = uncurry MkFoo <$> anyJust2 (apSubstMaybe su) (apSubstMaybe su) (x, y)

However, it is still all too tempting to accidentally use the Applicative Maybe instance (or the Monad Maybe instance, which has similar short-circuiting behavior for Nothing values) when defining custom substitution functions. In fact, this is a mistake that even the cryptol codebase has made before! Ideally, we'd make it harder for users to stumble into this pitfall. To that end, I propose that we change apSubstMaybe to instead return Changed Type, where Changed is defined as:

data Changed a = Unchanged | Changed a
  deriving Functor

Moreover, Changed would intentionally not have Applicative or Monad instances: the only way to compose Changed values would be with combinators such as anyJust2 (which would also need to manipulate Changed values instead of Maybe values). At that point, we might also consider renaming some of these functions, since they would no longer use Maybe, Just, etc.

This would be a breaking change for users of the Cryptol API, so we should make sure to survey what the breakage would be before landing such a change.

[sauclovian-g]

Seems like a good idea to me. It's all too easy to invoke wrong implicit behavior.