{-# LANGUAGE UndecidableInstances #-} -- required below GHC 9.6 TODO maybe untrue for this

{- | Assertions on precise generic data representation.

I like being real picky with my generic code, disallowing misuse at the type
level. However, this makes it less flexible overall, and is a large chunk of the
code I have to write over and over again.

I mainly care about sanity checks, along the lines of "if the generic
representations looks like this, type error out". So they don't make any
term-level changes.

So, instead of hiding these in generic type class instances, I put them in type
family equations. Now we can turn these checks on and off -- and when they're
on, you have to carry around that fact in your types. Fantastic!

Checks are formed as 'Constraint's, where a failure triggers a 'TypeError' and a
success goes to the empty constraint '()' (@'()' :: 'Constraint'@ as well as
'Type').

These checks were always done on the type-level, but they were "inline" with the
rest of the type class. By pulling them out, we *should* be incurring some
compile-time performance penalty (albeit hopefully minor due to the simple
nature of the checks), but making no change to runtime.
-}

module Generic.Data.Rep.Assert where

import GHC.Generics
import GHC.TypeLits ( TypeError )
import Generic.Data.Rep.Error

import Data.Kind

-- | Generic representation assertions, on the constructor level (bits that come
--   after 'D1').
data GCAssert
  = NoEmpty -- ^ Is not an empty type (does not have 0 constructors)
  | NoSum   -- ^ Is not a sum type (has 0 or 1 constructors)
  | NeedSum -- ^ Is     a sum type (has 0 or >2 constructors)

-- | Convert a generic representation constructor-level assertion "label" to the
--   assertion it represents, and make that assertion.
type family ApplyGCAssert x a where
    ApplyGCAssert 'NoEmpty a = GCNoEmpty a
    ApplyGCAssert 'NoSum   a = GCNoSum   a
    ApplyGCAssert 'NeedSum a = GCNeedSum a

-- | Apply a list of generic representation constructor-level assertions.
type ApplyGCAsserts :: [GCAssert] -> (k -> Type) -> Constraint
type family ApplyGCAsserts ls a where
    ApplyGCAsserts '[]       a = ()
    ApplyGCAsserts (l ': ls) a = (ApplyGCAssert l a, ApplyGCAsserts ls a)

type GCNoEmpty :: (k -> Type) -> Constraint
type family GCNoEmpty a where
    GCNoEmpty V1 = TypeError ENoEmpty
    GCNoEmpty a = ()

type GCNoSum :: (k -> Type) -> Constraint
type family GCNoSum a where
    GCNoSum (_ :+: _) = TypeError EUnexpectedSum
    GCNoSum a = ()

type GCNeedSum :: (k -> Type) -> Constraint
type family GCNeedSum a where
    GCNeedSum (C1 _ _) = TypeError EUnexpectedNonSum
    GCNeedSum a = ()