Constrained.hs

-- SPDX-FileCopyrightText: 2022 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# LANGUAGE QuantifiedConstraints, DeriveLift #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Morley.Util.Constrained
  ( Constrained(..)
  , NullConstraint
  , mapConstrained
  , traverseConstrained
  , withConstrained
  , withConstrainedM
  , foldConstrained
  , foldConstrainedM
  ) where

import Data.GADT.Compare (GCompare, GEq, defaultCompare, defaultEq)
import Fmt (Buildable(..))
import Language.Haskell.TH.Syntax (Lift)

-- | Always truthful unary constraint. Can be used to essentially turn
-- 'Constrained' into a somewhat inefficient @Some@.
type NullConstraint :: forall k. k -> Constraint
class NullConstraint any
instance NullConstraint any

type Constrained :: (k -> Constraint) -> (k -> Type) -> Type
data Constrained c f where
  Constrained :: forall c f a. c a => f a -> Constrained c f

-- | Map over argument.
mapConstrained :: (forall t. c t => f t -> g t) -> Constrained c f -> Constrained c g
mapConstrained f = foldConstrained $ Constrained . f

-- | Traverse over argument.
traverseConstrained :: Functor m => (forall a. c a => f a -> m (g a)) -> Constrained c f -> m (Constrained c g)
traverseConstrained f = foldConstrained $ fmap Constrained . f

-- | Apply function to constrained value
withConstrained :: Constrained c f -> (forall t. c t => f t -> r) -> r
withConstrained (Constrained x) f = f x

-- | Monadic 'withConstrained'
withConstrainedM :: Monad m => m (Constrained c f) -> (forall t. f t -> m r) -> m r
withConstrainedM m f = m >>= foldConstrained f

-- | Flipped version of 'withConstrained'
foldConstrained :: (forall t. c t => f t -> r) -> Constrained c f -> r
foldConstrained f (Constrained x) = f x

-- | Flipped version of 'withConstrainedM'
foldConstrainedM :: Monad m => (forall t. c t => f t -> m r) -> m (Constrained c f) -> m r
foldConstrainedM f m = m >>= foldConstrained f

deriving stock instance (forall a. c a => Show (f a)) => Show (Constrained c f)

instance (forall a. c a => NFData (f a)) => NFData (Constrained c f) where
  rnf (Constrained x) = rnf x

deriving stock instance (forall a. c a => Lift (f a)) => Lift (Constrained c f)

instance (forall a. c a => Buildable (f a)) => Buildable (Constrained c f) where
  build (Constrained a) = build a

instance GEq f => Eq (Constrained c f) where
  (Constrained a) == (Constrained b) = defaultEq a b

instance GCompare f => Ord (Constrained c f) where
  compare (Constrained a) (Constrained b) = defaultCompare a b