{-# LANGUAGE UndecidableInstances #-} -- type family 'Weakened' in constraints
{-# LANGUAGE AllowAmbiguousTypes #-} -- ambiguous intermediate type classes

{- | 'Strongweak.WeakenN.WeakenN' internals.

Just in case. You shouldn't need these, but they might be fun to look at.

__Internal module. Exports may change without warning. Try not to use.__
-}

module Strongweak.WeakenN.Internal where

import Strongweak.Weaken ( Weaken(weaken), type WeakenedN )
import Strongweak.Strengthen
import GHC.TypeNats ( type Natural, type (-) )
import Unsafe.Coerce ( unsafeCoerce )

class WeakenWeakenN (n :: Natural) a where
    weakenWeakenN :: a -> WeakenedN n a

-- | Zero case: return the value as-is.
instance {-# OVERLAPPING #-} WeakenWeakenN 0 a where
    weakenWeakenN :: a -> WeakenedN 0 a
weakenWeakenN = a -> a
a -> WeakenedN 0 a
forall a. a -> a
id

-- | Inductive case. @n /= 0@, else this explodes.
instance (Weaken a, WeakenWeakenN (n-1) (Weakened a))
  => WeakenWeakenN n a where
    weakenWeakenN :: a -> WeakenedN n a
weakenWeakenN a
a =
        case forall (n :: Natural) a. WeakenWeakenN n a => a -> WeakenedN n a
weakenWeakenN @(n-1) @(Weakened a) (a -> Weakened a
forall a. Weaken a => a -> Weakened a
weaken a
a) of
          WeakenedN (n - 1) (Weakened a)
x -> forall (n :: Natural) a.
WeakenedN (n - 1) (Weakened a) -> WeakenedN n a
weakenedNRL1 @n @a WeakenedN (n - 1) (Weakened a)
x

-- | Inverted inductive 'WeakenedN'case.
--
-- @n@ must not be 0.
weakenedNRL1 :: forall n a. WeakenedN (n-1) (Weakened a) -> WeakenedN n a
weakenedNRL1 :: forall (n :: Natural) a.
WeakenedN (n - 1) (Weakened a) -> WeakenedN n a
weakenedNRL1 = WeakenedN (n - 1) (Weakened a) -> WeakenedN n a
forall a b. a -> b
unsafeCoerce

class WeakenWeakenN n a => StrengthenWeakenN (n :: Natural) a where
    strengthenWeakenN :: WeakenedN n a -> Either StrengthenFailure' a

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

instance (Strengthen a, StrengthenWeakenN (n-1) (Weakened a))
  => StrengthenWeakenN n a where
    strengthenWeakenN :: WeakenedN n a -> Either StrengthenFailure' a
strengthenWeakenN WeakenedN n a
a =
        case forall (n :: Natural) a.
StrengthenWeakenN n a =>
WeakenedN n a -> Either StrengthenFailure' a
strengthenWeakenN @(n-1) @(Weakened a) (forall (n :: Natural) 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 :: Natural) a.
WeakenedN n a -> WeakenedN (n - 1) (Weakened a)
weakenedNLR1 = WeakenedN n a -> WeakenedN (n - 1) (Weakened a)
forall a b. a -> b
unsafeCoerce