    {-# LANGUAGE DeriveFunctor #-}

    -- | Contexts with at most one hole.

    module Agda.Utils.AffineHole where

    import Control.Applicative

    data AffineHole r a
      = ZeroHoles a
          -- ^ A constant term.
      | OneHole (r -> a)
          -- ^ A term with one hole.
      | ManyHoles
          -- ^ A term with many holes (error value).
      deriving (Functor)

    instance Applicative (AffineHole r) where
      pure = ZeroHoles

      ZeroHoles f <*> ZeroHoles a = ZeroHoles $ f a
      ZeroHoles f <*> OneHole g   = OneHole $ f . g
      OneHole h   <*> ZeroHoles a = OneHole (`h` 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@.