    -- | Contexts with at most one hole.

    module Agda.Utils.AffineHole where

    data AffineHole r a
      = ZeroHoles a
          -- ^ A constant term.
      | OneHole (r -> a) r
          -- ^ A term with one hole and the (old) contents.
      | ManyHoles
          -- ^ A term with many holes (error value).
      deriving ((forall a b. (a -> b) -> AffineHole r a -> AffineHole r b)
    -> (forall a b. a -> AffineHole r b -> AffineHole r a)
    -> Functor (AffineHole r)
    forall a b. a -> AffineHole r b -> AffineHole r a
    forall a b. (a -> b) -> AffineHole r a -> AffineHole r b
    forall r a b. a -> AffineHole r b -> AffineHole r a
    forall r a b. (a -> b) -> AffineHole r a -> AffineHole r b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> AffineHole r b -> AffineHole r a
    $c<$ :: forall r a b. a -> AffineHole r b -> AffineHole r a
    fmap :: forall a b. (a -> b) -> AffineHole r a -> AffineHole r b
    $cfmap :: forall r a b. (a -> b) -> AffineHole r a -> AffineHole r b
    Functor)

    instance Applicative (AffineHole r) where
      pure :: forall a. a -> AffineHole r a
    pure = a -> AffineHole r a
    forall r a. a -> AffineHole r a
    ZeroHoles

      ZeroHoles a -> b
    f <*> :: forall a b.
    AffineHole r (a -> b) -> AffineHole r a -> AffineHole r b
    <*> ZeroHoles a
    a = b -> AffineHole r b
    forall r a. a -> AffineHole r a
    ZeroHoles (b -> AffineHole r b) -> b -> AffineHole r b
    forall a b. (a -> b) -> a -> b
    $ a -> b
    f a
    a
      ZeroHoles a -> b
    f <*> OneHole r -> a
    g r
    y = (r -> b) -> r -> AffineHole r b
    forall r a. (r -> a) -> r -> AffineHole r a
    OneHole (a -> b
    f (a -> b) -> (r -> a) -> r -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . r -> a
    g) r
    y
      OneHole r -> a -> b
    h r
    x <*> ZeroHoles a
    a = (r -> b) -> r -> AffineHole r b
    forall r a. (r -> a) -> r -> AffineHole r a
    OneHole (r -> a -> b
    `h` a
    a) r
    x
      AffineHole r (a -> b)
    _ <*> AffineHole r a
    _ = AffineHole r b
    forall r a. AffineHole r a
    ManyHoles

    -- NB: @AffineHole r@ is not a monad.
    -- @
    --   OneHole (h :: r -> a) >>= (k :: a -> AffineHole r b) = _ :: AffineHole r b
    -- @
    -- We are lacking an @r@ to make use of @h@.