module Strongweak.SW where
import Refined ( Refined )
import Data.Vector.Sized ( Vector )
import Data.Kind ( Type )
import Data.Word
import Data.Int
import Numeric.Natural ( Natural )
data Strength = Strong | Weak
type family Weak (a :: Type) :: Type
type instance Weak Word8 = Natural
type instance Weak Word16 = Natural
type instance Weak Word32 = Natural
type instance Weak Word64 = Natural
type instance Weak Int8 = Integer
type instance Weak Int16 = Integer
type instance Weak Int32 = Integer
type instance Weak Int64 = Integer
type instance Weak (Vector n a) = [a]
type instance Weak (Refined p a) = a
type family SW (s :: Strength) a :: Type where
SW 'Strong a = a
SW 'Weak a = Weak a