begin to rip out TypeReps; cleanup

TODO.md

@@ -22,3 +22,12 @@ start lol.
 The `Show`ing feels a little weird too, but I think it's just that we get away
 with it thanks to having lots of concrete instances. Non-concrete instances
 would drop it.
+
+Hmm. Not too sure how `Refined` instances will look. How do we get a `Symbol`
+from the `a` in `Refined p a`? We can say "it's some type refined with this
+predicate", but we apparently can't tell you the type.
+
+Hold on, we went with type-level show for predicates because we were doing lots
+of combination. We do no such thing here. Why don't we just write in the
+`TypeRep`s ourselves? Easy for concrete, fine for `Refined`. Apparently not a
+problem for decomposing instances either.

src/Strongweak/Generic/Strengthen.hs

@@ -18,9 +18,8 @@ import Data.Either.Validation
 import GHC.Generics
 import Data.Kind
 import GHC.TypeNats
-import GHC.Exts ( proxy#, Proxy# )
-
-import Control.Applicative ( liftA2 ) -- required for older GHCs
+import Control.Applicative qualified as A -- liftA2 export workaround
+import Strongweak.Util.TypeNats ( natVal'' )
 
 -- | Strengthen a value generically.
 --
@@ -72,7 +71,7 @@ instance
   , GStrengthenS wcd scd wcc scc (si + ProdArity wl) wr sr
   ) => GStrengthenS wcd scd wcc scc si (wl :*: wr) (sl :*: sr) where
     gstrengthenS (l :*: r) =
-        liftA2 (:*:)
+        A.liftA2 (:*:)
                (gstrengthenS @wcd @scd @wcc @scc @si                  l)
                (gstrengthenS @wcd @scd @wcc @scc @(si + ProdArity wl) r)
 
@@ -139,9 +138,3 @@ selName' = selName @s undefined
 type family ProdArity (f :: Type -> Type) :: Natural where
     ProdArity (S1 c f)  = 1
     ProdArity (l :*: r) = ProdArity l + ProdArity r
-
---------------------------------------------------------------------------------
-
-natVal'' :: forall n. KnownNat n => Natural
-natVal'' = natVal' (proxy# :: Proxy# n)
-{-# INLINE natVal'' #-}

src/Strongweak/Strengthen.hs

@@ -28,6 +28,7 @@ module Strongweak.Strengthen
 
 import Strongweak.Util.Typeable ( typeRep' )
 import Strongweak.Util.Text ( tshow )
+import Strongweak.Util.TypeNats ( natVal'' )
 import Strongweak.Weaken ( Weaken(..) )
 import Data.Either.Validation
 import Data.Typeable ( Typeable, TypeRep )
@@ -45,7 +46,7 @@ import Rerefined
 import Data.Vector.Generic.Sized qualified as VGS -- Shazbot!
 import Data.Vector.Generic qualified as VG
 import Data.Foldable qualified as Foldable
-import Control.Applicative ( liftA2 ) -- required for older GHCs
+import Control.Applicative qualified as A -- liftA2 export workaround
 import Data.Functor.Identity
 import Data.Functor.Const
 import Acc.NeAcc
@@ -188,38 +189,43 @@ maybeFailShow detail = \case
     Just a  -> Success a
     Nothing -> failShowNoVal @(Weak a) detail
 
--- | Assert a predicate to refine a type.
-instance (Refine p a, Typeable a, Typeable p, Typeable k)
-  => Strengthen (Refined (p :: k) a) where
+maybeFail :: [Text] -> Maybe a -> Result a
+maybeFail detail = \case
+    Just a  -> Success a
+    Nothing -> fail1 $ FailOther detail
+
+-- | Strengthen a type by refining it with a predicate.
+instance Refine p a => Strengthen (Refined p a) where
     strengthen = refine .> \case
-      Left  rf -> failShowNoVal @a
-        [ "refinement: "<>tshow (typeRep' @p)
-        , "failed with..."
+      Left  rf -> fail1 $ FailOther
+        [ "refinement failure:"
         , prettyRefineFailure rf
         ]
       Right ra -> Success ra
 
--- | Assert a functor predicate to refine a type.
-instance (Refine1 p f, Typeable f, Typeable (a :: ak), Typeable ak, Typeable p, Typeable k)
-  => Strengthen (Refined1 (p :: k) f a) where
+-- | Strengthen a type by refining it with a functor predicate.
+instance Refine1 p f => Strengthen (Refined1 p f a) where
     strengthen = refine1 .> \case
-      Left  rf -> failShowNoVal @(f a)
-        [ "refinement: "<>tshow (typeRep' @p)
-        , "failed with..."
-        , prettyRefineFailure rf
-        ]
+      Left  rf -> fail1 $ FailOther
+        [ "refinement failure:"
+        , prettyRefineFailure rf ]
       Right ra -> Success ra
 
 -- | Strengthen a plain list into a non-empty list by asserting non-emptiness.
-instance Typeable a => Strengthen (NonEmpty a) where
-    strengthen = NonEmpty.nonEmpty .> maybeFailShow ["empty list"]
+instance Strengthen (NonEmpty a) where
+    strengthen = NonEmpty.nonEmpty .> maybeFail
+        [ "type: [a] -> NonEmpty a"
+        , "fail: empty list" ]
 
 -- | Strengthen a plain list into a sized vector by asserting length.
-instance
-  ( VG.Vector v a, KnownNat n
-  , Typeable v, Typeable a
-  ) => Strengthen (VGS.Vector v n a) where
-      strengthen = VGS.fromList .> maybeFailShow ["incorrect length"]
+instance (VG.Vector v a, KnownNat n) => Strengthen (VGS.Vector v n a) where
+    strengthen as =
+        case VGS.fromList as of
+          Just va -> Success va
+          Nothing -> fail1 $ FailOther
+            [ "type: [a] -> Vector v "<>tshow n<>" a"
+            , "fail: wrong length (got "<>tshow (length as)<>")" ]
+      where n = natVal'' @n
 
 -- | Add wrapper.
 instance Strengthen (Identity a) where
@@ -256,6 +262,7 @@ strengthenBounded
     .  ( Typeable n, Integral n, Show n
        , Typeable m, Integral m, Show m, Bounded m
        ) => n -> Result m
+-- TODO this is the last usage of FailShow remaining
 strengthenBounded n
   | n <= maxB && n >= minB = Success (fromIntegral n)
   | otherwise = failShow n
@@ -274,7 +281,7 @@ instance Strengthen a => Strengthen [a] where
 
 -- | Decomposer. Strengthen both elements of a tuple.
 instance (Strengthen a, Strengthen b) => Strengthen (a, b) where
-    strengthen (a, b) = liftA2 (,) (strengthen a) (strengthen b)
+    strengthen (a, b) = A.liftA2 (,) (strengthen a) (strengthen b)
 
 -- | Decomposer. Strengthen either side of an 'Either'.
 instance (Strengthen a, Strengthen b) => Strengthen (Either a b) where

src/Strongweak/Util/TypeNats.hs

@@ -0,0 +1,10 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module Strongweak.Util.TypeNats where
+
+import GHC.TypeNats
+import GHC.Exts ( proxy# )
+
+natVal'' :: forall n. KnownNat n => Natural
+natVal'' = natVal' (proxy# @n)
+{-# INLINE natVal'' #-}

strongweak.cabal

@@ -37,6 +37,7 @@ library
       Strongweak.Strengthen.Unsafe
       Strongweak.Util.Text
       Strongweak.Util.Typeable
+      Strongweak.Util.TypeNats
       Strongweak.Weaken
   other-modules:
       Paths_strongweak