singletons + On + via

On.hs

{-# Language DataKinds                #-}
{-# Language DerivingVia              #-}
{-# Language FlexibleInstances        #-}
{-# Language GADTs                    #-}
{-# Language InstanceSigs             #-}
{-# Language PolyKinds                #-}
{-# Language RankNTypes               #-}
{-# Language ScopedTypeVariables      #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications         #-}
{-# Language TypeOperators            #-}
{-# Language UndecidableInstances     #-}

import Data.Coerce
import Data.Function
import Data.Hashable
import Data.Kind
import Data.List
import Data.Ord
import Data.Singletons
import Data.Singletons.Prelude.Num
import Data.Singletons.Prelude.Tuple
import Data.Singletons.TH

-- Can be made an instance where it appears only in
-- negative/contravariant position (am I sure about that?) like Eq,
-- Ord, Hashable.
--
-- Can I make a version for Foldable? That takes a polymorphic
-- function?
--
-- This takes a singletons function (~>) which means we can pass it
-- functions like
--
--   FstSym0 :: (k1,k2) ~> k1
--
type On :: forall a b. (a ~> b) -> Type
newtype On f where
 On :: a -> On @a @b f

type                                   Good :: Type -> Constraint
class    (a ~ Demote a, SingKind a) => Good a
instance (a ~ Demote a, SingKind a) => Good a

instance (Good a, Good b, Eq b, SingI f) => Eq (On @a @b f) where
 (==) :: On @a @b f -> On @a @b f -> Bool
 (==) = coerce ((==) @b `on` f) where
  f :: a->b
  f = fromSing (sing @f)

instance (Good a, Good b, Ord b, SingI f) => Ord (On @a @b f) where
 compare :: On @a @b f -> On @a @b f -> Ordering
 compare = coerce (comparing f) where
  f :: a->b
  f = fromSing (sing @f)

instance (Good a, Good b, Show b, SingI f) => Show (On @a @b f) where
 show :: On @a @b f -> String
 show = coerce (show . f) where
  f :: a->b
  f = fromSing (sing @f)

instance (Good a, Good b, Hashable b, SingI f) => Hashable (On @a @b f) where
 hashWithSalt :: Int -> On @a @b f -> Int
 hashWithSalt salt = coerce (hashWithSalt salt . f) where
  f :: a->b
  f = fromSing (sing @f)

 hash :: On @a @b f -> Int
 hash = coerce (hash . f) where
  f :: a->b
  f = fromSing (sing @f)

-- {-# Language ApplyingVia #-}
--
-- sort @(via On @_ @_ @FstSym0)
sortOnFst :: forall a b. Good a => Good b => Ord a => [(a,b)] -> [(a,b)]
sortOnFst = coerce do sort @(On @(a,b) @a FstSym0)

newtype Pair a = Pair (a, a)

-- {-# Language DerivingVia #-}
deriving via On @(a,a) @a FstSym0
 instance (Eq a, Good a) => Eq (Pair a)
deriving via On @(a,a) @a FstSym0
 instance (Ord a, Good a) => Ord (Pair a)
deriving via On @(a,a) @a FstSym0
 instance (Hashable a, Good a) => Hashable (Pair a)