module Strongweak.WeakenN ( WeakenN(..) ) where

import Strongweak.WeakenN.Internal
import Strongweak.Weaken ( Weaken(..), type WeakenedN )
import Strongweak.Strengthen ( Strengthen(..) )
import GHC.TypeNats ( type Natural )

{- | When weakening (or strengthening), chain the operation @n@ times.

You may achieve this without extra newtypes by nesting uses of
'Strongweak.Weaken.SW'. However, strongweak generics can't handle this, forcing
you to write manual instances.

'WeakenN' 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:

@
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
@

And so on. (This type is only much use from @n = 2@ onwards.)
-}
newtype WeakenN (n :: Natural) a = WeakenN { forall (n :: Natural) a. WeakenN n a -> a
unWeakenN :: a }
    deriving stock Int -> WeakenN n a -> ShowS
[WeakenN n a] -> ShowS
WeakenN n a -> String
(Int -> WeakenN n a -> ShowS)
-> (WeakenN n a -> String)
-> ([WeakenN n a] -> ShowS)
-> Show (WeakenN n a)
forall (n :: Natural) a. Show a => Int -> WeakenN n a -> ShowS
forall (n :: Natural) a. Show a => [WeakenN n a] -> ShowS
forall (n :: Natural) a. Show a => WeakenN n a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (n :: Natural) a. Show a => Int -> WeakenN n a -> ShowS
showsPrec :: Int -> WeakenN n a -> ShowS
$cshow :: forall (n :: Natural) a. Show a => WeakenN n a -> String
show :: WeakenN n a -> String
$cshowList :: forall (n :: Natural) a. Show a => [WeakenN n a] -> ShowS
showList :: [WeakenN n a] -> ShowS
Show
    deriving (Eq (WeakenN n a)
Eq (WeakenN n a) =>
(WeakenN n a -> WeakenN n a -> Ordering)
-> (WeakenN n a -> WeakenN n a -> Bool)
-> (WeakenN n a -> WeakenN n a -> Bool)
-> (WeakenN n a -> WeakenN n a -> Bool)
-> (WeakenN n a -> WeakenN n a -> Bool)
-> (WeakenN n a -> WeakenN n a -> WeakenN n a)
-> (WeakenN n a -> WeakenN n a -> WeakenN n a)
-> Ord (WeakenN n a)
WeakenN n a -> WeakenN n a -> Bool
WeakenN n a -> WeakenN n a -> Ordering
WeakenN n a -> WeakenN n a -> WeakenN n a
forall (n :: Natural) a. Ord a => Eq (WeakenN n a)
forall (n :: Natural) a.
Ord a =>
WeakenN n a -> WeakenN n a -> Bool
forall (n :: Natural) a.
Ord a =>
WeakenN n a -> WeakenN n a -> Ordering
forall (n :: Natural) a.
Ord a =>
WeakenN n a -> WeakenN n a -> WeakenN n a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: forall (n :: Natural) a.
Ord a =>
WeakenN n a -> WeakenN n a -> Ordering
compare :: WeakenN n a -> WeakenN n a -> Ordering
$c< :: forall (n :: Natural) a.
Ord a =>
WeakenN n a -> WeakenN n a -> Bool
< :: WeakenN n a -> WeakenN n a -> Bool
$c<= :: forall (n :: Natural) a.
Ord a =>
WeakenN n a -> WeakenN n a -> Bool
<= :: WeakenN n a -> WeakenN n a -> Bool
$c> :: forall (n :: Natural) a.
Ord a =>
WeakenN n a -> WeakenN n a -> Bool
> :: WeakenN n a -> WeakenN n a -> Bool
$c>= :: forall (n :: Natural) a.
Ord a =>
WeakenN n a -> WeakenN n a -> Bool
>= :: WeakenN n a -> WeakenN n a -> Bool
$cmax :: forall (n :: Natural) a.
Ord a =>
WeakenN n a -> WeakenN n a -> WeakenN n a
max :: WeakenN n a -> WeakenN n a -> WeakenN n a
$cmin :: forall (n :: Natural) a.
Ord a =>
WeakenN n a -> WeakenN n a -> WeakenN n a
min :: WeakenN n a -> WeakenN n a -> WeakenN n a
Ord, WeakenN n a -> WeakenN n a -> Bool
(WeakenN n a -> WeakenN n a -> Bool)
-> (WeakenN n a -> WeakenN n a -> Bool) -> Eq (WeakenN n a)
forall (n :: Natural) a. Eq a => WeakenN n a -> WeakenN n a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Natural) a. Eq a => WeakenN n a -> WeakenN n a -> Bool
== :: WeakenN n a -> WeakenN n a -> Bool
$c/= :: forall (n :: Natural) a. Eq a => WeakenN n a -> WeakenN n a -> Bool
/= :: WeakenN n a -> WeakenN n a -> Bool
Eq) via a

instance WeakenWeakenN n a => Weaken (WeakenN n a) where
    type Weakened (WeakenN n a) = WeakenedN n a
    weaken :: WeakenN n a -> Weakened (WeakenN n a)
weaken = forall (n :: Natural) a. WeakenWeakenN n a => a -> WeakenedN n a
weakenWeakenN @n @a (a -> WeakenedN n a)
-> (WeakenN n a -> a) -> WeakenN n a -> WeakenedN n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WeakenN n a -> a
forall (n :: Natural) a. WeakenN n a -> a
unWeakenN

instance StrengthenWeakenN n a => Strengthen (WeakenN n a) where
    strengthen :: Weakened (WeakenN n a) -> Either StrengthenFailure' (WeakenN n a)
strengthen = (a -> WeakenN n a)
-> Either StrengthenFailure' a
-> Either StrengthenFailure' (WeakenN n a)
forall a b.
(a -> b)
-> Either StrengthenFailure' a -> Either StrengthenFailure' b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> WeakenN n a
forall (n :: Natural) a. a -> WeakenN n a
WeakenN (Either StrengthenFailure' a
 -> Either StrengthenFailure' (WeakenN n a))
-> (WeakenedN n a -> Either StrengthenFailure' a)
-> WeakenedN n a
-> Either StrengthenFailure' (WeakenN n a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Natural) a.
StrengthenWeakenN n a =>
WeakenedN n a -> Either StrengthenFailure' a
strengthenWeakenN @n @a