{-# 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 = ()