Add special And associativity helpers e.g. _ :: Refined (pl And pr) a -> Refined pr (Refined pl a)

[raehik]

Some background. I use refined all over binrep to define binary representation building blocks. One such building block is data NullPad (n :: Natural)/type NullPadded n = Refined (NullPad n), for null-padded data. If you want null-padded bytestrings though, you also need them to be NullTerminated. So I end up with Refined (NullPad n) (Refined NullTerminate a).

The two Refined layers make the rest of my tools harder to use. I could write a custom newtype to work around it. But that goes against refined's design philosophy. And it turns out I can use And to solve it. The instances look something like this:

instance Put (Refined pr (Refined pl a)) => Put (Refined (pl `And` pr) a) where
    put = put . reallyUnsafeRefine @_ @pr . reallyUnsafeRefine @_ @pl . unrefine

instance Get (Refined pr (Refined pl a)) => Get (Refined (pl `And` pr) a) where
    get = (reallyUnsafeRefine . unrefine @pl . unrefine @pr) <$> get

The refines are safe, since I'm just re-associating the predicates. It would be great to have some And helpers in the base library to hide these unsafe primitives!

[chessai]

This makes total sense. Frankly I thought this already existed

[raehik]

This is how I've defined them in rerefined:

-- | Take just the left predicate from an 'And'.
rerefineAndL :: Refined (And l r) a -> Refined l a
rerefineAndL = unsafeRerefine

-- | Take just the right predicate from an 'And'.
rerefineAndR :: Refined (And l r) a -> Refined r a
rerefineAndR = unsafeRerefine

-- | Eliminate an 'And' by applying the left predicate, then the right.
eliminateAndLR :: Refined (And l r) a -> Refined r (Refined l a)
eliminateAndLR = unsafeRefine . unsafeRefine . unrefine

-- | Eliminate an 'And' by applying the right predicate, then the left.
eliminateAndRL :: Refined (And l r) a -> Refined l (Refined r a)
eliminateAndRL = unsafeRefine . unsafeRefine . unrefine

-- | Introduce an 'And' given a double-'Refined'. Inner is left.
introduceAndLR :: Refined r (Refined l a) -> Refined (And l r) a
introduceAndLR = unsafeRefine . unrefine . unrefine

-- | Introduce an 'And' given a double-'Refined'. Inner is right.
introduceAndRL :: Refined l (Refined r a) -> Refined (And l r) a
introduceAndRL = unsafeRefine . unrefine . unrefine

Is that about appropriate to be put into refined? (One or two of these may already exist.)

[chessai]

This makes total sense to me. A PR would be great.