FirstField.hs

{-# LANGUAGE 
    ScopedTypeVariables,
    TemplateHaskell,
    TypeFamilies,
    GADTs,
    KindSignatures,
    DataKinds,
    PolyKinds,
    TypeOperators,
    FlexibleContexts,
    RankNTypes,
    UndecidableInstances,
    FlexibleInstances,
    InstanceSigs,
    DefaultSignatures
 #-}
module FirstField (firstField) where

import Generics.SOP
import Data.Promotion.TH
import Data.Promotion.Prelude

promote [d|mapHead xs = map head xs|]

firstOfProduct :: NP I xs -> I (Head xs)
firstOfProduct (I x :* _) = I x

firstOfEach :: NS (NP I) xss -> NS I (MapHead xss)
firstOfEach (Z xs) = Z (firstOfProduct xs)
firstOfEach (S xs) = S (firstOfEach xs)

class AllEqual (xs :: [*]) where
  type AllEqualTo xs :: *
  reduce :: NS I xs -> AllEqualTo xs

instance {-# OVERLAPS #-} AllEqual '[a] where
  type AllEqualTo '[a] = a
  reduce (Z (I x)) = x

instance (AllEqual as, AllEqualTo as ~ a) => AllEqual (a ': as) where
  type AllEqualTo (a ': as) = a
  reduce (Z (I x)) = x
  reduce (S x) = reduce x

firstField :: (Generic a, AllEqual (MapHead (Code a))) => a -> AllEqualTo (MapHead (Code a))
firstField = reduce . firstOfEach . unSOP . from