module Strongweak.Example where import Strongweak import Strongweak.Generic import GHC.Generics ( Generic ) import Data.Word ( Word8 ) import Refined hiding ( Weaken(..) ) import Numeric.Natural data Ex1D (s :: Strength) = Ex1C { forall (s :: Strength). Ex1D s -> SW s Word8 ex1f1 :: SW s Word8 , forall (s :: Strength). Ex1D s -> SW s (Refined (LessThan 100) Natural) ex1f2 :: SW s (Refined (LessThan 100) Natural) } deriving stock (forall x. Ex1D s -> Rep (Ex1D s) x) -> (forall x. Rep (Ex1D s) x -> Ex1D s) -> Generic (Ex1D s) forall x. Rep (Ex1D s) x -> Ex1D s forall x. Ex1D s -> Rep (Ex1D s) x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a forall (s :: Strength) x. Rep (Ex1D s) x -> Ex1D s forall (s :: Strength) x. Ex1D s -> Rep (Ex1D s) x $cto :: forall (s :: Strength) x. Rep (Ex1D s) x -> Ex1D s $cfrom :: forall (s :: Strength) x. Ex1D s -> Rep (Ex1D s) x Generic deriving stock instance Show (Ex1D 'Strong) deriving stock instance Show (Ex1D 'Weak) instance Weaken (Ex1D 'Strong) (Ex1D 'Weak) where weaken :: Ex1D 'Strong -> Ex1D 'Weak weaken = Ex1D 'Strong -> Ex1D 'Weak forall s w. (Generic s, Generic w, GWeaken (Rep s) (Rep w)) => s -> w weakenGeneric instance Strengthen (Ex1D 'Weak) (Ex1D 'Strong) where strengthen :: Ex1D 'Weak -> Validation (NonEmpty StrengthenError) (Ex1D 'Strong) strengthen = Ex1D 'Weak -> Validation (NonEmpty StrengthenError) (Ex1D 'Strong) forall w s. (Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) => w -> Validation (NonEmpty StrengthenError) s strengthenGeneric data Ex2D (s :: Strength) = Ex2C { forall (s :: Strength). Ex2D s -> Ex1D s ex2f1 :: Ex1D s , forall (s :: Strength). Ex2D s -> SW s Word8 ex2f2 :: SW s Word8 } deriving stock (forall x. Ex2D s -> Rep (Ex2D s) x) -> (forall x. Rep (Ex2D s) x -> Ex2D s) -> Generic (Ex2D s) forall x. Rep (Ex2D s) x -> Ex2D s forall x. Ex2D s -> Rep (Ex2D s) x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a forall (s :: Strength) x. Rep (Ex2D s) x -> Ex2D s forall (s :: Strength) x. Ex2D s -> Rep (Ex2D s) x $cto :: forall (s :: Strength) x. Rep (Ex2D s) x -> Ex2D s $cfrom :: forall (s :: Strength) x. Ex2D s -> Rep (Ex2D s) x Generic deriving stock instance Show (Ex2D 'Strong) deriving stock instance Show (Ex2D 'Weak) instance Weaken (Ex2D 'Strong) (Ex2D 'Weak) where weaken :: Ex2D 'Strong -> Ex2D 'Weak weaken = Ex2D 'Strong -> Ex2D 'Weak forall s w. (Generic s, Generic w, GWeaken (Rep s) (Rep w)) => s -> w weakenGeneric instance Strengthen (Ex2D 'Weak) (Ex2D 'Strong) where strengthen :: Ex2D 'Weak -> Validation (NonEmpty StrengthenError) (Ex2D 'Strong) strengthen = Ex2D 'Weak -> Validation (NonEmpty StrengthenError) (Ex2D 'Strong) forall w s. (Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) => w -> Validation (NonEmpty StrengthenError) s strengthenGeneric ex1w :: Ex1D 'Weak ex1w :: Ex1D 'Weak ex1w = SW 'Weak Word8 -> SW 'Weak (Refined (LessThan 100) Natural) -> Ex1D 'Weak forall (s :: Strength). SW s Word8 -> SW s (Refined (LessThan 100) Natural) -> Ex1D s Ex1C Natural SW 'Weak Word8 256 Natural SW 'Weak (Refined (LessThan 100) Natural) 210 ex2w :: Ex2D 'Weak ex2w :: Ex2D 'Weak ex2w = Ex1D 'Weak -> SW 'Weak Word8 -> Ex2D 'Weak forall (s :: Strength). Ex1D s -> SW s Word8 -> Ex2D s Ex2C Ex1D 'Weak ex1w Natural SW 'Weak Word8 256 data ExVoid (s :: Strength) deriving stock (forall x. ExVoid s -> Rep (ExVoid s) x) -> (forall x. Rep (ExVoid s) x -> ExVoid s) -> Generic (ExVoid s) forall x. Rep (ExVoid s) x -> ExVoid s forall x. ExVoid s -> Rep (ExVoid s) x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a forall (s :: Strength) x. Rep (ExVoid s) x -> ExVoid s forall (s :: Strength) x. ExVoid s -> Rep (ExVoid s) x $cto :: forall (s :: Strength) x. Rep (ExVoid s) x -> ExVoid s $cfrom :: forall (s :: Strength) x. ExVoid s -> Rep (ExVoid s) x Generic instance Weaken (ExVoid 'Strong) (ExVoid 'Weak) where weaken :: ExVoid 'Strong -> ExVoid 'Weak weaken = ExVoid 'Strong -> ExVoid 'Weak forall s w. (Generic s, Generic w, GWeaken (Rep s) (Rep w)) => s -> w weakenGeneric instance Strengthen (ExVoid 'Weak) (ExVoid 'Strong) where strengthen :: ExVoid 'Weak -> Validation (NonEmpty StrengthenError) (ExVoid 'Strong) strengthen = ExVoid 'Weak -> Validation (NonEmpty StrengthenError) (ExVoid 'Strong) forall w s. (Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) => w -> Validation (NonEmpty StrengthenError) s strengthenGeneric data ExUnit (s :: Strength) = ExUnit deriving stock (forall x. ExUnit s -> Rep (ExUnit s) x) -> (forall x. Rep (ExUnit s) x -> ExUnit s) -> Generic (ExUnit s) forall x. Rep (ExUnit s) x -> ExUnit s forall x. ExUnit s -> Rep (ExUnit s) x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a forall (s :: Strength) x. Rep (ExUnit s) x -> ExUnit s forall (s :: Strength) x. ExUnit s -> Rep (ExUnit s) x $cto :: forall (s :: Strength) x. Rep (ExUnit s) x -> ExUnit s $cfrom :: forall (s :: Strength) x. ExUnit s -> Rep (ExUnit s) x Generic instance Weaken (ExUnit 'Strong) (ExUnit 'Weak) where weaken :: ExUnit 'Strong -> ExUnit 'Weak weaken = ExUnit 'Strong -> ExUnit 'Weak forall s w. (Generic s, Generic w, GWeaken (Rep s) (Rep w)) => s -> w weakenGeneric instance Strengthen (ExUnit 'Weak) (ExUnit 'Strong) where strengthen :: ExUnit 'Weak -> Validation (NonEmpty StrengthenError) (ExUnit 'Strong) strengthen = ExUnit 'Weak -> Validation (NonEmpty StrengthenError) (ExUnit 'Strong) forall w s. (Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) => w -> Validation (NonEmpty StrengthenError) s strengthenGeneric