{-# LANGUAGE UndecidableInstances #-}
module Binrep.Generic.CBLen where
import Binrep.BLen
import Binrep.Generic.Internal
import GHC.Generics
import GHC.TypeLits
import Data.Kind
import Data.Type.Equality
import Data.Type.Bool
type CBLenGeneric w a = GCBLen w (Rep a)
type family GCBLen w (f :: k -> Type) :: Natural where
GCBLen _ U1 = 0
GCBLen _ (K1 i c) = CBLen c
GCBLen w (l :*: r) = GCBLen w l + GCBLen w r
GCBLen w (l :+: r) = CBLen w + GCBLenCaseMaybe (GCBLenSum w (l :+: r))
GCBLen _ V1 = TypeError GErrRefuseVoid
GCBLen w (M1 _ _ f) = GCBLen w f
type family GCBLenSum w (f :: k -> Type) where
GCBLenSum w (C1 ('MetaCons name _ _) f) = JustX (GCBLen w f) name
GCBLenSum w (l :+: r) = MaybeEq (GCBLenSum w l) (GCBLenSum w r)
type family MaybeEq a b where
MaybeEq (JustX n nName) (JustX m _) = If (n == m) (JustX n nName) NothingX
MaybeEq _ _ = NothingX
type family GCBLenCaseMaybe a where
GCBLenCaseMaybe (JustX n _) = n
GCBLenCaseMaybe NothingX =
TypeError
( 'Text "Two constructors didn't have equal constant size."
':$$: 'Text "Sry dunno how to thread errors thru LOL"
)
data JustX a b
data NothingX