Generic.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

{- | Exact, opt-in nominal derivation for structural bindings.

The derivation supplies only nominal construction and destruction; wire keys,
union tags, presence, nullability, and defaults remain exclusively in the
@.keiro@ spec and the generated codec. Exact representation mismatches fail at
compile time; both binding laws and finite codec cases remain required evidence
against implementation defects and semantic mistakes.
-}
module Keiro.Codec.Structural.Generic (
    GNominalBinding,
    genericStructuralBinding,
) where

import Data.Kind (Constraint, Type)
import GHC.Generics
import GHC.TypeLits (ErrorMessage (..), TypeError)
import Keiro.Codec.Structural (StructuralBinding (..))

{- | Generic representations with identical constructor names, selector names,
field order, arity, and field types. There are deliberately no coercion,
prefix-stripping, or positional-only options.
-}
class GNominalBinding (domain :: Type -> Type) (shape :: Type -> Type) where
    gNominalToShape :: domain parameter -> shape parameter
    gNominalFromShape :: shape parameter -> domain parameter

instance {-# OVERLAPPING #-} (GNominalBinding domain shape) => GNominalBinding (M1 D domainMeta domain) (M1 D shapeMeta shape) where
    gNominalToShape (M1 value) = M1 (gNominalToShape value)
    gNominalFromShape (M1 value) = M1 (gNominalFromShape value)

instance {-# OVERLAPPING #-} (SameConstructor domainMeta shapeMeta, GNominalBinding domain shape) => GNominalBinding (M1 C domainMeta domain) (M1 C shapeMeta shape) where
    gNominalToShape (M1 value) = M1 (gNominalToShape value)
    gNominalFromShape (M1 value) = M1 (gNominalFromShape value)

instance {-# OVERLAPPING #-} (SameSelector domainMeta shapeMeta, GNominalBinding domain shape) => GNominalBinding (M1 S domainMeta domain) (M1 S shapeMeta shape) where
    gNominalToShape (M1 value) = M1 (gNominalToShape value)
    gNominalFromShape (M1 value) = M1 (gNominalFromShape value)

instance {-# OVERLAPPING #-} (GNominalBinding domainLeft shapeLeft, GNominalBinding domainRight shapeRight) => GNominalBinding (domainLeft :*: domainRight) (shapeLeft :*: shapeRight) where
    gNominalToShape (left :*: right) = gNominalToShape left :*: gNominalToShape right
    gNominalFromShape (left :*: right) = gNominalFromShape left :*: gNominalFromShape right

instance {-# OVERLAPPING #-} (GNominalBinding domainLeft shapeLeft, GNominalBinding domainRight shapeRight) => GNominalBinding (domainLeft :+: domainRight) (shapeLeft :+: shapeRight) where
    gNominalToShape (L1 value) = L1 (gNominalToShape value)
    gNominalToShape (R1 value) = R1 (gNominalToShape value)
    gNominalFromShape (L1 value) = L1 (gNominalFromShape value)
    gNominalFromShape (R1 value) = R1 (gNominalFromShape value)

instance {-# OVERLAPPING #-} GNominalBinding (K1 domainIndex value) (K1 shapeIndex value) where
    gNominalToShape (K1 value) = K1 value
    gNominalFromShape (K1 value) = K1 value

instance {-# OVERLAPPING #-} GNominalBinding U1 U1 where
    gNominalToShape U1 = U1
    gNominalFromShape U1 = U1

instance {-# OVERLAPPING #-} GNominalBinding V1 V1 where
    gNominalToShape value = case value of {}
    gNominalFromShape value = case value of {}

instance
    {-# OVERLAPPABLE #-}
    ( TypeError
        ( 'Text "keiro structural binding has no exact nominal correspondence between "
            ':<>: 'ShowType domain
            ':<>: 'Text " and "
            ':<>: 'ShowType shape
            ':$$: 'Text "Run keiro-dsl scaffold and fill the binding by hand at this error location in the scaffolded module."
        )
    ) =>
    GNominalBinding domain shape
    where
    gNominalToShape _ = error "unreachable: TypeError prevents generic structural binding construction"
    gNominalFromShape _ = error "unreachable: TypeError prevents generic structural binding construction"

type family SameConstructor (domainMeta :: Meta) (shapeMeta :: Meta) :: Constraint where
    SameConstructor ('MetaCons name domainFixity domainRecord) ('MetaCons name shapeFixity shapeRecord) = ()
    SameConstructor ('MetaCons domainName domainFixity domainRecord) ('MetaCons shapeName shapeFixity shapeRecord) =
        TypeError
            ( 'Text "keiro structural binding constructor mismatch: "
                ':<>: 'ShowType domainName
                ':<>: 'Text " versus "
                ':<>: 'ShowType shapeName
                ':$$: 'Text "Run keiro-dsl scaffold and fill the binding by hand at this error location in the scaffolded module."
            )

type family SameSelector (domainMeta :: Meta) (shapeMeta :: Meta) :: Constraint where
    SameSelector ('MetaSel name domainUnpack domainStrict domainDecided) ('MetaSel name shapeUnpack shapeStrict shapeDecided) = ()
    SameSelector ('MetaSel domainName domainUnpack domainStrict domainDecided) ('MetaSel shapeName shapeUnpack shapeStrict shapeDecided) =
        TypeError
            ( 'Text "keiro structural binding selector mismatch: "
                ':<>: 'ShowType domainName
                ':<>: 'Text " versus "
                ':<>: 'ShowType shapeName
                ':$$: 'Text "Run keiro-dsl scaffold and fill the binding by hand at this error location in the scaffolded module."
            )

-- | Derive a total binding when both generic representations correspond exactly.
genericStructuralBinding ::
    ( Generic domain
    , Generic shape
    , GNominalBinding (Rep domain) (Rep shape)
    ) =>
    StructuralBinding domain shape
genericStructuralBinding =
    StructuralBinding
        { bindingToShape = to . gNominalToShape . from
        , bindingFromShape = to . gNominalFromShape . from
        }