    module Hackage.Security.Client.Formats (
        -- * Formats
        -- ** Type level
        FormatUn
      , FormatGz
        -- ** Term level
      , Format(..)
      , Formats(..)
        -- * Key membership
      , HasFormat(..)
        -- ** Utility
      , hasFormatAbsurd
      , hasFormatGet
        -- * Map-like operations
      , formatsMap
      , formatsMember
      , formatsLookup
      ) where

    import Prelude
    import Data.Kind (Type)
    import Hackage.Security.Util.Stack
    import Hackage.Security.Util.TypedEmbedded

    {-------------------------------------------------------------------------------
      Formats
    -------------------------------------------------------------------------------}

    data FormatUn
    data FormatGz

    -- | Format is a singleton type (reflection type to term level)
    --
    -- NOTE: In the future we might add further compression formats.
    data Format :: Type -> Type where
      FUn :: Format FormatUn
      FGz :: Format FormatGz

    deriving instance Show (Format f)
    deriving instance Eq   (Format f)

    instance Unify Format where
      unify :: forall typ typ'. Format typ -> Format typ' -> Maybe (typ :=: typ')
    unify Format typ
    FUn Format typ'
    FUn = (typ :=: typ') -> Maybe (typ :=: typ')
    forall a. a -> Maybe a
    Just typ :=: typ
    typ :=: typ'
    forall a. a :=: a
    Refl
      unify Format typ
    FGz Format typ'
    FGz = (typ :=: typ') -> Maybe (typ :=: typ')
    forall a. a -> Maybe a
    Just typ :=: typ
    typ :=: typ'
    forall a. a :=: a
    Refl
      unify Format typ
    _   Format typ'
    _   = Maybe (typ :=: typ')
    forall a. Maybe a
    Nothing

    {-------------------------------------------------------------------------------
      Products
    -------------------------------------------------------------------------------}

    -- | Available formats
    --
    -- Rather than having a general list here, we enumerate all possibilities.
    -- This means we are very precise about what we expect, and we avoid any runtime
    -- errors about unexpected format definitions.
    --
    -- NOTE: If we add additional cases here (for dealing with additional formats)
    -- all calls to @error "inaccessible"@ need to be reevaluated.
    data Formats :: Type -> Type -> Type where
      FsNone :: Formats () a
      FsUn   :: a -> Formats (FormatUn :- ()) a
      FsGz   :: a -> Formats (FormatGz :- ()) a
      FsUnGz :: a -> a -> Formats (FormatUn :- FormatGz :- ()) a

    deriving instance Eq   a => Eq   (Formats fs a)
    deriving instance Show a => Show (Formats fs a)

    instance Functor (Formats fs) where
      fmap :: forall a b. (a -> b) -> Formats fs a -> Formats fs b
    fmap a -> b
    g = (forall f. Format f -> a -> b) -> Formats fs a -> Formats fs b
    forall a b fs.
    (forall f. Format f -> a -> b) -> Formats fs a -> Formats fs b
    formatsMap (\Format f
    _format -> a -> b
    g)

    {-------------------------------------------------------------------------------
      Key membership
    -------------------------------------------------------------------------------}

    -- | @HasFormat fs f@ is a proof that @f@ is a key in @fs@.
    --
    -- See 'formatsMember' and 'formatsLookup' for typical usage.
    data HasFormat :: Type -> Type -> Type where
      HFZ :: Format f       -> HasFormat (f  :- fs) f
      HFS :: HasFormat fs f -> HasFormat (f' :- fs) f

    deriving instance Eq   (HasFormat fs f)
    deriving instance Show (HasFormat fs f)

    hasFormatAbsurd :: HasFormat () f -> a
    hasFormatAbsurd :: forall f a. HasFormat () f -> a
    hasFormatAbsurd HasFormat () f
    _ = String -> a
    forall a. HasCallStack => String -> a
    error String
    "inaccessible"

    hasFormatGet :: HasFormat fs f -> Format f
    hasFormatGet :: forall fs f. HasFormat fs f -> Format f
    hasFormatGet (HFZ Format f
    f)  = Format f
    f
    hasFormatGet (HFS HasFormat fs f
    hf) = HasFormat fs f -> Format f
    forall fs f. HasFormat fs f -> Format f
    hasFormatGet HasFormat fs f
    hf

    {-------------------------------------------------------------------------------
      Map-like functionality
    -------------------------------------------------------------------------------}

    formatsMap :: (forall f. Format f -> a -> b) -> Formats fs a -> Formats fs b
    formatsMap :: forall a b fs.
    (forall f. Format f -> a -> b) -> Formats fs a -> Formats fs b
    formatsMap forall f. Format f -> a -> b
    _ Formats fs a
    FsNone        = Formats fs b
    Formats () b
    forall a. Formats () a
    FsNone
    formatsMap forall f. Format f -> a -> b
    f (FsUn   a
    a)    = b -> Formats (FormatUn :- ()) b
    forall a. a -> Formats (FormatUn :- ()) a
    FsUn   (Format FormatUn -> a -> b
    forall f. Format f -> a -> b
    f Format FormatUn
    FUn a
    a)
    formatsMap forall f. Format f -> a -> b
    f (FsGz   a
    a)    = b -> Formats (FormatGz :- ()) b
    forall a. a -> Formats (FormatGz :- ()) a
    FsGz   (Format FormatGz -> a -> b
    forall f. Format f -> a -> b
    f Format FormatGz
    FGz a
    a)
    formatsMap forall f. Format f -> a -> b
    f (FsUnGz a
    a a
    a') = b -> b -> Formats (FormatUn :- (FormatGz :- ())) b
    forall a. a -> a -> Formats (FormatUn :- (FormatGz :- ())) a
    FsUnGz (Format FormatUn -> a -> b
    forall f. Format f -> a -> b
    f Format FormatUn
    FUn a
    a) (Format FormatGz -> a -> b
    forall f. Format f -> a -> b
    f Format FormatGz
    FGz a
    a')

    formatsMember :: Format f -> Formats fs a -> Maybe (HasFormat fs f)
    formatsMember :: forall f fs a. Format f -> Formats fs a -> Maybe (HasFormat fs f)
    formatsMember Format f
    _   Formats fs a
    FsNone       = Maybe (HasFormat fs f)
    forall a. Maybe a
    Nothing
    formatsMember Format f
    FUn (FsUn   a
    _  ) = HasFormat fs f -> Maybe (HasFormat fs f)
    forall a. a -> Maybe a
    Just (HasFormat fs f -> Maybe (HasFormat fs f))
    -> HasFormat fs f -> Maybe (HasFormat fs f)
    forall a b. (a -> b) -> a -> b
    $ Format f -> HasFormat (f :- ()) f
    forall f fs. Format f -> HasFormat (f :- fs) f
    HFZ Format f
    Format FormatUn
    FUn
    formatsMember Format f
    FUn (FsGz     a
    _) = Maybe (HasFormat fs f)
    forall a. Maybe a
    Nothing
    formatsMember Format f
    FUn (FsUnGz a
    _ a
    _) = HasFormat fs f -> Maybe (HasFormat fs f)
    forall a. a -> Maybe a
    Just (HasFormat fs f -> Maybe (HasFormat fs f))
    -> HasFormat fs f -> Maybe (HasFormat fs f)
    forall a b. (a -> b) -> a -> b
    $ Format f -> HasFormat (f :- (FormatGz :- ())) f
    forall f fs. Format f -> HasFormat (f :- fs) f
    HFZ Format f
    Format FormatUn
    FUn
    formatsMember Format f
    FGz (FsUn   a
    _  ) = Maybe (HasFormat fs f)
    forall a. Maybe a
    Nothing
    formatsMember Format f
    FGz (FsGz     a
    _) = HasFormat fs f -> Maybe (HasFormat fs f)
    forall a. a -> Maybe a
    Just (HasFormat fs f -> Maybe (HasFormat fs f))
    -> HasFormat fs f -> Maybe (HasFormat fs f)
    forall a b. (a -> b) -> a -> b
    $ Format f -> HasFormat (f :- ()) f
    forall f fs. Format f -> HasFormat (f :- fs) f
    HFZ Format f
    Format FormatGz
    FGz
    formatsMember Format f
    FGz (FsUnGz a
    _ a
    _) = HasFormat fs f -> Maybe (HasFormat fs f)
    forall a. a -> Maybe a
    Just (HasFormat fs f -> Maybe (HasFormat fs f))
    -> HasFormat fs f -> Maybe (HasFormat fs f)
    forall a b. (a -> b) -> a -> b
    $ HasFormat (f :- ()) f -> HasFormat (FormatUn :- (f :- ())) f
    forall fs f f'. HasFormat fs f -> HasFormat (f' :- fs) f
    HFS (Format f -> HasFormat (f :- ()) f
    forall f fs. Format f -> HasFormat (f :- fs) f
    HFZ Format f
    Format FormatGz
    FGz)

    formatsLookup :: HasFormat fs f -> Formats fs a -> a
    formatsLookup :: forall fs f a. HasFormat fs f -> Formats fs a -> a
    formatsLookup (HFZ Format f
    FUn) (FsUn   a
    a  ) = a
    a
    formatsLookup (HFZ Format f
    FUn) (FsUnGz a
    a a
    _) = a
    a
    formatsLookup (HFZ Format f
    FGz) (FsGz     a
    a) = a
    a
    formatsLookup (HFS HasFormat fs f
    hf)  (FsUn   a
    _  ) = HasFormat () f -> a
    forall f a. HasFormat () f -> a
    hasFormatAbsurd HasFormat fs f
    HasFormat () f
    hf
    formatsLookup (HFS HasFormat fs f
    hf)  (FsGz     a
    _) = HasFormat () f -> a
    forall f a. HasFormat () f -> a
    hasFormatAbsurd HasFormat fs f
    HasFormat () f
    hf
    formatsLookup (HFS HasFormat fs f
    hf)  (FsUnGz a
    _ a
    a) = HasFormat fs f -> Formats fs a -> a
    forall fs f a. HasFormat fs f -> Formats fs a -> a
    formatsLookup HasFormat fs f
    hf (a -> Formats (FormatGz :- ()) a
    forall a. a -> Formats (FormatGz :- ()) a
    FsGz a
    a)