content: {-# OPTIONS_HADDOCK not-home #-}
  
  {-# LANGUAGE AllowAmbiguousTypes #-}
  {-# LANGUAGE BlockArguments #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE FunctionalDependencies #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  {-|
  Module      : Data.Generic.HKD.Named
  Description : Construct an HKD record with named parameters.
  Copyright   : (c) Tom Harding, 2019
  License     : MIT
  Maintainer  : tom.harding@habito.com
  Stability   : experimental
  -}
  module Data.Generic.HKD.Named
    ( Record (..)
    ) where
  
  import Data.Functor.Contravariant (Contravariant (..))
  import Data.Generic.HKD.Types (HKD, HKD_)
  import Data.Generics.Product.Internal.Subtype (GUpcast (..))
  import Data.Kind (Type)
  import GHC.Generics
  import Named ((:!), NamedF (..))
  
  type family Append (xs :: Type -> Type) (ys :: Type -> Type) :: Type -> Type where
    Append (S1 meta head) tail    = S1 meta head :*: tail
    Append (left :*: right) other = left :*: Append right other
  
  type family Rearrange (i :: Type -> Type) :: Type -> Type where
    Rearrange (S1       m inner) = S1       m (Rearrange inner)
    Rearrange (M1 index m inner) = M1 index m (Rearrange inner)
    Rearrange (left :*: right)   = Append (Rearrange left) (Rearrange right)
    Rearrange (Rec0 inner)       = Rec0 inner
  
  -- | The 'Data.Generic.HKD.record' function lets us supply arguments to a type
  -- one by one, but can cause confusion when working with a record. If the
  -- record contains two fields of the same type, for example, we've introduced
  -- an opportunity for bugs and confusion. The @record@ function uses the
  -- wonderful @named@ package to help us:
  --
  -- >>> :set -XDeriveGeneric -XTypeApplications
  --
  -- >>> :{
  -- data User
  --   = User { name :: String, enemy :: String }
  --   deriving Generic
  -- :}
  --
  -- >>> :{
  -- test :: _
  -- test = record @User
  -- :}
  -- ...
  -- ... Found type wildcard ...
  -- ... standing for ...("name" :! f [Char])
  -- ...   -> ("enemy" :! f [Char]) -> HKD User f...
  -- ...
  class Record (structure :: Type) (f :: Type -> Type) (k :: Type)
      | f structure -> k where
    record :: k
  
  class GRecord (rep :: Type -> Type) (f :: Type -> Type) (structure :: Type) (k :: Type)
      | f structure rep -> k where
    grecord :: (forall p. rep p -> HKD structure f) -> k
  
  instance GRecord inner f structure k
      => GRecord (D1 meta inner) f structure k where
    grecord rebuild = grecord (rebuild . M1)
  
  instance GRecord inner f structure k
      => GRecord (C1 meta inner) f structure k where
    grecord rebuild = grecord (rebuild . M1)
  
  instance
      ( rec ~ (Rec0 inner)
      , k ~ (name :! inner -> HKD structure f)
      , meta ~ 'MetaSel ('Just name) i d c
      )
      => GRecord (S1 meta rec) f structure k where
    grecord fill = \(Arg inner) -> fill (M1 (K1 inner))
  
  instance
      ( GRecord right f structure k'
      , rec ~ Rec0 x
      , left ~ S1 ('MetaSel ('Just name) i d c) rec
      , k ~ (name :! x -> k')
      )
      => GRecord (left :*: right) f structure k where
    grecord fill = \(Arg left) -> grecord \right -> fill (M1 (K1 left) :*: right)
  
  instance
      ( Contravariant (HKD_ f structure)
      , Functor (HKD_ f structure)
  
      , list ~ Rearrange (HKD_ f structure)
      , GUpcast list (HKD_ f structure)
      , GRecord list f structure k
      )
      => Record structure f k where
    record = grecord @_ @f @structure (to . gupcast @list @(HKD_ f structure))
  