-- | 'weaken' over generic representations.

module Strongweak.Generic.Weaken where

import Strongweak.Weaken

import GHC.Generics

-- | Weaken a value generically.
--
-- The weak and strong types must be /compatible/. See 'Strongweak.Generic' for
-- the definition of compatibility in this context.
weakenGeneric :: (Generic s, Generic w, GWeaken (Rep s) (Rep w)) => s -> w
weakenGeneric :: forall s w.
(Generic s, Generic w, GWeaken (Rep s) (Rep w)) =>
s -> w
weakenGeneric = forall a x. Generic a => Rep a x -> a
to forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (s :: k -> Type) (w :: k -> Type) (p :: k).
GWeaken s w =>
s p -> w p
gweaken forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a x. Generic a => a -> Rep a x
from

class GWeaken s w where
    gweaken :: s p -> w p

-- | Strip all meta.
instance GWeaken s w => GWeaken (M1 is ms s) (M1 iw mw w) where
    gweaken :: forall (p :: k). M1 is ms s p -> M1 iw mw w p
gweaken = forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (s :: k -> Type) (w :: k -> Type) (p :: k).
GWeaken s w =>
s p -> w p
gweaken forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1

-- | Nothing to do for empty datatypes.
instance GWeaken V1 V1 where
    gweaken :: forall (p :: k). V1 p -> V1 p
gweaken = forall a. a -> a
id

-- | Nothing to do for empty constructors.
instance GWeaken U1 U1 where
    gweaken :: forall (p :: k). U1 p -> U1 p
gweaken = forall a. a -> a
id

-- | Special case: if source and target types are equal, copy the value through.
instance GWeaken (Rec0 s) (Rec0 s) where
    gweaken :: forall (p :: k). Rec0 s p -> Rec0 s p
gweaken = forall a. a -> a
id

-- | Weaken a field using the existing 'Weaken' instance.
instance {-# OVERLAPS #-} (Weaken s, Weak s ~ w) => GWeaken (Rec0 s) (Rec0 w) where
    gweaken :: forall (p :: k). Rec0 s p -> Rec0 w p
gweaken = forall k i c (p :: k). c -> K1 i c p
K1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Weaken a => a -> Weak a
weaken forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i c (p :: k). K1 i c p -> c
unK1

-- | Weaken product types by weakening left and right.
instance (GWeaken ls lw, GWeaken rs rw) => GWeaken (ls :*: rs) (lw :*: rw) where
    gweaken :: forall (p :: k). (:*:) ls rs p -> (:*:) lw rw p
gweaken (ls p
l :*: rs p
r) = forall {k} (s :: k -> Type) (w :: k -> Type) (p :: k).
GWeaken s w =>
s p -> w p
gweaken ls p
l forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall {k} (s :: k -> Type) (w :: k -> Type) (p :: k).
GWeaken s w =>
s p -> w p
gweaken rs p
r

-- | Weaken sum types by casing and weakening left or right.
instance (GWeaken ls lw, GWeaken rs rw) => GWeaken (ls :+: rs) (lw :+: rw) where
    gweaken :: forall (p :: k). (:+:) ls rs p -> (:+:) lw rw p
gweaken = \case L1 ls p
l -> forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k -> Type) (w :: k -> Type) (p :: k).
GWeaken s w =>
s p -> w p
gweaken ls p
l
                    R1 rs p
r -> forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k -> Type) (w :: k -> Type) (p :: k).
GWeaken s w =>
s p -> w p
gweaken rs p
r