-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Convert between strong and weak representations of types
--   
--   Please see README.md.
@package strongweak
@version 0.11.0

module Strongweak.Util.TypeNats
natVal'' :: forall (n :: Nat). KnownNat n => Natural

module Strongweak.Weaken

-- | Weaken some <tt>a</tt>, relaxing certain invariants.
--   
--   See <a>Strongweak</a> for class design notes and laws.
class Weaken a where {
    
    -- | The weakened type for some type.
    type Weakened a;
}

-- | Weaken some <tt>a</tt> to its associated weak type <tt><a>Weakened</a>
--   a</tt>.
weaken :: Weaken a => a -> Weakened a

-- | The type of <tt>a</tt> after weakening <tt>n</tt> times.
type family WeakenedN (n :: Natural) a

-- | Lift a function on a weak type to the associated strong type by
--   weakening first.
liftWeakF :: Weaken a => (Weakened a -> b) -> a -> b

-- | A "via type" newtype for defining strongweak instances for
--   zero-invariant, coercible newtypes.
--   
--   Use like so:
--   
--   <pre>
--   deriving via <a>SWCoercibly</a> a instance <a>Weaken</a> (<a>Identity</a> a)
--   </pre>
newtype SWCoercibly a
SWCoercibly :: a -> SWCoercibly a
[unSWCoercibly] :: SWCoercibly a -> a
instance forall k (b :: k) a. Strongweak.Weaken.Weaken (Data.Functor.Const.Const a b)
instance (Strongweak.Weaken.Weaken a, Strongweak.Weaken.Weaken b) => Strongweak.Weaken.Weaken (Data.Either.Either a b)
instance Strongweak.Weaken.Weaken (Data.Functor.Identity.Identity a)
instance Strongweak.Weaken.Weaken GHC.Int.Int16
instance Strongweak.Weaken.Weaken GHC.Int.Int32
instance Strongweak.Weaken.Weaken GHC.Int.Int64
instance Strongweak.Weaken.Weaken GHC.Int.Int8
instance Strongweak.Weaken.Weaken a => Strongweak.Weaken.Weaken [a]
instance Strongweak.Weaken.Weaken (GHC.Base.NonEmpty a)
instance forall k (p :: k) a. Strongweak.Weaken.Weaken (Rerefined.Refine.Refined p a)
instance forall k k1 (p :: k) (f :: k1 -> GHC.Types.Type) (a :: k1). Strongweak.Weaken.Weaken (Rerefined.Refine.Refined1 p f a)
instance Strongweak.Weaken.Weaken (Strongweak.Weaken.SWCoercibly a)
instance (Strongweak.Weaken.Weaken a, Strongweak.Weaken.Weaken b) => Strongweak.Weaken.Weaken (a, b)
instance Data.Vector.Generic.Base.Vector v a => Strongweak.Weaken.Weaken (Data.Vector.Generic.Sized.Internal.Vector v n a)
instance Strongweak.Weaken.Weaken GHC.Word.Word16
instance Strongweak.Weaken.Weaken GHC.Word.Word32
instance Strongweak.Weaken.Weaken GHC.Word.Word64
instance Strongweak.Weaken.Weaken GHC.Word.Word8

module Strongweak.Strengthen.Unsafe

-- | Unsafely transform a <tt><a>Weakened</a> a</tt> to an <tt>a</tt>,
--   without asserting invariants.
--   
--   Naturally, you must only even <i>consider</i> using this if you have a
--   guarantee that your value is safe to treat as strong.
--   
--   For example, you may unsafely strengthen some <tt><a>Natural</a>
--   n</tt> into a <a>Word8</a> by unsafely coercing the value, ignoring
--   the possibility that <tt>n &gt;= 255</tt>.
--   
--   What happens if it turns out you're lying to the computer and your
--   weak value doesn't fit in its strong counterpart? That depends on the
--   strengthen.
--   
--   <ul>
--   <li>Numeric coercions should safely overflow.</li>
--   <li>Some will raise an error (e.g. <a>NonEmpty</a>).</li>
--   <li>Others will appear to work, but later explode your computer.</li>
--   </ul>
--   
--   See <a>Strongweak</a> for class design notes and laws.
class Weaken a => UnsafeStrengthen a

-- | Unsafely transform a <tt><a>Weakened</a> a</tt> to its associated
--   strong type <tt>a</tt>.
unsafeStrengthen :: UnsafeStrengthen a => Weakened a -> a
instance forall k (b :: k) a. Strongweak.Strengthen.Unsafe.UnsafeStrengthen (Data.Functor.Const.Const a b)
instance (Strongweak.Strengthen.Unsafe.UnsafeStrengthen a, Strongweak.Strengthen.Unsafe.UnsafeStrengthen b) => Strongweak.Strengthen.Unsafe.UnsafeStrengthen (Data.Either.Either a b)
instance Strongweak.Strengthen.Unsafe.UnsafeStrengthen (Data.Functor.Identity.Identity a)
instance Strongweak.Strengthen.Unsafe.UnsafeStrengthen GHC.Int.Int16
instance Strongweak.Strengthen.Unsafe.UnsafeStrengthen GHC.Int.Int32
instance Strongweak.Strengthen.Unsafe.UnsafeStrengthen GHC.Int.Int64
instance Strongweak.Strengthen.Unsafe.UnsafeStrengthen GHC.Int.Int8
instance Strongweak.Strengthen.Unsafe.UnsafeStrengthen a => Strongweak.Strengthen.Unsafe.UnsafeStrengthen [a]
instance Strongweak.Strengthen.Unsafe.UnsafeStrengthen (GHC.Base.NonEmpty a)
instance forall k (p :: k) a. Strongweak.Strengthen.Unsafe.UnsafeStrengthen (Rerefined.Refine.Refined p a)
instance Strongweak.Strengthen.Unsafe.UnsafeStrengthen (Strongweak.Weaken.SWCoercibly a)
instance (Strongweak.Strengthen.Unsafe.UnsafeStrengthen a, Strongweak.Strengthen.Unsafe.UnsafeStrengthen b) => Strongweak.Strengthen.Unsafe.UnsafeStrengthen (a, b)
instance Data.Vector.Generic.Base.Vector v a => Strongweak.Strengthen.Unsafe.UnsafeStrengthen (Data.Vector.Generic.Sized.Internal.Vector v n a)
instance Strongweak.Strengthen.Unsafe.UnsafeStrengthen GHC.Word.Word16
instance Strongweak.Strengthen.Unsafe.UnsafeStrengthen GHC.Word.Word32
instance Strongweak.Strengthen.Unsafe.UnsafeStrengthen GHC.Word.Word64
instance Strongweak.Strengthen.Unsafe.UnsafeStrengthen GHC.Word.Word8

module Strongweak.Strengthen

-- | Attempt to strengthen some <tt><a>Weakened</a> a</tt>, asserting
--   certain invariants.
--   
--   We take <a>Weaken</a> as a superclass in order to maintain strong/weak
--   type pair consistency. We choose this dependency direction because we
--   treat the strong type as the "canonical" one, so <a>Weaken</a> is the
--   more natural (and straightforward) class to define. That does mean the
--   instances for this class are a little confusingly worded. Alas.
--   
--   See <a>Strongweak</a> for class design notes and laws.
class Weaken a => Strengthen a

-- | Attempt to strengthen some <tt><a>Weakened</a> a</tt> to its
--   associated strong type <tt>a</tt>.
strengthen :: Strengthen a => Weakened a -> Either StrengthenFailure' a

-- | Weaken a strong value, then strengthen it again.
--   
--   Potentially useful if you have previously used <a>unsafeStrengthen</a>
--   and now wish to check the invariants. For example:
--   
--   <pre>
--   &gt;&gt;&gt; restrengthen $ unsafeStrengthen @(Vector 2 Natural) [0]
--   Left ...
--   </pre>
restrengthen :: (Strengthen a, Weaken a) => a -> Either StrengthenFailure' a

-- | Strengthen one numeric type into another.
--   
--   <tt>n</tt> must be "wider" than <tt>m</tt>.
--   
--   <tt><a>FiniteBits</a> m</tt> is for error printing.
strengthenBounded :: forall m n. (Typeable n, Integral n, Typeable m, Integral m, Bounded m, FiniteBits m) => n -> Either StrengthenFailure' m

-- | A failure encountered during strengthening.
--   
--   Strengthening can involve multiple distinct checks. In such cases, you
--   may record multiple failures in a single <a>StrengthenFailure</a> by
--   placing them in the inner failure list and noting their meaning in the
--   detail field.
data StrengthenFailure text
StrengthenFailure :: [text] -> [(text, StrengthenFailure text)] -> StrengthenFailure text

-- | Detail on strengthen failure.
--   
--   We use a list here for the cases where you want multiple lines of
--   detail. Separating with a newline would make prettifying later harder,
--   so we delay.
--   
--   Note that this should probably never be empty. TODO consider
--   <tt>NonEmpty</tt>, but fairly unimportant.
[strengthenFailDetail] :: StrengthenFailure text -> [text]

-- | Optional wrapped failures.
--   
--   The <tt>text</tt> type acts as an index. Its meaning depends on the
--   failure in question, and should be explained in
--   <a>strengthenFailDetail</a>.
[strengthenFailInner] :: StrengthenFailure text -> [(text, StrengthenFailure text)]
type StrengthenFailure' = StrengthenFailure Builder

-- | Shorthand for failing a strengthen with no inner failures.
failStrengthen1 :: [text] -> Either (StrengthenFailure text) a

-- | Shorthand for failing a strengthen.
failStrengthen :: [text] -> [(text, StrengthenFailure text)] -> Either (StrengthenFailure text) a

-- | The weakened type for some type.
type family Weakened a
instance GHC.Show.Show text => GHC.Show.Show (Strongweak.Strengthen.StrengthenFailure text)
instance forall k (b :: k) a. Strongweak.Strengthen.Strengthen (Data.Functor.Const.Const a b)
instance (Strongweak.Strengthen.Strengthen a, Strongweak.Strengthen.Strengthen b) => Strongweak.Strengthen.Strengthen (Data.Either.Either a b)
instance Strongweak.Strengthen.Strengthen (Data.Functor.Identity.Identity a)
instance Strongweak.Strengthen.Strengthen GHC.Int.Int16
instance Strongweak.Strengthen.Strengthen GHC.Int.Int32
instance Strongweak.Strengthen.Strengthen GHC.Int.Int64
instance Strongweak.Strengthen.Strengthen GHC.Int.Int8
instance Strongweak.Strengthen.Strengthen a => Strongweak.Strengthen.Strengthen [a]
instance Strongweak.Strengthen.Strengthen (GHC.Base.NonEmpty a)
instance forall k (p :: k) a. Rerefined.Predicate.Refine p a => Strongweak.Strengthen.Strengthen (Rerefined.Refine.Refined p a)
instance forall k k1 (p :: k) (f :: k1 -> GHC.Types.Type) (a :: k1). Rerefined.Predicate.Refine1 p f => Strongweak.Strengthen.Strengthen (Rerefined.Refine.Refined1 p f a)
instance Strongweak.Strengthen.Strengthen (Strongweak.Weaken.SWCoercibly a)
instance (Strongweak.Strengthen.Strengthen l, Strongweak.Strengthen.Strengthen r) => Strongweak.Strengthen.Strengthen (l, r)
instance (Data.Vector.Generic.Base.Vector v a, GHC.TypeNats.KnownNat n) => Strongweak.Strengthen.Strengthen (Data.Vector.Generic.Sized.Internal.Vector v n a)
instance Strongweak.Strengthen.Strengthen GHC.Word.Word16
instance Strongweak.Strengthen.Strengthen GHC.Word.Word32
instance Strongweak.Strengthen.Strengthen GHC.Word.Word64
instance Strongweak.Strengthen.Strengthen GHC.Word.Word8


-- | <a>strengthen</a> over generic representations.
--   
--   As with base instances, generic strengthening collates all failures
--   rather than short-circuiting on the first failure. Failures are
--   annotated with precise information describing where the failure
--   occurred:
--   
--   <ul>
--   <li>data type name</li>
--   <li>constructor name</li>
--   <li>field index</li>
--   <li>field name (if present)</li>
--   </ul>
module Strongweak.Strengthen.Generic

-- | Strengthen a value generically.
--   
--   The weak and strong types must be <i>compatible</i>. See
--   <a>Generic</a> for the definition of compatibility in this context.
strengthenGeneric :: (Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) => w -> Either StrengthenFailure' s

-- | Generic strengthening at the datatype level.
class GStrengthenD (w :: k -> Type) (s :: k -> Type)
gstrengthenD :: forall (p :: k). GStrengthenD w s => w p -> Either StrengthenFailure' (s p)

-- | Generic strengthening at the constructor sum level.
class GStrengthenC (wdn :: Symbol) (sdn :: Symbol) (w :: k -> Type) (s :: k -> Type)
gstrengthenC :: forall (p :: k). GStrengthenC wdn sdn w s => w p -> Either StrengthenFailure' (s p)
class ReifyCstrs (ld :: Symbol) (lc :: Symbol) (rd :: Symbol) (rc :: Symbol)
reifyCstrs :: ReifyCstrs ld lc rd rc => Builder

-- | Generic strengthening at the constructor level.
class GStrengthenS (i :: Natural) (w :: k -> Type) (s :: k -> Type)
gstrengthenS :: forall (p :: k). GStrengthenS i w s => w p -> Either [(Builder, StrengthenFailure')] (s p)
class ReifySelector (i :: Natural) (l :: Maybe Symbol) (r :: Maybe Symbol)
reifySelector :: ReifySelector i l r => Builder
(.>) :: (a -> b) -> (b -> c) -> a -> c
type family ProdArity (f :: k -> Type) :: Natural
instance forall k (w :: k -> GHC.Types.Type) (s :: k -> GHC.Types.Type) (wcd :: GHC.Types.Symbol) (wcn :: GHC.Types.Symbol) (scd :: GHC.Types.Symbol) (scn :: GHC.Types.Symbol) (_wmc2 :: GHC.Generics.FixityI) (_wmc3 :: GHC.Types.Bool) (_smc2 :: GHC.Generics.FixityI) (_smc3 :: GHC.Types.Bool). (Strongweak.Strengthen.Generic.GStrengthenS 0 w s, Strongweak.Strengthen.Generic.ReifyCstrs wcd wcn scd scn) => Strongweak.Strengthen.Generic.GStrengthenC wcd scd (GHC.Generics.C1 ('GHC.Generics.MetaCons wcn _wmc2 _wmc3) w) (GHC.Generics.C1 ('GHC.Generics.MetaCons scn _smc2 _smc3) s)
instance forall k (wdn :: GHC.Types.Symbol) (sdn :: GHC.Types.Symbol) (wl :: k -> GHC.Types.Type) (sl :: k -> GHC.Types.Type) (wr :: k -> GHC.Types.Type) (sr :: k -> GHC.Types.Type). (Strongweak.Strengthen.Generic.GStrengthenC wdn sdn wl sl, Strongweak.Strengthen.Generic.GStrengthenC wdn sdn wr sr) => Strongweak.Strengthen.Generic.GStrengthenC wdn sdn (wl GHC.Generics.:+: wr) (sl GHC.Generics.:+: sr)
instance Strongweak.Strengthen.Generic.GStrengthenC wdn sdn GHC.Generics.V1 GHC.Generics.V1
instance forall k (wdn :: GHC.Types.Symbol) (sdn :: GHC.Types.Symbol) (w :: k -> GHC.Types.Type) (s :: k -> GHC.Types.Type) (_wmd2 :: GHC.Types.Symbol) (_wmd3 :: GHC.Types.Symbol) (_wmd4 :: GHC.Types.Bool) (_smd2 :: GHC.Types.Symbol) (_smd3 :: GHC.Types.Symbol) (_smd4 :: GHC.Types.Bool). Strongweak.Strengthen.Generic.GStrengthenC wdn sdn w s => Strongweak.Strengthen.Generic.GStrengthenD (GHC.Generics.D1 ('GHC.Generics.MetaData wdn _wmd2 _wmd3 _wmd4) w) (GHC.Generics.D1 ('GHC.Generics.MetaData sdn _smd2 _smd3 _smd4) s)
instance forall k (i :: GHC.Num.Natural.Natural) (wl :: k -> GHC.Types.Type) (sl :: k -> GHC.Types.Type) (wr :: k -> GHC.Types.Type) (sr :: k -> GHC.Types.Type). (Strongweak.Strengthen.Generic.GStrengthenS i wl sl, Strongweak.Strengthen.Generic.GStrengthenS (i GHC.TypeNats.+ Strongweak.Strengthen.Generic.ProdArity wl) wr sr) => Strongweak.Strengthen.Generic.GStrengthenS i (wl GHC.Generics.:*: wr) (sl GHC.Generics.:*: sr)
instance (Strongweak.Weaken.Weakened s GHC.Types.~ w, Strongweak.Strengthen.Strengthen s, Strongweak.Strengthen.Generic.ReifySelector i wmr smr) => Strongweak.Strengthen.Generic.GStrengthenS i (GHC.Generics.S1 ('GHC.Generics.MetaSel wmr _wms2 _wms3 _wms4) (GHC.Generics.Rec0 w)) (GHC.Generics.S1 ('GHC.Generics.MetaSel smr _sms2 _sms3 _sms4) (GHC.Generics.Rec0 s))
instance Strongweak.Strengthen.Generic.GStrengthenS i (GHC.Generics.S1 ('GHC.Generics.MetaSel _wms1 _wms2 _wms3 _wms4) (GHC.Generics.Rec0 a)) (GHC.Generics.S1 ('GHC.Generics.MetaSel _sms1 _sms2 _sms3 _sms4) (GHC.Generics.Rec0 a))
instance Strongweak.Strengthen.Generic.GStrengthenS i GHC.Generics.U1 GHC.Generics.U1
instance (GHC.TypeLits.KnownSymbol ld, GHC.TypeLits.KnownSymbol lc, GHC.TypeLits.KnownSymbol rd, GHC.TypeLits.KnownSymbol rc) => Strongweak.Strengthen.Generic.ReifyCstrs ld lc rd rc
instance (GHC.TypeLits.KnownSymbol d, GHC.TypeLits.KnownSymbol c) => Strongweak.Strengthen.Generic.ReifyCstrs d c d c
instance (GHC.TypeNats.KnownNat i, GHC.TypeLits.KnownSymbol lnm) => Strongweak.Strengthen.Generic.ReifySelector i ('GHC.Maybe.Just lnm) ('GHC.Maybe.Just lnm)
instance (GHC.TypeNats.KnownNat i, GHC.TypeLits.KnownSymbol lnm, GHC.TypeLits.KnownSymbol rnm) => Strongweak.Strengthen.Generic.ReifySelector i ('GHC.Maybe.Just lnm) ('GHC.Maybe.Just rnm)
instance (GHC.TypeNats.KnownNat i, GHC.TypeLits.KnownSymbol lnm) => Strongweak.Strengthen.Generic.ReifySelector i ('GHC.Maybe.Just lnm) 'GHC.Maybe.Nothing
instance (GHC.TypeNats.KnownNat i, GHC.TypeLits.KnownSymbol rnm) => Strongweak.Strengthen.Generic.ReifySelector i 'GHC.Maybe.Nothing ('GHC.Maybe.Just rnm)
instance GHC.TypeNats.KnownNat i => Strongweak.Strengthen.Generic.ReifySelector i 'GHC.Maybe.Nothing 'GHC.Maybe.Nothing


-- | <a>weaken</a> over generic representations.
module Strongweak.Weaken.Generic

-- | Weaken a value generically.
--   
--   The weak and strong types must be <i>compatible</i>. See
--   <a>Generic</a> for the definition of compatibility in this context.
weakenGeneric :: (Generic s, Generic w, GWeaken (Rep s) (Rep w)) => s -> w
class GWeaken (s :: k -> Type) (w :: k -> Type)
gweaken :: forall (p :: k). GWeaken s w => s p -> w p
instance forall k (ls :: k -> GHC.Types.Type) (lw :: k -> GHC.Types.Type) (rs :: k -> GHC.Types.Type) (rw :: k -> GHC.Types.Type). (Strongweak.Weaken.Generic.GWeaken ls lw, Strongweak.Weaken.Generic.GWeaken rs rw) => Strongweak.Weaken.Generic.GWeaken (ls GHC.Generics.:*: rs) (lw GHC.Generics.:*: rw)
instance forall k (ls :: k -> GHC.Types.Type) (lw :: k -> GHC.Types.Type) (rs :: k -> GHC.Types.Type) (rw :: k -> GHC.Types.Type). (Strongweak.Weaken.Generic.GWeaken ls lw, Strongweak.Weaken.Generic.GWeaken rs rw) => Strongweak.Weaken.Generic.GWeaken (ls GHC.Generics.:+: rs) (lw GHC.Generics.:+: rw)
instance Strongweak.Weaken.Generic.GWeaken (GHC.Generics.Rec0 s) (GHC.Generics.Rec0 s)
instance (Strongweak.Weaken.Weaken s, Strongweak.Weaken.Weakened s GHC.Types.~ w) => Strongweak.Weaken.Generic.GWeaken (GHC.Generics.Rec0 s) (GHC.Generics.Rec0 w)
instance forall k (s :: k -> GHC.Types.Type) (w :: k -> GHC.Types.Type) is (ms :: GHC.Generics.Meta) iw (mw :: GHC.Generics.Meta). Strongweak.Weaken.Generic.GWeaken s w => Strongweak.Weaken.Generic.GWeaken (GHC.Generics.M1 is ms s) (GHC.Generics.M1 iw mw w)
instance Strongweak.Weaken.Generic.GWeaken GHC.Generics.U1 GHC.Generics.U1
instance Strongweak.Weaken.Generic.GWeaken GHC.Generics.V1 GHC.Generics.V1


-- | <a>WeakenN</a> internals.
--   
--   Just in case. You shouldn't need these, but they might be fun to look
--   at.
--   
--   <b>Internal module. Exports may change without warning. Try not to
--   use.</b>
module Strongweak.WeakenN.Internal
class WeakenWeakenN (n :: Natural) a
weakenWeakenN :: WeakenWeakenN n a => a -> WeakenedN n a

-- | Inverted inductive <a>WeakenedN</a>case.
--   
--   <tt>n</tt> must not be 0.
weakenedNRL1 :: forall (n :: Natural) a. WeakenedN (n - 1) (Weakened a) -> WeakenedN n a
class WeakenWeakenN n a => StrengthenWeakenN (n :: Natural) a
strengthenWeakenN :: StrengthenWeakenN n a => WeakenedN n a -> Either StrengthenFailure' a

-- | Inductive <a>WeakenedN</a>case.
--   
--   <tt>n</tt> must not be 0.
weakenedNLR1 :: forall (n :: Natural) a. WeakenedN n a -> WeakenedN (n - 1) (Weakened a)
instance (Strongweak.Strengthen.Strengthen a, Strongweak.WeakenN.Internal.StrengthenWeakenN (n GHC.TypeNats.- 1) (Strongweak.Weaken.Weakened a)) => Strongweak.WeakenN.Internal.StrengthenWeakenN n a
instance Strongweak.WeakenN.Internal.StrengthenWeakenN 0 a
instance (Strongweak.Weaken.Weaken a, Strongweak.WeakenN.Internal.WeakenWeakenN (n GHC.TypeNats.- 1) (Strongweak.Weaken.Weakened a)) => Strongweak.WeakenN.Internal.WeakenWeakenN n a
instance Strongweak.WeakenN.Internal.WeakenWeakenN 0 a

module Strongweak.WeakenN

-- | When weakening (or strengthening), chain the operation <tt>n</tt>
--   times.
--   
--   You may achieve this without extra newtypes by nesting uses of
--   <a>SW</a>. However, strongweak generics can't handle this, forcing you
--   to write manual instances.
--   
--   <a>WeakenN</a> provides this nesting behaviour in a type. In return
--   for adding a boring newtype layer to the strong representation, you
--   can chain weakening and strengthenings without having to write them
--   manually.
--   
--   The type works as follows:
--   
--   <pre>
--   Weakened (WeakenN 0 a) = a
--   Weakened (WeakenN 1 a) = Weakened a
--   Weakened (WeakenN 2 a) = Weakened (Weakened a)
--   Weakened (WeakenN n a) = WeakenedN n a
--   </pre>
--   
--   And so on. (This type is only much use from <tt>n = 2</tt> onwards.)
newtype WeakenN (n :: Natural) a
WeakenN :: a -> WeakenN (n :: Natural) a
[unWeakenN] :: WeakenN (n :: Natural) a -> a
instance GHC.Classes.Eq a => GHC.Classes.Eq (Strongweak.WeakenN.WeakenN n a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Strongweak.WeakenN.WeakenN n a)
instance GHC.Show.Show a => GHC.Show.Show (Strongweak.WeakenN.WeakenN n a)
instance Strongweak.WeakenN.Internal.StrengthenWeakenN n a => Strongweak.Strengthen.Strengthen (Strongweak.WeakenN.WeakenN n a)
instance Strongweak.WeakenN.Internal.WeakenWeakenN n a => Strongweak.Weaken.Weaken (Strongweak.WeakenN.WeakenN n a)


-- | Definitions using a type-level strength switch.
module Strongweak.Strength

-- | Strength enumeration: it's either strong, or weak.
--   
--   Primarily interesting at the type level (using DataKinds).
data Strength
Strong :: Strength
Weak :: Strength

-- | Get either the strong or weak representation of a type, depending on
--   the type-level "switch" provided.
--   
--   This is intended to be used in data types that take a <a>Strength</a>
--   type. Define your type using strong fields wrapped in <tt>SW s</tt>.
--   You then get the weak representation for free, using the same
--   definition.
--   
--   <pre>
--   data A (s :: Strength) = A
--     { a1 :: SW s Word8
--     , a2 :: String }
--   </pre>
type family SW (s :: Strength) a

-- | Shortcut for a <a>SW</a>-wrapped <a>WeakenN</a>.
type SWN (s :: Strength) (n :: Natural) a = SW s WeakenN n a


-- | Generic <a>strengthen</a> and <a>weaken</a>.
module Strongweak.Generic

-- | Weaken a value generically.
--   
--   The weak and strong types must be <i>compatible</i>. See
--   <a>Generic</a> for the definition of compatibility in this context.
weakenGeneric :: (Generic s, Generic w, GWeaken (Rep s) (Rep w)) => s -> w

-- | Strengthen a value generically.
--   
--   The weak and strong types must be <i>compatible</i>. See
--   <a>Generic</a> for the definition of compatibility in this context.
strengthenGeneric :: (Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) => w -> Either StrengthenFailure' s

-- | <tt>DerivingVia</tt> wrapper for strongweak instances.
--   
--   We can't use <a>Generically</a> conveniently because we need to talk
--   about two data types, not one -- we would have to do something like
--   <tt><a>Generically</a> (<tt>Tagged</tt> w s)</tt>, which is ugly. So
--   we instead define our own adorable little "via type" here!
--   
--   Use like so:
--   
--   <pre>
--   data XYZ (s :: Strength) = XYZ
--     { xyz1 :: SW s Word8
--     , xyz2 :: Word8
--     , xyz3 :: ()
--     } deriving stock Generic
--   deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Weaken (XYZ 'Strong)
--   deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Strengthen (XYZ 'Strong)
--   </pre>
--   
--   Regrettably, use of this requires UndecidableInstances.
newtype GenericallySW s w
GenericallySW :: s -> GenericallySW s w
[unGenericallySW] :: GenericallySW s w -> s

-- | <a>GenericallySW</a> where the type takes a <a>Strength</a> in its
--   last type var.
--   
--   Shorter instances for types of a certain shape.
--   
--   Regrettably, use of this requires UndecidableInstances.
newtype GenericallySW0 (f :: Strength -> Type)
GenericallySW0 :: f 'Strong -> GenericallySW0 (f :: Strength -> Type)
[unGenericallySW0] :: GenericallySW0 (f :: Strength -> Type) -> f 'Strong
instance (GHC.Generics.Generic s, GHC.Generics.Generic w, Strongweak.Strengthen.Generic.GStrengthenD (GHC.Generics.Rep w) (GHC.Generics.Rep s), Strongweak.Weaken.Weaken (Strongweak.Generic.GenericallySW s w)) => Strongweak.Strengthen.Strengthen (Strongweak.Generic.GenericallySW s w)
instance (GHC.Generics.Generic (f 'Strongweak.Strength.Strong), GHC.Generics.Generic (f 'Strongweak.Strength.Weak), Strongweak.Strengthen.Generic.GStrengthenD (GHC.Generics.Rep (f 'Strongweak.Strength.Weak)) (GHC.Generics.Rep (f 'Strongweak.Strength.Strong)), Strongweak.Weaken.Weaken (Strongweak.Generic.GenericallySW0 f)) => Strongweak.Strengthen.Strengthen (Strongweak.Generic.GenericallySW0 f)
instance (GHC.Generics.Generic s, GHC.Generics.Generic w, Strongweak.Weaken.Generic.GWeaken (GHC.Generics.Rep s) (GHC.Generics.Rep w)) => Strongweak.Weaken.Weaken (Strongweak.Generic.GenericallySW s w)
instance (GHC.Generics.Generic (f 'Strongweak.Strength.Strong), GHC.Generics.Generic (f 'Strongweak.Strength.Weak), Strongweak.Weaken.Generic.GWeaken (GHC.Generics.Rep (f 'Strongweak.Strength.Strong)) (GHC.Generics.Rep (f 'Strongweak.Strength.Weak))) => Strongweak.Weaken.Weaken (Strongweak.Generic.GenericallySW0 f)


-- | Main import module for basic use.
--   
--   For defining <a>Strengthen</a> instances, import
--   <a>Strongweak.Strengthen</a>.
module Strongweak

-- | Weaken some <tt>a</tt>, relaxing certain invariants.
--   
--   See <a>Strongweak</a> for class design notes and laws.
class Weaken a where {
    
    -- | The weakened type for some type.
    type Weakened a;
}

-- | Weaken some <tt>a</tt> to its associated weak type <tt><a>Weakened</a>
--   a</tt>.
weaken :: Weaken a => a -> Weakened a

-- | Attempt to strengthen some <tt><a>Weakened</a> a</tt>, asserting
--   certain invariants.
--   
--   We take <a>Weaken</a> as a superclass in order to maintain strong/weak
--   type pair consistency. We choose this dependency direction because we
--   treat the strong type as the "canonical" one, so <a>Weaken</a> is the
--   more natural (and straightforward) class to define. That does mean the
--   instances for this class are a little confusingly worded. Alas.
--   
--   See <a>Strongweak</a> for class design notes and laws.
class Weaken a => Strengthen a

-- | Attempt to strengthen some <tt><a>Weakened</a> a</tt> to its
--   associated strong type <tt>a</tt>.
strengthen :: Strengthen a => Weakened a -> Either StrengthenFailure' a

-- | When weakening (or strengthening), chain the operation <tt>n</tt>
--   times.
--   
--   You may achieve this without extra newtypes by nesting uses of
--   <a>SW</a>. However, strongweak generics can't handle this, forcing you
--   to write manual instances.
--   
--   <a>WeakenN</a> provides this nesting behaviour in a type. In return
--   for adding a boring newtype layer to the strong representation, you
--   can chain weakening and strengthenings without having to write them
--   manually.
--   
--   The type works as follows:
--   
--   <pre>
--   Weakened (WeakenN 0 a) = a
--   Weakened (WeakenN 1 a) = Weakened a
--   Weakened (WeakenN 2 a) = Weakened (Weakened a)
--   Weakened (WeakenN n a) = WeakenedN n a
--   </pre>
--   
--   And so on. (This type is only much use from <tt>n = 2</tt> onwards.)
newtype WeakenN (n :: Natural) a
WeakenN :: a -> WeakenN (n :: Natural) a
[unWeakenN] :: WeakenN (n :: Natural) a -> a

-- | A "via type" newtype for defining strongweak instances for
--   zero-invariant, coercible newtypes.
--   
--   Use like so:
--   
--   <pre>
--   deriving via <a>SWCoercibly</a> a instance <a>Weaken</a> (<a>Identity</a> a)
--   </pre>
newtype SWCoercibly a
SWCoercibly :: a -> SWCoercibly a
[unSWCoercibly] :: SWCoercibly a -> a

-- | Lift a function on a weak type to the associated strong type by
--   weakening first.
liftWeakF :: Weaken a => (Weakened a -> b) -> a -> b

-- | Strength enumeration: it's either strong, or weak.
--   
--   Primarily interesting at the type level (using DataKinds).
data Strength
Strong :: Strength
Weak :: Strength

-- | Get either the strong or weak representation of a type, depending on
--   the type-level "switch" provided.
--   
--   This is intended to be used in data types that take a <a>Strength</a>
--   type. Define your type using strong fields wrapped in <tt>SW s</tt>.
--   You then get the weak representation for free, using the same
--   definition.
--   
--   <pre>
--   data A (s :: Strength) = A
--     { a1 :: SW s Word8
--     , a2 :: String }
--   </pre>
type family SW (s :: Strength) a

-- | Shortcut for a <a>SW</a>-wrapped <a>WeakenN</a>.
type SWN (s :: Strength) (n :: Natural) a = SW s WeakenN n a