{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE AllowAmbiguousTypes #-} -- StrengthenN, and typeRep'
-- StrengthenN type families in constraints
{-# LANGUAGE UndecidableInstances #-}

module Strongweak.Strengthen
  (
  -- * 'Strengthen' class
    Strengthen(..)
  , restrengthen
  , StrengthenN(strengthenN)

  -- ** Helpers
  , strengthenBounded

  -- * Strengthen failures
  , StrengthenFailure(..)
  , StrengthenFailure'
  , failStrengthen1
  , failStrengthen

  -- * Re-exports
  , Strongweak.Weaken.Weakened
  ) where

import Strongweak.Weaken ( Weaken(Weakened) )

import Strongweak.Weaken ( Weaken(weaken) )

import Strongweak.Weaken ( SWCoercibly(..) )

import Strongweak.Util.TypeNats ( natVal'' )

import GHC.TypeNats ( KnownNat )
import Data.Word
import Data.Int
import Rerefined
import Data.Vector.Generic.Sized qualified as VGS -- Shazbot!
import Data.Vector.Generic qualified as VG
import Data.Functor.Identity
import Data.Functor.Const
import Data.List.NonEmpty qualified as NonEmpty
import Data.List.NonEmpty ( NonEmpty )

import Data.Text.Builder.Linear qualified as TBL
import GHC.Exts ( fromString )

import Data.Bits ( FiniteBits )

import Data.Typeable ( Typeable, TypeRep, typeRep, Proxy(Proxy) )

-- for strengthenN
import GHC.TypeNats ( type Natural, type (-) )
import Strongweak.Weaken ( type WeakenedN, WeakenN )
import Unsafe.Coerce ( unsafeCoerce )

{- | Attempt to strengthen some @'Weakened' a@, asserting certain invariants.

We take 'Weaken' 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 'Weaken' is the more natural (and
straightforward) class to define. That does mean the instances for this class
are a little confusingly worded. Alas.

See "Strongweak" for class design notes and laws.
-}
class Weaken a => Strengthen a where
    -- | Attempt to strengthen some @'Weakened' a@ to its associated strong type
    --   @a@.
    strengthen :: Weakened a -> Either StrengthenFailure' a

-- | Weaken a strong value, then strengthen it again.
--
-- Potentially useful if you have previously used
-- 'Strongweak.Strengthen.Unsafe.unsafeStrengthen' and now wish to check the
-- invariants. For example:
--
-- >>> restrengthen $ unsafeStrengthen @(Vector 2 Natural) [0]
-- Left ...
restrengthen :: (Strengthen a, Weaken a) => a -> Either StrengthenFailure' a
restrengthen :: forall a.
(Strengthen a, Weaken a) =>
a -> Either StrengthenFailure' a
restrengthen = Weakened a -> Either StrengthenFailure' a
forall a. Strengthen a => Weakened a -> Either StrengthenFailure' a
strengthen (Weakened a -> Either StrengthenFailure' a)
-> (a -> Weakened a) -> a -> Either StrengthenFailure' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Weakened a
forall a. Weaken a => a -> Weakened a
weaken

-- | A failure encountered during strengthening.
--
-- Strengthening can involve multiple distinct checks. In such cases, you may
-- record multiple failures in a single 'StrengthenFailure' by placing them in
-- the inner failure list and noting their meaning in the detail field.
data StrengthenFailure text = StrengthenFailure
  { forall text. StrengthenFailure text -> [text]
strengthenFailDetail :: [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 @NonEmpty@,
  -- but fairly unimportant.

  , forall text.
StrengthenFailure text -> [(text, StrengthenFailure text)]
strengthenFailInner  :: [(text, StrengthenFailure text)]
  -- ^ Optional wrapped failures.
  --
  -- The @text@ type acts as an index. Its meaning depends on the failure
  -- in question, and should be explained in 'strengthenFailDetail'.
  } deriving stock Int -> StrengthenFailure text -> ShowS
[StrengthenFailure text] -> ShowS
StrengthenFailure text -> String
(Int -> StrengthenFailure text -> ShowS)
-> (StrengthenFailure text -> String)
-> ([StrengthenFailure text] -> ShowS)
-> Show (StrengthenFailure text)
forall text. Show text => Int -> StrengthenFailure text -> ShowS
forall text. Show text => [StrengthenFailure text] -> ShowS
forall text. Show text => StrengthenFailure text -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall text. Show text => Int -> StrengthenFailure text -> ShowS
showsPrec :: Int -> StrengthenFailure text -> ShowS
$cshow :: forall text. Show text => StrengthenFailure text -> String
show :: StrengthenFailure text -> String
$cshowList :: forall text. Show text => [StrengthenFailure text] -> ShowS
showList :: [StrengthenFailure text] -> ShowS
Show

type StrengthenFailure' = StrengthenFailure TBL.Builder

-- | Shorthand for failing a strengthen.
failStrengthen
    :: [text] -> [(text, StrengthenFailure text)]
    -> Either (StrengthenFailure text) a
failStrengthen :: forall text a.
[text]
-> [(text, StrengthenFailure text)]
-> Either (StrengthenFailure text) a
failStrengthen [text]
t [(text, StrengthenFailure text)]
fs = StrengthenFailure text -> Either (StrengthenFailure text) a
forall a b. a -> Either a b
Left (StrengthenFailure text -> Either (StrengthenFailure text) a)
-> StrengthenFailure text -> Either (StrengthenFailure text) a
forall a b. (a -> b) -> a -> b
$ [text]
-> [(text, StrengthenFailure text)] -> StrengthenFailure text
forall text.
[text]
-> [(text, StrengthenFailure text)] -> StrengthenFailure text
StrengthenFailure [text]
t [(text, StrengthenFailure text)]
fs

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

-- TODO add a via type for obtaining strengthen via unsafestrengthen :)
-- should be permitted only for non-failing, zero invariant strengthens

instance Strengthen (SWCoercibly a) where
    strengthen :: Weakened (SWCoercibly a)
-> Either StrengthenFailure' (SWCoercibly a)
strengthen = SWCoercibly a -> Either StrengthenFailure' (SWCoercibly a)
forall a b. b -> Either a b
Right (SWCoercibly a -> Either StrengthenFailure' (SWCoercibly a))
-> (a -> SWCoercibly a)
-> a
-> Either StrengthenFailure' (SWCoercibly a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SWCoercibly a
forall a. a -> SWCoercibly a
SWCoercibly

deriving via SWCoercibly a instance Strengthen (Identity a)
deriving via SWCoercibly a instance Strengthen (Const a b)

-- | Strengthen a type by refining it with a predicate.
instance Refine p a => Strengthen (Refined p a) where
    strengthen :: Weakened (Refined p a) -> Either StrengthenFailure' (Refined p a)
strengthen = a -> Either RefineFailure (Refined p a)
forall {k} (p :: k) a.
Refine p a =>
a -> Either RefineFailure (Refined p a)
refine (a -> Either RefineFailure (Refined p a))
-> (Either RefineFailure (Refined p a)
    -> Either StrengthenFailure' (Refined p a))
-> a
-> Either StrengthenFailure' (Refined p a)
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> \case
      Right Refined p a
ra -> Refined p a -> Either StrengthenFailure' (Refined p a)
forall a b. b -> Either a b
Right Refined p a
ra
      Left  RefineFailure
rf -> [Builder] -> Either StrengthenFailure' (Refined p a)
forall text a. [text] -> Either (StrengthenFailure text) a
failStrengthen1
        [ Builder
"refinement failure:"
        , Text -> Builder
TBL.fromText (RefineFailure -> Text
prettyRefineFailure RefineFailure
rf) ]
        -- ^ TODO rerefined: provide a TBL pretty function

-- | Strengthen a type by refining it with a functor predicate.
instance Refine1 p f => Strengthen (Refined1 p f a) where
    strengthen :: Weakened (Refined1 p f a)
-> Either StrengthenFailure' (Refined1 p f a)
strengthen = f a -> Either RefineFailure (Refined1 p f a)
forall {k1} {k2} (p :: k1) (f :: k2 -> Type) (a :: k2).
Refine1 p f =>
f a -> Either RefineFailure (Refined1 p f a)
refine1 (f a -> Either RefineFailure (Refined1 p f a))
-> (Either RefineFailure (Refined1 p f a)
    -> Either StrengthenFailure' (Refined1 p f a))
-> f a
-> Either StrengthenFailure' (Refined1 p f a)
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> \case
      Right Refined1 p f a
ra -> Refined1 p f a -> Either StrengthenFailure' (Refined1 p f a)
forall a b. b -> Either a b
Right Refined1 p f a
ra
      Left  RefineFailure
rf -> [Builder] -> Either StrengthenFailure' (Refined1 p f a)
forall text a. [text] -> Either (StrengthenFailure text) a
failStrengthen1
        [ Builder
"refinement failure:"
        , Text -> Builder
TBL.fromText (RefineFailure -> Text
prettyRefineFailure RefineFailure
rf) ]

-- | Strengthen a plain list into a non-empty list by asserting non-emptiness.
instance Strengthen (NonEmpty a) where
    strengthen :: Weakened (NonEmpty a) -> Either StrengthenFailure' (NonEmpty a)
strengthen = [a] -> Maybe (NonEmpty a)
forall a. [a] -> Maybe (NonEmpty a)
NonEmpty.nonEmpty ([a] -> Maybe (NonEmpty a))
-> (Maybe (NonEmpty a) -> Either StrengthenFailure' (NonEmpty a))
-> [a]
-> Either StrengthenFailure' (NonEmpty a)
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> \case
      Just NonEmpty a
neas -> NonEmpty a -> Either StrengthenFailure' (NonEmpty a)
forall a b. b -> Either a b
Right NonEmpty a
neas
      Maybe (NonEmpty a)
Nothing   -> [Builder] -> Either StrengthenFailure' (NonEmpty a)
forall text a. [text] -> Either (StrengthenFailure text) a
failStrengthen1 ([Builder] -> Either StrengthenFailure' (NonEmpty a))
-> [Builder] -> Either StrengthenFailure' (NonEmpty a)
forall a b. (a -> b) -> a -> b
$
        [ Builder
"type: [a] -> NonEmpty a"
        , Builder
"fail: empty list" ]

-- | Strengthen a plain list into a sized vector by asserting length.
instance (VG.Vector v a, KnownNat n) => Strengthen (VGS.Vector v n a) where
    -- as of text-linear-builder-0.1.3, we can use 'fromUnboundedDec' for the
    -- phantom vector size
    -- I don't believe you can actually ever construct a vector with size
    -- greater than @'maxBound' \@'Int'@. but still!
    strengthen :: Weakened (Vector v n a) -> Either StrengthenFailure' (Vector v n a)
strengthen Weakened (Vector v n a)
as =
        case [a] -> Maybe (Vector v n a)
forall (v :: Type -> Type) a (n :: Nat).
(Vector v a, KnownNat n) =>
[a] -> Maybe (Vector v n a)
VGS.fromList [a]
Weakened (Vector v n a)
as of
          Just Vector v n a
va -> Vector v n a -> Either StrengthenFailure' (Vector v n a)
forall a b. b -> Either a b
Right Vector v n a
va
          Maybe (Vector v n a)
Nothing -> [Builder] -> Either StrengthenFailure' (Vector v n a)
forall text a. [text] -> Either (StrengthenFailure text) a
failStrengthen1 ([Builder] -> Either StrengthenFailure' (Vector v n a))
-> [Builder] -> Either StrengthenFailure' (Vector v n a)
forall a b. (a -> b) -> a -> b
$
            [ Builder
"type: [a] -> Vector v "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Nat -> Builder
forall a. Integral a => a -> Builder
TBL.fromUnboundedDec Nat
nBuilder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
" a"
            , Builder
"fail: wrong length (got "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Int -> Builder
forall a. (Integral a, FiniteBits a) => a -> Builder
TBL.fromDec ([a] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [a]
Weakened (Vector v n a)
as)Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
")" ]
      where n :: Nat
n = forall (n :: Nat). KnownNat n => Nat
natVal'' @n

{- TODO controversial. seems logical, but also kinda annoying.
instance (Show a, Typeable a) => Strengthen (Maybe a) where
    strengthen = \case [a] -> pure $ Just a
                       []  -> pure Nothing
                       x   -> strengthenFailBase x "list wasn't [a] or []"
-}

-- Strengthen 'Natural's into Haskell's bounded unsigned numeric types.
instance Strengthen Word8  where strengthen :: Weakened Word8 -> Either StrengthenFailure' Word8
strengthen = Nat -> Either StrengthenFailure' Word8
Weakened Word8 -> Either StrengthenFailure' Word8
forall m n.
(Typeable n, Integral n, Typeable m, Integral m, Bounded m,
 FiniteBits m) =>
n -> Either StrengthenFailure' m
strengthenBounded
instance Strengthen Word16 where strengthen :: Weakened Word16 -> Either StrengthenFailure' Word16
strengthen = Nat -> Either StrengthenFailure' Word16
Weakened Word16 -> Either StrengthenFailure' Word16
forall m n.
(Typeable n, Integral n, Typeable m, Integral m, Bounded m,
 FiniteBits m) =>
n -> Either StrengthenFailure' m
strengthenBounded
instance Strengthen Word32 where strengthen :: Weakened Word32 -> Either StrengthenFailure' Word32
strengthen = Nat -> Either StrengthenFailure' Word32
Weakened Word32 -> Either StrengthenFailure' Word32
forall m n.
(Typeable n, Integral n, Typeable m, Integral m, Bounded m,
 FiniteBits m) =>
n -> Either StrengthenFailure' m
strengthenBounded
instance Strengthen Word64 where strengthen :: Weakened Word64 -> Either StrengthenFailure' Word64
strengthen = Nat -> Either StrengthenFailure' Word64
Weakened Word64 -> Either StrengthenFailure' Word64
forall m n.
(Typeable n, Integral n, Typeable m, Integral m, Bounded m,
 FiniteBits m) =>
n -> Either StrengthenFailure' m
strengthenBounded

-- Strengthen 'Integer's into Haskell's bounded signed numeric types.
instance Strengthen Int8   where strengthen :: Weakened Int8 -> Either StrengthenFailure' Int8
strengthen = Integer -> Either StrengthenFailure' Int8
Weakened Int8 -> Either StrengthenFailure' Int8
forall m n.
(Typeable n, Integral n, Typeable m, Integral m, Bounded m,
 FiniteBits m) =>
n -> Either StrengthenFailure' m
strengthenBounded
instance Strengthen Int16  where strengthen :: Weakened Int16 -> Either StrengthenFailure' Int16
strengthen = Integer -> Either StrengthenFailure' Int16
Weakened Int16 -> Either StrengthenFailure' Int16
forall m n.
(Typeable n, Integral n, Typeable m, Integral m, Bounded m,
 FiniteBits m) =>
n -> Either StrengthenFailure' m
strengthenBounded
instance Strengthen Int32  where strengthen :: Weakened Int32 -> Either StrengthenFailure' Int32
strengthen = Integer -> Either StrengthenFailure' Int32
Weakened Int32 -> Either StrengthenFailure' Int32
forall m n.
(Typeable n, Integral n, Typeable m, Integral m, Bounded m,
 FiniteBits m) =>
n -> Either StrengthenFailure' m
strengthenBounded
instance Strengthen Int64  where strengthen :: Weakened Int64 -> Either StrengthenFailure' Int64
strengthen = Integer -> Either StrengthenFailure' Int64
Weakened Int64 -> Either StrengthenFailure' Int64
forall m n.
(Typeable n, Integral n, Typeable m, Integral m, Bounded m,
 FiniteBits m) =>
n -> Either StrengthenFailure' m
strengthenBounded

-- | Strengthen one numeric type into another.
--
-- @n@ must be "wider" than @m@.
--
-- @'FiniteBits' m@ is for error printing.
strengthenBounded
    :: forall m n
    .  ( Typeable n, Integral n
       , Typeable m, Integral m, Bounded m, FiniteBits m
       ) => n -> Either StrengthenFailure' m
strengthenBounded :: forall m n.
(Typeable n, Integral n, Typeable m, Integral m, Bounded m,
 FiniteBits m) =>
n -> Either StrengthenFailure' m
strengthenBounded n
n
  | n
n n -> n -> Bool
forall a. Ord a => a -> a -> Bool
<= n
maxBn Bool -> Bool -> Bool
&& n
n n -> n -> Bool
forall a. Ord a => a -> a -> Bool
>= n
minBn = m -> Either StrengthenFailure' m
forall a b. b -> Either a b
Right (n -> m
forall a b. (Integral a, Num b) => a -> b
fromIntegral n
n)
  | Bool
otherwise = [Builder] -> Either StrengthenFailure' m
forall text a. [text] -> Either (StrengthenFailure text) a
failStrengthen1
        [ Builder
"numeric strengthen: "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>String -> Builder
forall a. IsString a => String -> a
fromString (TypeRep -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep
forall {k} (a :: k). Typeable a => TypeRep
typeRep' @n))
          Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
" -> "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>String -> Builder
forall a. IsString a => String -> a
fromString (TypeRep -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep
forall {k} (a :: k). Typeable a => TypeRep
typeRep' @m))
        , Builder
"bounds check does not hold: "
          Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>m -> Builder
forall a. (Integral a, FiniteBits a) => a -> Builder
TBL.fromDec m
minBmBuilder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
" <= "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>n -> Builder
forall a. Integral a => a -> Builder
TBL.fromUnboundedDec n
n
          Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
" <= "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>m -> Builder
forall a. (Integral a, FiniteBits a) => a -> Builder
TBL.fromDec m
maxBm
        ]
  where
    maxBn :: n
maxBn = forall a b. (Integral a, Num b) => a -> b
fromIntegral @m @n m
maxBm
    minBn :: n
minBn = forall a b. (Integral a, Num b) => a -> b
fromIntegral @m @n m
minBm
    maxBm :: m
maxBm = forall a. Bounded a => a
maxBound @m
    minBm :: m
minBm = forall a. Bounded a => a
minBound @m

--------------------------------------------------------------------------------

-- | Decomposer. Strengthen every element in a list.
instance Strengthen a => Strengthen [a] where
    strengthen :: Weakened [a] -> Either StrengthenFailure' [a]
strengthen = [Weakened a] -> Either StrengthenFailure' [a]
Weakened [a] -> Either StrengthenFailure' [a]
forall a.
Strengthen a =>
[Weakened a] -> Either StrengthenFailure' [a]
strengthenList

-- TODO using reverse, SLOW!! >:(
strengthenList :: Strengthen a => [Weakened a] -> Either StrengthenFailure' [a]
strengthenList :: forall a.
Strengthen a =>
[Weakened a] -> Either StrengthenFailure' [a]
strengthenList = Int
-> [a]
-> [Either StrengthenFailure' a]
-> Either StrengthenFailure' [a]
forall {a} {a}.
(Integral a, FiniteBits a) =>
a
-> [a]
-> [Either StrengthenFailure' a]
-> Either StrengthenFailure' [a]
goR (Int
0 :: Int) [] ([Either StrengthenFailure' a] -> Either StrengthenFailure' [a])
-> ([Weakened a] -> [Either StrengthenFailure' a])
-> [Weakened a]
-> Either StrengthenFailure' [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Weakened a -> Either StrengthenFailure' a)
-> [Weakened a] -> [Either StrengthenFailure' a]
forall a b. (a -> b) -> [a] -> [b]
map Weakened a -> Either StrengthenFailure' a
forall a. Strengthen a => Weakened a -> Either StrengthenFailure' a
strengthen
  where
    goR :: a
-> [a]
-> [Either StrengthenFailure' a]
-> Either StrengthenFailure' [a]
goR a
i [a]
as = \case
      Either StrengthenFailure' a
r:[Either StrengthenFailure' a]
rs ->
        case Either StrengthenFailure' a
r of
          Right a
a -> a
-> [a]
-> [Either StrengthenFailure' a]
-> Either StrengthenFailure' [a]
goR (a
ia -> a -> a
forall a. Num a => a -> a -> a
+a
1) (a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
as) [Either StrengthenFailure' a]
rs
          Left  StrengthenFailure'
e -> a
-> [(Builder, StrengthenFailure')]
-> [Either StrengthenFailure' a]
-> Either StrengthenFailure' [a]
forall {a} {b} {a}.
(Integral a, FiniteBits a) =>
a
-> [(Builder, StrengthenFailure')]
-> [Either StrengthenFailure' b]
-> Either StrengthenFailure' a
goL (a
ia -> a -> a
forall a. Num a => a -> a -> a
+a
1) [(a -> Builder
forall a. (Integral a, FiniteBits a) => a -> Builder
TBL.fromDec a
i, StrengthenFailure'
e)]    [Either StrengthenFailure' a]
rs
      []   -> [a] -> Either StrengthenFailure' [a]
forall a b. b -> Either a b
Right ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
as)
    goL :: a
-> [(Builder, StrengthenFailure')]
-> [Either StrengthenFailure' b]
-> Either StrengthenFailure' a
goL a
i [(Builder, StrengthenFailure')]
es = \case
      Either StrengthenFailure' b
r:[Either StrengthenFailure' b]
rs ->
        case Either StrengthenFailure' b
r of
          Right b
_ -> a
-> [(Builder, StrengthenFailure')]
-> [Either StrengthenFailure' b]
-> Either StrengthenFailure' a
goL (a
ia -> a -> a
forall a. Num a => a -> a -> a
+a
1) [(Builder, StrengthenFailure')]
es                      [Either StrengthenFailure' b]
rs
          Left  StrengthenFailure'
e -> a
-> [(Builder, StrengthenFailure')]
-> [Either StrengthenFailure' b]
-> Either StrengthenFailure' a
goL (a
ia -> a -> a
forall a. Num a => a -> a -> a
+a
1) ((a -> Builder
forall a. (Integral a, FiniteBits a) => a -> Builder
TBL.fromDec a
i, StrengthenFailure'
e)(Builder, StrengthenFailure')
-> [(Builder, StrengthenFailure')]
-> [(Builder, StrengthenFailure')]
forall a. a -> [a] -> [a]
:[(Builder, StrengthenFailure')]
es) [Either StrengthenFailure' b]
rs
      []   -> [Builder]
-> [(Builder, StrengthenFailure')] -> Either StrengthenFailure' a
forall text a.
[text]
-> [(text, StrengthenFailure text)]
-> Either (StrengthenFailure text) a
failStrengthen [Builder
"list had failures"] [(Builder, StrengthenFailure')]
es

-- | Decomposer. Strengthen both elements of a tuple.
instance (Strengthen l, Strengthen r) => Strengthen (l, r) where
    strengthen :: Weakened (l, r) -> Either StrengthenFailure' (l, r)
strengthen (Weakened l
l, Weakened r
r) =
        case Weakened l -> Either StrengthenFailure' l
forall a. Strengthen a => Weakened a -> Either StrengthenFailure' a
strengthen Weakened l
l of
          Right l
sl ->
            case Weakened r -> Either StrengthenFailure' r
forall a. Strengthen a => Weakened a -> Either StrengthenFailure' a
strengthen Weakened r
r of
              Right r
sr -> (l, r) -> Either StrengthenFailure' (l, r)
forall a b. b -> Either a b
Right (l
sl, r
sr)
              Left  StrengthenFailure'
er -> [Builder]
-> [(Builder, StrengthenFailure')]
-> Either StrengthenFailure' (l, r)
forall text a.
[text]
-> [(text, StrengthenFailure text)]
-> Either (StrengthenFailure text) a
failStrengthen [Builder
"2-tuple: right failed"]
                [(Builder
"R", StrengthenFailure'
er)]
          Left  StrengthenFailure'
el ->
            case forall a. Strengthen a => Weakened a -> Either StrengthenFailure' a
strengthen @r Weakened r
r of
              Right r
_  -> [Builder]
-> [(Builder, StrengthenFailure')]
-> Either StrengthenFailure' (l, r)
forall text a.
[text]
-> [(text, StrengthenFailure text)]
-> Either (StrengthenFailure text) a
failStrengthen [Builder
"2-tuple:  left failed"]
                [(Builder
"L", StrengthenFailure'
el)]
              Left  StrengthenFailure'
er -> [Builder]
-> [(Builder, StrengthenFailure')]
-> Either StrengthenFailure' (l, r)
forall text a.
[text]
-> [(text, StrengthenFailure text)]
-> Either (StrengthenFailure text) a
failStrengthen [Builder
"2-tuple:   l&r failed"]
                [(Builder
"R", StrengthenFailure'
er), (Builder
"L", StrengthenFailure'
el)]

-- | Decomposer. Strengthen either side of an 'Either'.
instance (Strengthen a, Strengthen b) => Strengthen (Either a b) where
    strengthen :: Weakened (Either a b) -> Either StrengthenFailure' (Either a b)
strengthen = \case Left  Weakened a
a -> a -> Either a b
forall a b. a -> Either a b
Left  (a -> Either a b)
-> Either StrengthenFailure' a
-> Either StrengthenFailure' (Either a b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Weakened a -> Either StrengthenFailure' a
forall a. Strengthen a => Weakened a -> Either StrengthenFailure' a
strengthen Weakened a
a
                       Right Weakened b
b -> b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b)
-> Either StrengthenFailure' b
-> Either StrengthenFailure' (Either a b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Weakened b -> Either StrengthenFailure' b
forall a. Strengthen a => Weakened a -> Either StrengthenFailure' a
strengthen Weakened b
b

--------------------------------------------------------------------------------

-- from flow
(.>) :: (a -> b) -> (b -> c) -> a -> c
a -> b
f .> :: forall a b c. (a -> b) -> (b -> c) -> a -> c
.> b -> c
g = b -> c
g (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f

typeRep' :: forall a. Typeable a => TypeRep
typeRep' :: forall {k} (a :: k). Typeable a => TypeRep
typeRep' = Proxy a -> TypeRep
forall {k} (proxy :: k -> Type) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall (t :: k). Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)

class WeakenN n a => StrengthenN (n :: Natural) a where
    strengthenN :: WeakenedN n a -> Either StrengthenFailure' a

instance {-# OVERLAPPING #-} StrengthenN 0 a where
    strengthenN :: WeakenedN 0 a -> Either StrengthenFailure' a
strengthenN = a -> Either StrengthenFailure' a
WeakenedN 0 a -> Either StrengthenFailure' a
forall a b. b -> Either a b
Right

instance (Strengthen a, StrengthenN (n-1) (Weakened a))
  => StrengthenN n a where
    strengthenN :: WeakenedN n a -> Either StrengthenFailure' a
strengthenN WeakenedN n a
a =
        case forall (n :: Nat) a.
StrengthenN n a =>
WeakenedN n a -> Either StrengthenFailure' a
strengthenN @(n-1) @(Weakened a) (forall (n :: Nat) a.
WeakenedN n a -> WeakenedN (n - 1) (Weakened a)
weakenedNLR1 @n @a WeakenedN n a
a) of
          Left  StrengthenFailure'
e  -> StrengthenFailure' -> Either StrengthenFailure' a
forall a b. a -> Either a b
Left StrengthenFailure'
e
          Right Weakened a
sa -> Weakened a -> Either StrengthenFailure' a
forall a. Strengthen a => Weakened a -> Either StrengthenFailure' a
strengthen Weakened a
sa

-- | Inductive 'WeakenedN' case.
--
-- @n@ must not be 0.
weakenedNLR1 :: forall n a. WeakenedN n a -> WeakenedN (n-1) (Weakened a)
weakenedNLR1 :: forall (n :: Nat) a.
WeakenedN n a -> WeakenedN (n - 1) (Weakened a)
weakenedNLR1 = WeakenedN n a -> WeakenedN (n - 1) (Weakened a)
forall a b. a -> b
unsafeCoerce