+SWChain for chaining strongweak ops; many tweaks

The implementation of SWChain is really cool.
We have to do some `unsafeCoerce`ing and use intermediate type classes,
but we get fully parametric chaining. I'm very proud of it.

Author: raehik

TODO.md

@@ -1,5 +1,4 @@
 # strongweak to-dos
-* OOPS overlap between `Weak :: Weaken a => Type` and `Weak :: Strength`
 * split into base definitions and orphan instances?
 * deleted generic failure tests because clumsy. kinda sad but idk :(
 

src/Strongweak.hs

@@ -26,7 +26,7 @@ import Strongweak.Strengthen
 
 {- $strongweak-instance-design
 
-A given strong type @a@ has exactly one associated weak type @'Weak' a@.
+A given strong type @a@ has exactly one associated weak type @'Weakened' a@.
 Multiple strong types may weaken to the same weak type.
 
 The following laws must hold:
@@ -43,6 +43,12 @@ with the overall design. Here is some relevant guidance.
   * Most (all?) instances should handle (relax or assert) a single invariant.
   * Most instances should not have a recursive context.
 
+If you want to handle multiple invariants, chain the weakens/strengthens.
+You may do this by nesting 'SW' uses, but you will then have to write your own
+instances, as the generics cannot handle such chaining. Alternatively, you may
+use 'SWChain'. This will add another newtype layer to the strong representation,
+but the generics are happy with it.
+
 Some types may not have any invariants which may be usefully relaxed e.g.
 @'Either' a b@. For these, you may write a recursive instance that
 weakens/strengthens "through" the type e.g. @('Weak' a, 'Weak' b) => Weak
@@ -57,4 +63,17 @@ a @'Weak' a = a, weaken = id@ overlapping instance, which I do not want. On the
 other hand, @[a]@ /does/ weaken to @['Weak' a]@, because there are no invariants
 present to remove, so decomposing is all the user could hope to do.
 
+Another problem is coercible newtypes such as @Tagged@ from the @tagged@
+package. These have no invariants for us to weaken, so one's knee-jerk reaction
+might be to weaken the inner type. But what if the user doesn't want to weaken
+that inner type? They might be happy with using 'Data.Word.Word' instead of
+'Numeric.Natural.Natural', for example.
+
+strongweak provides a special type 'Coercibly' which permits precisely defining
+how to weaken a newtype/pair of coercible types. For this reason, zero-invariant
+coercible newtypes are excluded from the strongweak ecosystem (e.g.
+'Data.Functor.Identity.Identity', 'Data.Functor.Const.Const', @Tagged@).
+
+If your newtype puts the wrapped type as the final type variable, use
+'Coercibly1' for a considerably simpler invocation.
 -}

src/Strongweak/Chain.hs

@@ -0,0 +1,113 @@
+{-# LANGUAGE UndecidableInstances #-} -- type family 'Weakened' in constraints
+{-# LANGUAGE AllowAmbiguousTypes #-} -- TODO
+
+module Strongweak.Chain where
+
+import Strongweak.Weaken
+import Strongweak.Strengthen
+import GHC.TypeNats
+
+import Unsafe.Coerce
+
+{- | 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.
+
+'SWChain' 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 (SWChain 0 a) = a
+Weakened (SWChain 1 a) = Weakened a
+Weakened (SWChain 2 a) = Weakened (Weakened a)
+Weakened (SWChain n a) = WeakenedN n a
+@
+
+And so on. (This type is only much use from @n = 2@ onwards.)
+-}
+newtype SWChain (n :: Natural) a = SWChain { unSWChain :: a }
+    deriving stock Show
+
+instance WeakenN n a => Weaken (SWChain n a) where
+    type Weakened (SWChain n a) = WeakenedN n a
+    weaken = weakenN @n @a . unSWChain
+
+class WeakenN (n :: Natural) a where
+    weakenN :: a -> WeakenedN n a
+
+-- | Zero case: return the value as-is.
+--
+-- TODO The overlapping rules always confuse me. @OVERLAPPING@ is right, right?
+instance {-# OVERLAPPING #-} WeakenN 0 a where
+    weakenN = id
+
+-- | Inductive case. @n /= 0@, else this explodes.
+instance (Weaken a, WeakenN (n-1) (Weakened a)) => WeakenN n a where
+    weakenN a =
+        case weakenN @(n-1) @(Weakened a) (weaken a) of
+          x -> weakenedNRL1 @n @a x
+
+-- | Inverted inductive 'WeakenedN'case.
+--
+-- @n@ must not be 0.
+weakenedNRL1 :: forall n a. WeakenedN (n-1) (Weakened a) -> WeakenedN n a
+weakenedNRL1 = unsafeCoerce
+
+-- | Inductive 'WeakenedN'case.
+--
+-- @n@ must not be 0.
+weakenedNLR1 :: forall n a. WeakenedN n a -> WeakenedN (n-1) (Weakened a)
+weakenedNLR1 = unsafeCoerce
+
+instance StrengthenN n a => Strengthen (SWChain n a) where
+    strengthen = fmap SWChain . strengthenN @n @a
+
+class WeakenN n a => StrengthenN (n :: Natural) a where
+    strengthenN :: WeakenedN n a -> Either StrengthenFailure' a
+
+instance {-# OVERLAPPING #-} StrengthenN 0 a where
+    strengthenN = Right
+
+instance (Strengthen a, StrengthenN (n-1) (Weakened a))
+  => StrengthenN n a where
+    strengthenN a =
+        case strengthenN @(n-1) @(Weakened a) (weakenedNLR1 @n @a a) of
+          Left  e  -> Left e
+          Right sa -> strengthen sa
+
+{-
+
+instance Weaken (Chain 0 a) where
+    type Weakened (Chain 0 a) = a
+    weaken = unChain
+instance Strengthen (Chain 0 a) where
+    strengthen = Right . Chain
+
+instance Weaken a => Weaken (Chain 1 a) where
+    type Weakened (Chain 1 a) = Weakened a
+    weaken = weaken . unChain
+instance Strengthen a => Strengthen (Chain 1 a) where
+    strengthen = fmap Chain . strengthen
+
+instance (Weaken a, Weaken (Weakened a)) => Weaken (Chain 2 a) where
+    type Weakened (Chain 2 a) = Weakened (Weakened a)
+    weaken = weaken . weaken . unChain
+instance (Strengthen a, Strengthen (Weakened a)) => Strengthen (Chain 2 a) where
+    strengthen a = -- TODO how to pointfree this lol? pointfree fmap confuses me
+        case strengthen a of
+          Left  e  -> Left e
+          Right sa -> fmap Chain (strengthen sa)
+-}
+
+{-
+newtype Twice a = Twice { unTwice :: a }
+    deriving stock Show
+instance (Weaken a, Weaken (Weakened a)) => Weaken (Twice a) where
+    type Weakened (Twice a) = Weakened (Weakened a)
+    weaken = weaken . weaken . unTwice
+-}

src/Strongweak/Coercibly.hs

@@ -0,0 +1,70 @@
+-- TODO what to name this? "coerce" has to be in it (that's the main thing).
+-- also trivial? zero-invariant? what about the strategy?
+
+-- TODO no longer really need thanks to SWChain. but maybe keep it around idk
+
+module Strongweak.Coercibly where
+
+import Strongweak.Weaken
+import Strongweak.Strengthen
+import Data.Coerce
+import Data.Kind ( type Type )
+
+{- | A @from@ that can be safely coerced between @to@.
+
+You can use this to decide precisely how to weaken a newtype: whether to only
+strip the newtype via 'Shallow', or to strip the newtype and weaken the inner
+type via 'Deep'.
+-}
+newtype Coercibly (stg :: Strategy) (from :: Type) to
+  = Coercibly { unCoercibly :: from }
+    deriving stock Show
+
+-- | How to weaken a layer type.
+data Strategy
+  = Shallow -- ^ Remove the layer.
+  | Deep    -- ^ Remove the layer, and weaken the inner type.
+
+-- note that without the Coercible instance, we get a confusing "couldn't match
+-- representation of type 'from' with that of 'to'" error message. this might
+-- happen in user code that tries to be parametric with 'Coercibly'
+
+-- | Remove the coercible @from@ layer.
+instance Coercible from to => Weaken (Coercibly Shallow from to) where
+    type Weakened (Coercibly Shallow from to) = to
+    weaken = coerce . unCoercibly
+
+-- | Remove the coercible @from@ layer and weaken the result.
+instance (Coercible from to, Weaken to) => Weaken (Coercibly Deep from to) where
+    type Weakened (Coercibly Deep from to) = Weakened to
+    weaken = weaken . coerce @from @to . unCoercibly
+
+-- | An @f a@ that can be safely coerced between @a@.
+newtype Coercibly1 (stg :: Strategy) f (a :: Type)
+  = Coercibly1 { unCoercibly1 :: f a }
+    deriving stock Show
+
+-- | Remove the coercible @f a@ layer.
+instance Coercible (f a) a => Weaken (Coercibly1 Shallow f a) where
+    type Weakened (Coercibly1 Shallow f a) = a
+    weaken = coerce . unCoercibly1
+
+-- | Remove the coercible @f a@ layer and weaken the result.
+instance (Coercible (f a) a, Weaken a) => Weaken (Coercibly1 Deep f a) where
+    type Weakened (Coercibly1 Deep f a) = Weakened a
+    weaken = weaken . coerce @(f a) @a . unCoercibly1
+
+
+instance Coercible from to => Strengthen (Coercibly Shallow from to) where
+    strengthen = Right . Coercibly . coerce @to @from
+
+instance (Coercible from to, Strengthen to)
+  => Strengthen (Coercibly Deep from to) where
+    strengthen = fmap (Coercibly . coerce @to @from) <$> strengthen
+
+instance Coercible (f a) a => Strengthen (Coercibly1 Shallow f a) where
+    strengthen = Right . Coercibly1 . coerce @a @(f a)
+
+instance (Coercible (f a) a, Strengthen a)
+  => Strengthen (Coercibly1 Deep f a) where
+    strengthen = fmap (Coercibly1 . coerce @a @(f a)) <$> strengthen

src/Strongweak/Example.hs

@@ -0,0 +1,16 @@
+module Strongweak.Example where
+import Strongweak
+import Strongweak.Generic
+import GHC.Generics ( Generic )
+import Data.List.NonEmpty as NE
+import Data.Word
+
+data A (s :: Strength) = A
+  { a1 :: SW s (NE.NonEmpty (SW s Word8))
+  } deriving stock Generic
+deriving instance Show (A Weak)
+deriving instance Show (A Strong)
+
+instance Weaken (A Strong) where
+    type Weakened (A Strong) = A Weak
+    weaken = undefined -- weakenGeneric

src/Strongweak/Generic.hs

@@ -30,11 +30,9 @@ between any /compatible/ pair of types. Compatibility is defined as follows:
 
   * Both types' generic representation (the SOP tree structure) match exactly.
   * For each leaf pair of types, either the types are identical, or the
-  appropriate instance exists to transform from source to target.
+    appropriate instance exists to transform from source to target.
 
-If they aren't compatible, the derivation will fail with a type error. I'm
-fairly certain that if it succeeds, your instance is guaranteed correct
-(assuming the instances it uses internally are all OK!).
+If they aren't compatible, the derivation will fail with a type error.
 
 I don't think GHC strongly guarantees the SOP property, so if you receive
 surprising derivation errors, the types might have differing generic
@@ -46,6 +44,11 @@ Also, generic strengthening requires that all metadata is present for both
 types: for the datatype, constructors and selectors. GHC will always add this
 metadata for you, but manually-derived Generic instances (which are usually a
 bad idea) do not require it.
+
+Note that the generics only handle one "layer" at a time. If you have a data
+type with nested 'Strongweak.Strengthen.SW' uses, these generics will fail with
+a type error. Write the instance manually instead. (I can't think of an easy way
+to handle this, but TODO all the same.)
 -}
 
 {- | @DerivingVia@ wrapper for strongweak instances.

src/Strongweak/Strengthen.hs

@@ -21,8 +21,7 @@ module Strongweak.Strengthen
   ) where
 
 import Strongweak.Util.TypeNats ( natVal'' )
-import Strongweak.Weaken
-  ( Weaken(Weakened, weaken), Coercibly(..), Coercibly1(..), Strategy(..) )
+import Strongweak.Weaken ( Weaken(Weakened, weaken) )
 
 import GHC.TypeNats ( KnownNat )
 import Data.Word
@@ -42,8 +41,6 @@ import Data.Bits ( FiniteBits )
 
 import Data.Typeable ( Typeable, TypeRep, typeRep, Proxy(Proxy) )
 
-import Data.Coerce
-
 {- | Attempt to strengthen some @'Weakened' a@, asserting certain invariants.
 
 We take 'Weaken' as a superclass in order to maintain strong/weak type pair
@@ -143,14 +140,6 @@ instance (VG.Vector v a, KnownNat n) => Strengthen (VGS.Vector v n a) where
             , "fail: wrong length (got "<>TBL.fromDec (length as)<>")" ]
       where n = natVal'' @n
 
--- | Add wrapper.
-instance Strengthen (Identity a) where
-    strengthen = Right . Identity
-
--- | Add wrapper.
-instance Strengthen (Const a b) where
-    strengthen = Right . Const
-
 {- TODO controversial. seems logical, but also kinda annoying.
 instance (Show a, Typeable a) => Strengthen (Maybe a) where
     strengthen = \case [a] -> pure $ Just a
@@ -248,18 +237,5 @@ f .> g = g . f
 typeRep' :: forall a. Typeable a => TypeRep
 typeRep' = typeRep (Proxy @a)
 
-instance Coercible from to => Strengthen (Coercibly Shallow from to) where
-    strengthen = Right . Coercibly . coerce @to @from
-
--- TODO wrap errors here?
-instance (Coercible from to, Strengthen to)
-  => Strengthen (Coercibly Deep from to) where
-    strengthen = fmap (Coercibly . coerce @to @from) <$> strengthen
-
-instance Coercible (f a) a => Strengthen (Coercibly1 Shallow f a) where
-    strengthen = Right . Coercibly1 . coerce @a @(f a)
-
--- TODO wrap errors here?
-instance (Coercible (f a) a, Strengthen a)
-  => Strengthen (Coercibly1 Deep f a) where
-    strengthen = fmap (Coercibly1 . coerce @a @(f a)) <$> strengthen
+instance Strengthen (Identity a) where
+    strengthen = Right . Identity

src/Strongweak/Strengthen/Unsafe.hs

@@ -47,14 +47,6 @@ instance VG.Vector v a => UnsafeStrengthen (VGS.Vector v n a) where
     unsafeStrengthen =
         Data.Vector.Generic.Sized.Internal.Vector . VG.fromList
 
--- | Add wrapper.
-instance UnsafeStrengthen (Identity a) where
-    unsafeStrengthen = Identity
-
--- | Add wrapper.
-instance UnsafeStrengthen (Const a b) where
-    unsafeStrengthen = Const
-
 {- TODO controversial. seems logical, but also kinda annoying.
 -- | Unsafely grab either 0 or 1 elements from a list.
 instance UnsafeStrengthen (Maybe a) where

src/Strongweak/Util/TypeErrors.hs

@@ -0,0 +1,9 @@
+module Strongweak.Util.TypeErrors where
+
+import GHC.TypeError
+
+type ErrZeroInvariantNewtype a =
+       Text a :<>: Text " is a zero-invariant, coercible newtype"
+  :$$: Text "These may not be used with strongweak type classes directly"
+  :$$: Text "  due to ambiguity with their handling"
+  :$$: Text "Wrap it using Strongweak.Coercibly"