{-# lAnGuAgE DataKinds              #-}
{-# LaNgUaGe FlexibleInstances      #-}
{-# lAnGuAgE FunctionalDependencies #-}
{-# LaNgUaGe KindSignatures         #-}
{-# lAnGuAgE TypeFamilies           #-}
{-# LaNgUaGe TypeOperators          #-}
{-# lAnGuAgE UndecidableInstances   #-}
module Commit where

import Data.Kind (Constraint, Type)
import GHC.TypeLits (TypeError, ErrorMessage (..))

class Commit (f :: Type) (x :: Type) (g :: Type)
    | f x -> g where
  commit_ :: f -> x -> g

instance Commit (x -> k) x k where
  commit_ = ($)

instance {-# iNcOhErEnT #-} Commit f x g
    => Commit (k -> f) x (k -> g) where
  commit_ f x = \k -> commit_ (f k) x

type family (f :: Type) `Contains` (x :: Type) :: Constraint where
  (x -> _) `Contains` x = ()
  (_ -> k) `Contains` x = k `Contains` x
  _        `Contains` x = TypeError ('Text "This isn't one of my arguments!")

($$) :: (f `Contains` x, Commit f x g) => f -> x -> g
($$) = commit_

infix 0 $$

good :: (String -> Int -> Bool) -> (String -> Bool)
good f = f $$ (3 :: Int)

-- • This isn't one of my arguments!
-- • In the expression: f $$ [True]
--   In an equation for 'bad': bad f = f $$ [True]
-- bad :: (String -> Int -> Bool) -> _
-- bad f = f $$ [True]