tweak code, move things around a bit

src/Strongweak/Strength.hs

@@ -1,9 +1,14 @@
+-- | Definitions using a type-level strength switch.
+
 module Strongweak.Strength where
 
 import Strongweak.Weaken ( type Weakened )
 import Data.Kind ( type Type )
 
--- | Strength enumeration: is it strong, or weak?
+import Strongweak.WeakenN
+import GHC.TypeNats ( type Natural )
+
+-- | Strength enumeration: it's either strong, or weak.
 --
 -- Primarily interesting at the type level (using DataKinds).
 data Strength = Strong | Weak
@@ -24,3 +29,6 @@ data A (s :: Strength) = A
 type family SW (s :: Strength) a :: Type where
     SW Strong a =          a
     SW Weak   a = Weakened a
+
+-- | Shortcut for a 'SW'-wrapped 'WeakenN'.
+type SWN (s :: Strength) (n :: Natural) a = SW s (WeakenN n a)

src/Strongweak/WeakenN.hs

@@ -1,17 +1,9 @@
-{-# LANGUAGE UndecidableInstances #-} -- type family 'Weakened' in constraints
-{-# LANGUAGE AllowAmbiguousTypes #-} -- ambiguous intermediate type classes
+module Strongweak.WeakenN ( WeakenN(..) ) where
 
-module Strongweak.WeakenN
-  ( WeakenN(..)
-  , type SWN
-  ) where
-
-import Strongweak.Weaken ( Weaken(weaken), type WeakenedN )
-import Strongweak.Strengthen
-import GHC.TypeNats ( type Natural, type (-) )
-import Unsafe.Coerce ( unsafeCoerce )
-
-import Strongweak.Strength ( type Strength, type SW )
+import Strongweak.WeakenN.Internal
+import Strongweak.Weaken ( Weaken(..), type WeakenedN )
+import Strongweak.Strengthen ( Strengthen(..) )
+import GHC.TypeNats ( type Natural )
 
 {- | When weakening (or strengthening), chain the operation @n@ times.
 
@@ -37,53 +29,9 @@ And so on. (This type is only much use from @n = 2@ onwards.)
 newtype WeakenN (n :: Natural) a = WeakenN { unWeakenN :: a }
     deriving stock Show
 
--- | Shortcut for a 'SW'-wrapped 'WeakenN'.
-type SWN (s :: Strength) (n :: Natural) a = SW s (WeakenN n a)
-
 instance WeakenWeakenN n a => Weaken (WeakenN n a) where
     type Weakened (WeakenN n a) = WeakenedN n a
     weaken = weakenWeakenN @n @a . unWeakenN
 
-class WeakenWeakenN (n :: Natural) a where
-    weakenWeakenN :: a -> WeakenedN n a
-
--- | Zero case: return the value as-is.
---
--- TODO The overlapping rules always confuse me. @OVERLAPPING@ is right, right?
-instance {-# OVERLAPPING #-} WeakenWeakenN 0 a where
-    weakenWeakenN = id
-
--- | Inductive case. @n /= 0@, else this explodes.
-instance (Weaken a, WeakenWeakenN (n-1) (Weakened a))
-  => WeakenWeakenN n a where
-    weakenWeakenN a =
-        case weakenWeakenN @(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 StrengthenWeakenN n a => Strengthen (WeakenN n a) where
     strengthen = fmap WeakenN . strengthenWeakenN @n @a
-
-class WeakenWeakenN n a => StrengthenWeakenN (n :: Natural) a where
-    strengthenWeakenN :: WeakenedN n a -> Either StrengthenFailure' a
-
-instance {-# OVERLAPPING #-} StrengthenWeakenN 0 a where
-    strengthenWeakenN = Right
-
-instance (Strengthen a, StrengthenWeakenN (n-1) (Weakened a))
-  => StrengthenWeakenN n a where
-    strengthenWeakenN a =
-        case strengthenWeakenN @(n-1) @(Weakened a) (weakenedNLR1 @n @a a) of
-          Left  e  -> Left e
-          Right sa -> strengthen sa

src/Strongweak/WeakenN/Internal.hs

@@ -0,0 +1,55 @@
+{-# 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 = id
+
+-- | Inductive case. @n /= 0@, else this explodes.
+instance (Weaken a, WeakenWeakenN (n-1) (Weakened a))
+  => WeakenWeakenN n a where
+    weakenWeakenN a =
+        case weakenWeakenN @(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
+
+class WeakenWeakenN n a => StrengthenWeakenN (n :: Natural) a where
+    strengthenWeakenN :: WeakenedN n a -> Either StrengthenFailure' a
+
+instance {-# OVERLAPPING #-} StrengthenWeakenN 0 a where
+    strengthenWeakenN = Right
+
+instance (Strengthen a, StrengthenWeakenN (n-1) (Weakened a))
+  => StrengthenWeakenN n a where
+    strengthenWeakenN a =
+        case strengthenWeakenN @(n-1) @(Weakened a) (weakenedNLR1 @n @a a) of
+          Left  e  -> Left e
+          Right sa -> strengthen sa
+
+-- | Inductive 'WeakenedN'case.
+--
+-- @n@ must not be 0.
+weakenedNLR1 :: forall n a. WeakenedN n a -> WeakenedN (n-1) (Weakened a)
+weakenedNLR1 = unsafeCoerce

strongweak.cabal

@@ -39,6 +39,7 @@ library
       Strongweak.Weaken
       Strongweak.Weaken.Generic
       Strongweak.WeakenN
+      Strongweak.WeakenN.Internal
   other-modules:
       Paths_strongweak
   hs-source-dirs: