{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

import Data.Set (Set)
import Data.Set qualified as Set
import Data.Kind (Type, Constraint)

main :: IO ()
main = pure ()

-- Provides a liftA2-like ('cliftA2') function that might require arbitrary
-- constraints on its type parameters.
class ConstrainedApplicative f where
  type AppC f b :: Constraint
  type AppC _ _ = ()

  cliftA2
    :: (AppC f a, AppC f b, AppC f c)
    => (a -> b -> c) -> f a -> f b -> f c

instance ConstrainedApplicative [] where
  cliftA2 = liftA2

instance ConstrainedApplicative Set where
  type AppC Set k = Ord k
  cliftA2 f xs ys = Set.fromList $ cliftA2 f (Set.toList xs) (Set.toList ys)

-- An existentially wrapped 'PairClosed' @f@.
data NoB f
  = forall b. (PairClosed f, AppC f b) => NoB (f b)

-- Class newtype for 'AppC' (to work around QuantifiedConstraints and its
-- restrictions with type families).
class    AppC f b => AppC' f b where
instance AppC f b => AppC' f b where

-- A 'ConstrainedApplicative' @f@ is 'PairClosed' if whenever @'AppC' f a@ and
-- @'AppC' f b@ hold (for any @a@ and @b@), then @'AppC' f (a, b)@ holds.
class
  ( ConstrainedApplicative f
  , forall a b. (AppC' f a, AppC f b) => AppC' f (a, b)
  ) => PairClosed f where
instance
  ( ConstrainedApplicative f
  , forall a b. (AppC' f a, AppC f b) => AppC' f (a, b)
  ) => PairClosed f where

f :: NoB f -> NoB f -> NoB f
f (NoB fx) (NoB fy) = NoB (cliftA2 (,) fx fy)