remove Tagged, add Coercibly

This appears to be what I want. Given a newtype, I can choose to remove
just the newtype layering, or do that and also weaken the inner type.
Furthermore, I can recover either option even if an instance already
exists, by using `Coercibly` directly. Very interesting! Now we can have
more agency over newtype wrappers in strongweak, which was previously a
bit problematic, /and/ it potentially solves an orphan instance issue in
binrep.

Author: raehik

package.yaml

@@ -66,7 +66,6 @@ dependencies:
 - rerefined ^>= 0.8.0
 - vector-sized >= 1.5.0 && < 1.7
 - vector >= 0.12.3.1 && < 0.14
-- tagged ^>= 0.8.8
 
 library:
   source-dirs: src

src/Strongweak/Strengthen.hs

@@ -21,7 +21,8 @@ module Strongweak.Strengthen
   ) where
 
 import Strongweak.Util.TypeNats ( natVal'' )
-import Strongweak.Weaken ( Weaken(Weakened, weaken) )
+import Strongweak.Weaken
+  ( Weaken(Weakened, weaken), Coercibly(..), Coercibly1(..), Strategy(..) )
 
 import GHC.TypeNats ( KnownNat )
 import Data.Word
@@ -41,7 +42,7 @@ import Data.Bits ( FiniteBits )
 
 import Data.Typeable ( Typeable, TypeRep, typeRep, Proxy(Proxy) )
 
-import Data.Tagged ( Tagged(..) )
+import Data.Coerce
 
 {- | Attempt to strengthen some @'Weakened' a@, asserting certain invariants.
 
@@ -247,7 +248,18 @@ f .> g = g . f
 typeRep' :: forall a. Typeable a => TypeRep
 typeRep' = typeRep (Proxy @a)
 
--- | SPECIAL: Strengthen through a 'Tagged'. That is, strengthen @a@ then tag it
---   with @x@.
-instance Strengthen a => Strengthen (Tagged x a) where
-    strengthen = fmap Tagged <$> strengthen
+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

src/Strongweak/Weaken.hs

@@ -10,6 +10,10 @@ module Strongweak.Weaken
   , Strength(..)
   , type SW
   , type SWDepth
+
+  , Coercibly(..)
+  , Coercibly1(..)
+  , Strategy(..)
   ) where
 
 import Rerefined
@@ -23,7 +27,8 @@ import Data.Functor.Const
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.List.NonEmpty ( NonEmpty )
 import GHC.TypeNats
-import Data.Tagged ( Tagged(..) )
+
+import Data.Coerce
 
 {- | Weaken some @a@, relaxing certain invariants.
 
@@ -89,15 +94,8 @@ instance VG.Vector v a => Weaken (VGS.Vector v n a) where
     type Weakened (VGS.Vector v n a) = [a]
     weaken = VGS.toList
 
--- | Strip wrapper.
-instance Weaken   (Identity a) where
-    type Weakened (Identity a) = a
-    weaken = runIdentity
-
--- | Strip wrapper.
-instance Weaken   (Const a b) where
-    type Weakened (Const a b) = a
-    weaken = getConst
+deriving via Coercibly1 Shallow Identity    a instance Weaken (Identity a)
+deriving via Coercibly  Shallow (Const a b) a instance Weaken (Const a b)
 
 {- TODO controversial. seems logical, but also kinda annoying.
 -- | Weaken 'Maybe' (0 or 1) into '[]' (0 to n).
@@ -151,13 +149,46 @@ instance (Weaken a, Weaken b) => Weaken (Either a b) where
     weaken = \case Left  a -> Left  $ weaken a
                    Right b -> Right $ weaken b
 
--- | SPECIAL: Weaken through a 'Tagged'. That is, strip the 'Tagged' and weaken
---   the inner @a@.
---
--- This appears to contribute a useful role: we want to plug some newtype into
--- the strongweak ecosystem, but it would result in orphan instances. With this,
--- we can go through 'Tagged', and the phantom type helps us handle
--- parameterized newtypes (like @newtype 'ByteOrdered' (end :: 'ByteOrder') a@).
-instance Weaken a => Weaken (Tagged x a) where
-    type Weakened (Tagged x a) = Weakened a
-    weaken = weaken . unTagged
+-- 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'
+
+-- | How to weaken a layer type.
+data Strategy
+  = Shallow -- ^ Remove the layer.
+  | Deep    -- ^ Remove the layer, and weaken the inner 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
+
+-- | 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

strongweak.cabal

@@ -56,7 +56,6 @@ library
   build-depends:
       base >=4.18 && <5
     , rerefined >=0.8.0 && <0.9
-    , tagged >=0.8.8 && <0.9
     , text >=2.0 && <2.2
     , text-builder-linear >=0.1.3 && <0.2
     , vector >=0.12.3.1 && <0.14
@@ -94,7 +93,6 @@ test-suite spec
     , quickcheck-instances >=0.3.26 && <0.4
     , rerefined >=0.8.0 && <0.9
     , strongweak
-    , tagged >=0.8.8 && <0.9
     , text >=2.0 && <2.2
     , text-builder-linear >=0.1.3 && <0.2
     , vector >=0.12.3.1 && <0.14