start cleaning up

Author: raehik

src/Strongweak.hs

@@ -23,6 +23,7 @@ module Strongweak
 
 import Strongweak.Weaken
 import Strongweak.Strengthen
+import Strongweak.Strength
 
 {- $strongweak-instance-design
 

src/Strongweak/Chain.hs

@@ -1,13 +1,12 @@
 {-# LANGUAGE UndecidableInstances #-} -- type family 'Weakened' in constraints
-{-# LANGUAGE AllowAmbiguousTypes #-} -- TODO
+{-# LANGUAGE AllowAmbiguousTypes #-} -- ambiguous intermediate type classes
 
 module Strongweak.Chain where
 
-import Strongweak.Weaken
+import Strongweak.Weaken ( Weaken(weaken), type WeakenedN )
 import Strongweak.Strengthen
 import GHC.TypeNats
-
-import Unsafe.Coerce
+import Unsafe.Coerce ( unsafeCoerce )
 
 {- | When weakening (or strengthening), chain the operation @n@ times.
 

src/Strongweak/Example.hs

@@ -0,0 +1,26 @@
+module Strongweak.Strength where
+
+import Strongweak.Weaken ( type Weakened )
+import Data.Kind ( type Type )
+
+-- | Strength enumeration: is it strong, or weak?
+--
+-- Primarily interesting at the type level (using DataKinds).
+data Strength = Strong | Weak
+
+{- | Get either the strong or weak representation of a type, depending on the
+     type-level "switch" provided.
+
+This is intended to be used in data types that take a 'Strength' type. Define
+your type using strong fields wrapped in @SW s@. You then get the weak
+representation for free, using the same definition.
+
+@
+data A (s :: Strength) = A
+  { a1 :: SW s Word8
+  , a2 :: String }
+@
+-}
+type family SW (s :: Strength) a :: Type where
+    SW Strong a =          a
+    SW Weak   a = Weakened a

src/Strongweak/Strength.hs

@@ -20,8 +20,13 @@ module Strongweak.Strengthen
   , Strongweak.Weaken.Weakened
   ) where
 
+import Strongweak.Weaken ( Weaken(Weakened) )
+
+import Strongweak.Weaken ( Weaken(weaken) )
+
+import Strongweak.Weaken ( SWCoercibly(..) )
+
 import Strongweak.Util.TypeNats ( natVal'' )
-import Strongweak.Weaken ( Weaken(Weakened, weaken) )
 
 import GHC.TypeNats ( KnownNat )
 import Data.Word
@@ -101,6 +106,15 @@ failStrengthen t fs = Left $ StrengthenFailure t fs
 failStrengthen1 :: [text] -> Either (StrengthenFailure text) a
 failStrengthen1 t = failStrengthen 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 = Right . 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 = refine .> \case
@@ -236,6 +250,3 @@ f .> g = g . f
 
 typeRep' :: forall a. Typeable a => TypeRep
 typeRep' = typeRep (Proxy @a)
-
-instance Strengthen (Identity a) where
-    strengthen = Right . Identity

src/Strongweak/Strengthen.hs

@@ -7,11 +7,13 @@ import Rerefined.Refine
 import Data.Vector.Generic.Sized qualified as VGS -- Shazbot!
 import Data.Vector.Generic qualified as VG
 import Data.Vector.Generic.Sized.Internal qualified
-import Data.Functor.Identity
-import Data.Functor.Const
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.List.NonEmpty ( NonEmpty )
 
+import Strongweak.Weaken ( SWCoercibly(..) )
+import Data.Functor.Identity
+import Data.Functor.Const
+
 {- | Unsafely transform a @'Weakened' a@ to an @a@, without asserting invariants.
 
 Naturally, you must only even /consider/ using this if you have a guarantee that
@@ -34,6 +36,12 @@ class Weaken a => UnsafeStrengthen a where
     -- | Unsafely transform a @'Weakened' a@ to its associated strong type @a@.
     unsafeStrengthen :: Weakened a -> a
 
+instance UnsafeStrengthen (SWCoercibly a) where
+    unsafeStrengthen = SWCoercibly
+
+deriving via SWCoercibly a instance UnsafeStrengthen (Identity a)
+deriving via SWCoercibly a instance UnsafeStrengthen (Const a b)
+
 -- | Add a refinement to a type without checking the associated predicate.
 instance UnsafeStrengthen (Refined p a) where
     unsafeStrengthen = unsafeRefine

src/Strongweak/Strengthen/Unsafe.hs

@@ -2,16 +2,10 @@
 
 module Strongweak.Weaken
   (
-  -- * 'Weaken' class
-    Weaken(..)
+    Weaken(Weakened, weaken)
   , type WeakenedN
   , liftWeakF
-
-  -- * Strength switch helper
-  , Strength(..)
-  , type SW
-
-  , ErrZeroInvariantNewtype'
+  , SWCoercibly(..)
   ) where
 
 import Rerefined
@@ -26,10 +20,6 @@ import Data.List.NonEmpty qualified as NonEmpty
 import Data.List.NonEmpty ( NonEmpty )
 import GHC.TypeNats
 
-import GHC.TypeError
-import Strongweak.Util.TypeErrors
-import GHC.TypeLits ( type Symbol )
-
 {- | Weaken some @a@, relaxing certain invariants.
 
 See "Strongweak" for class design notes and laws.
@@ -41,38 +31,32 @@ class Weaken a where
     -- | Weaken some @a@ to its associated weak type @'Weakened' a@.
     weaken :: a -> Weakened a
 
--- | Strength enumeration: is it strong, or weak?
---
--- Primarily interesting at the type level (using DataKinds).
-data Strength = Strong | Weak
-
 -- | Lift a function on a weak type to the associated strong type by weakening
 --   first.
 liftWeakF :: Weaken a => (Weakened a -> b) -> a -> b
 liftWeakF f = f . weaken
 
-{- | Get either the strong or weak representation of a type, depending on the
-     type-level "switch" provided.
-
-This is intended to be used in data types that take a 'Strength' type. Define
-your type using strong fields wrapped in @SW s@. You then get the weak
-representation for free, using the same definition.
-
-@
-data A (s :: Strength) = A
-  { a1 :: SW s Word8
-  , a2 :: String }
-@
--}
-type family SW (s :: Strength) a :: Type where
-    SW Strong a =          a
-    SW Weak   a = Weakened a
-
 -- | The type of @a@ after weakening @n@ times.
 type family WeakenedN (n :: Natural) a :: Type where
     WeakenedN 0 a = a
     WeakenedN n a = Weakened (WeakenedN (n-1) a)
 
+-- | A "via type" newtype for defining strongweak instances for zero-invariant,
+--   coercible newtypes.
+--
+-- Use like so:
+--
+-- @
+-- deriving via 'SWCoercibly' a instance 'Weaken' ('Identity' a)
+-- @
+newtype SWCoercibly a = SWCoercibly { unSWCoercibly :: a }
+instance Weaken (SWCoercibly a) where
+    type Weakened (SWCoercibly a) = a
+    weaken = unSWCoercibly
+
+deriving via SWCoercibly a instance Weaken (Identity a)
+deriving via SWCoercibly a instance Weaken (Const a b)
+
 -- | Strip refined type refinement.
 instance Weaken   (Refined p a) where
     type Weakened (Refined p a) = a
@@ -144,37 +128,3 @@ instance (Weaken a, Weaken b) => Weaken (Either a b) where
     type Weakened (Either a b) = Either (Weakened a) (Weakened b)
     weaken = \case Left  a -> Left  $ weaken a
                    Right b -> Right $ weaken b
-
----
-
-newtype ErrZeroInvariantNewtype' (typeName :: Symbol) a
-  = ErrZeroInvariantNewtype' a
-instance Unsatisfiable (ErrZeroInvariantNewtype typeName)
-  => Weaken (ErrZeroInvariantNewtype' typeName a) where
-    type Weakened (ErrZeroInvariantNewtype' typeName a) =
-        TypeError (ErrZeroInvariantNewtype typeName)
-    weaken = unsatisfiable
-
---deriving via ErrZeroInvariantNewtype' "Identity" a
---  instance Weaken (Identity a)
-
-{- TODO 2024-10-16T04:21:22+0100
-aww this doesn't work haha. ok fine just gotta make some utils for filling out
-the context and Weakened associated type family for custom erroring instances
--}
-
-{-
-instance Unsatisfiable (ErrZeroInvariantNewtype "Identity")
-  => Weaken (Identity a) where
-    type Weakened (Identity a) = a
-    weaken = unsatisfiable
--}
-
--- TODO define custom errors using Unsatisfiable to point users to Coercibly
--- Unsatisfiable is base-4.19 -> GHC 9.8
---deriving via Coercibly1 Shallow Identity    a instance Weaken (Identity a)
---deriving via Coercibly  Shallow (Const a b) a instance Weaken (Const a b)
-
-instance Weaken (Identity a) where
-    type Weakened (Identity a) = a
-    weaken (Identity a) = a

src/Strongweak/Weaken.hs

@@ -32,8 +32,8 @@ library
       Strongweak
       Strongweak.Chain
       Strongweak.Coercibly
-      Strongweak.Example
       Strongweak.Generic
+      Strongweak.Strength
       Strongweak.Strengthen
       Strongweak.Strengthen.Generic
       Strongweak.Strengthen.Unsafe