content: {-# language AllowAmbiguousTypes #-}
  {-# language DataKinds #-}
  {-# language FlexibleContexts #-}
  {-# language FlexibleInstances #-}
  {-# language MultiParamTypeClasses #-}
  {-# language PolyKinds #-}
  {-# language ScopedTypeVariables #-}
  {-# language StandaloneKindSignatures #-}
  {-# language TypeApplications #-}
  {-# language TypeFamilies #-}
  {-# language TypeOperators #-}
  {-# language UndecidableInstances #-}
  
  module Rel8.Generic.Record
    ( Record(..)
    , GRecordable, GRecord, grecord, gunrecord
    )
  where
  
  -- base
  import Data.Kind ( Constraint, Type )
  import GHC.Generics
    ( Generic, Rep, from, to
    , (:+:)( L1, R1 ), (:*:)( (:*:) ), M1( M1 )
    , Meta( MetaCons, MetaSel ), D, C, S
    )
  import GHC.TypeLits ( type (+), AppendSymbol, Div, Mod, Nat, Symbol )
  import Prelude hiding ( Show )
  
  
  type GRecord :: (Type -> Type) -> Type -> Type
  type family GRecord rep where
    GRecord (M1 D meta rep) = M1 D meta (GRecord rep)
    GRecord (l :+: r) = GRecord l :+: GRecord r
    GRecord (M1 C ('MetaCons name fixity 'False) rep) =
      M1 C ('MetaCons name fixity 'True) (Snd (Count 0 rep))
    GRecord rep = rep
  
  
  type Count :: Nat -> (Type -> Type) -> (Nat, Type -> Type)
  type family Count n rep where
    Count n (M1 S ('MetaSel _selector su ss ds) rep) =
      '(n + 1, M1 S ('MetaSel ('Just (Show (n + 1))) su ss ds) rep)
    Count n (a :*: b) = CountHelper1 (Count n a) b
    Count n rep = '(n, rep)
  
  
  type CountHelper1 :: (Nat, Type -> Type) -> (Type -> Type) -> (Nat, Type -> Type)
  type family CountHelper1 tuple b where
    CountHelper1 '(n, a) b = CountHelper2 a (Count n b)
  
  
  type CountHelper2 :: (Type -> Type) -> (Nat, Type -> Type) -> (Nat, Type -> Type)
  type family CountHelper2 a tuple where
    CountHelper2 a '(n, b) = '(n, a :*: b)
  
  
  type Show :: Nat -> Symbol
  type Show n =
    AppendSymbol "_" (AppendSymbol (Show' (Div n 10)) (ShowDigit (Mod n 10)))
  
  
  type Show' :: Nat -> Symbol
  type family Show' n where
    Show' 0 = ""
    Show' n = AppendSymbol (Show' (Div n 10)) (ShowDigit (Mod n 10))
  
  
  type ShowDigit :: Nat -> Symbol
  type family ShowDigit n where
    ShowDigit 0 = "0"
    ShowDigit 1 = "1"
    ShowDigit 2 = "2"
    ShowDigit 3 = "3"
    ShowDigit 4 = "4"
    ShowDigit 5 = "5"
    ShowDigit 6 = "6"
    ShowDigit 7 = "7"
    ShowDigit 8 = "8"
    ShowDigit 9 = "9"
  
  
  type Snd :: (a, b) -> b
  type family Snd tuple where
    Snd '(_a, b) = b
  
  
  type GRecordable :: (Type -> Type) -> Constraint
  class GRecordable rep where
    grecord :: rep x -> GRecord rep x
    gunrecord :: GRecord rep x -> rep x
  
  
  instance GRecordable rep => GRecordable (M1 D meta rep) where
    grecord (M1 a) = M1 (grecord a)
    gunrecord (M1 a) = M1 (gunrecord a)
  
  
  instance (GRecordable l, GRecordable r) => GRecordable (l :+: r) where
    grecord (L1 a) = L1 (grecord a)
    grecord (R1 a) = R1 (grecord a)
    gunrecord (L1 a) = L1 (gunrecord a)
    gunrecord (R1 a) = R1 (gunrecord a)
  
  
  instance Countable 0 rep =>
    GRecordable (M1 C ('MetaCons name fixity 'False) rep)
   where
    grecord (M1 a) = M1 (count @0 a)
    gunrecord (M1 a) = M1 (uncount @0 a)
  
  
  instance {-# OVERLAPPABLE #-} GRecord rep ~ rep => GRecordable rep where
    grecord = id
    gunrecord = id
  
  
  type Countable :: Nat -> (Type -> Type) -> Constraint
  class Countable n rep where
    count :: rep x -> Snd (Count n rep) x
    uncount :: Snd (Count n rep) x -> rep x
  
  
  instance Countable n (M1 S ('MetaSel selector su ss ds) rep) where
    count (M1 a) = M1 a
    uncount (M1 a) = M1 a
  
  
  instance
    ( Countable n a, Countable n' b
    , '(n', a') ~ Count n a
    , Snd (CountHelper2 a' (Count n' b)) ~ (a' :*: Snd (Count n' b))
    )
    => Countable n (a :*: b)
   where
    count (a :*: b) = count @n a :*: count @n' b
    uncount (a :*: b) = uncount @n a :*: uncount @n' b
  
  
  instance {-# OVERLAPPABLE #-} Snd (Count n rep) ~ rep => Countable n rep where
    count = id
    uncount = id
  
  
  type Record :: Type -> Type
  newtype Record a = Record
    { unrecord :: a
    }
  
  
  instance (Generic a, GRecordable (Rep a)) => Generic (Record a) where
    type Rep (Record a) = GRecord (Rep a)
  
    from (Record a) = grecord (from a)
    to = Record . to . gunrecord
  