rerefined 0.2.0 → 0.3.0

raw patch · 29 files changed

+640/−331 lines, 29 filesdep +textdep +text-builder-lineardep +type-level-showdep −typeablydep ~basedep ~template-haskellPVP ok

version bump matches the API change (PVP)

Dependencies added: text, text-builder-linear, type-level-show

Dependencies removed: typeably

Dependency ranges changed: base, template-haskell

API changes (from Hackage documentation)

Files

• CHANGELOG.md +8/−0
• README.md +5/−12
• rerefined.cabal +20/−6
• src/Rerefined/Predicate.hs +38/−28
• src/Rerefined/Predicate/Common.hs +18/−25
• src/Rerefined/Predicate/Common/Binary.hs +13/−0
• src/Rerefined/Predicate/Fail.hs +5/−4
• src/Rerefined/Predicate/Logical.hs +34/−131
• src/Rerefined/Predicate/Logical/And.hs +56/−0
• src/Rerefined/Predicate/Logical/Equivalences.hs +19/−0
• src/Rerefined/Predicate/Logical/If.hs +29/−0
• src/Rerefined/Predicate/Logical/Iff.hs +33/−0
• src/Rerefined/Predicate/Logical/Nand.hs +27/−0
• src/Rerefined/Predicate/Logical/Nor.hs +30/−0
• src/Rerefined/Predicate/Logical/Not.hs +22/−0
• src/Rerefined/Predicate/Logical/Or.hs +27/−0
• src/Rerefined/Predicate/Logical/Xor.hs +30/−0
• src/Rerefined/Predicate/Relational.hs +1/−1
• src/Rerefined/Predicate/Relational/Internal.hs +76/−40
• src/Rerefined/Predicate/Relational/Length.hs +45/−15
• src/Rerefined/Predicate/Relational/Value.hs +18/−20
• src/Rerefined/Predicate/Succeed.hs +5/−4
• src/Rerefined/Predicates.hs +2/−3
• src/Rerefined/Predicates/RefinedShim.hs +0/−3
• src/Rerefined/Refine.hs +41/−14
• src/Rerefined/Refine/TH.hs +4/−2
• src/Rerefined/Refine/Unsafe.hs +0/−1
• src/Rerefined/Refined.hs +34/−4
• src/Rerefined/Refined1.hs +0/−18

@@ -1,3 +1,11 @@+## 0.3.0 (2024-05-07)+* refactor predicate names: now handled with a sort of type-level `Show`. no+  `Typeable`, lots of custom prettiness (infix operators!)+* refactor logical predicates, keeping them together doesn't help+* define relational operators using `Ordering` and logical `Or`+* add missing `Foldable`, `Traversable` instances to `Refined1`+* general cleanup+ ## 0.2.0 (2024-05-01) * add missing `Show` instance to `RefineFailure` * add missing `Functor` instance to `Refined1`

@@ -38,18 +38,11 @@ See [refined#101](https://github.com/nikita-volkov/refined/issues/101). `Typeable` is useful, but the way it is used brings lots of `Typeable` contexts. -rerefined has predicates declare their "predicate name" explicitly. You can-still use `Typeable` for non-combinator predicates, where no `Typeable` contexts-are incurred, but combinator predicates such as binary logical predicates-require more work. However, you can use all the existing `ShowS` helpers (that's-how `typeRep`s are printed anyway), so it's just like writing a manual `Show`-instance! Plus, combinator predicates are fairly unusual, so library users will-probably never see this.--Note that this change also improves predicate name display, since `typeRep`-tries to display inferred/hidden kinds for wrapped predicates in combinator-predicates, which are uninteresting. We can ignore these in our manual-instances!+rerefined asks that you do a bit more work upfront, but gives you tools and+grants much more power. Predicates declare their "predicate name" explicitly as+a type-level `Symbol`. Precedence is supported and infix operators are welcomed.+(For now, the logical operators primarily look like their propositional logic+counterparts.)  ### Cleaner design What do `LessThan`, `GreaterThan`, `EqualTo` etc. have in common? They're all

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           rerefined-version:        0.2.0+version:        0.3.0 synopsis:       Refinement types, again description:    Please see README.md. category:       Types, Data@@ -16,6 +16,10 @@ license:        MIT license-file:   LICENSE build-type:     Simple+tested-with:+    GHC==9.8+  , GHC==9.6+  , GHC==9.4 extra-source-files:     README.md     CHANGELOG.md@@ -29,20 +33,28 @@       Rerefined       Rerefined.Predicate       Rerefined.Predicate.Common+      Rerefined.Predicate.Common.Binary       Rerefined.Predicate.Fail       Rerefined.Predicate.Logical+      Rerefined.Predicate.Logical.And+      Rerefined.Predicate.Logical.Equivalences+      Rerefined.Predicate.Logical.If+      Rerefined.Predicate.Logical.Iff+      Rerefined.Predicate.Logical.Nand+      Rerefined.Predicate.Logical.Nor+      Rerefined.Predicate.Logical.Not+      Rerefined.Predicate.Logical.Or+      Rerefined.Predicate.Logical.Xor       Rerefined.Predicate.Relational       Rerefined.Predicate.Relational.Internal       Rerefined.Predicate.Relational.Length       Rerefined.Predicate.Relational.Value       Rerefined.Predicate.Succeed       Rerefined.Predicates-      Rerefined.Predicates.RefinedShim       Rerefined.Refine       Rerefined.Refine.TH       Rerefined.Refine.Unsafe       Rerefined.Refined-      Rerefined.Refined1   other-modules:       Paths_rerefined   hs-source-dirs:@@ -60,8 +72,10 @@       MagicHash   ghc-options: -Wall -Wno-unticked-promoted-constructors   build-depends:-      base >=4.16 && <5+      base >=4.17 && <5     , mono-traversable >=1.0.17.0 && <1.1-    , template-haskell-    , typeably >=0.1.0 && <0.2+    , template-haskell >=2.19.0.0 && <2.22+    , text >=2.0 && <2.2+    , text-builder-linear >=0.1.2 && <0.2+    , type-level-show >=0.1.0 && <0.2   default-language: GHC2021

@@ -1,40 +1,50 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+ -- | Base definitions for refinement predicates.  module Rerefined.Predicate   ( Refine(validate)   , Refine1(validate1)   , RefineFailure(..)-  , Predicate(predicateName)+  , Predicate(..)+  , predicateName   ) where -import GHC.Exts ( Proxy# )-import Data.Typeable ( Typeable, typeRep )-import Data.Typeable.Typeably-import Data.Proxy ( Proxy(Proxy) )+import GHC.Exts ( Proxy#, proxy# )+import Data.Text.Builder.Linear qualified as TBL+import GHC.TypeLits ( Natural, Symbol, KnownSymbol, symbolVal' )  -- | Types which define refinements on other types. class Predicate p where-    -- | The predicate name, as a 'Show'-like (for good bracketing).+    -- | Predicate name.     ---    -- Non-combinator predicates may derive this via 'Typeably'. Combinator-    -- predicates must write a 'Show'-like instance manually, in order to avoid-    -- incurring insidious 'Typeable' contexts for the wrapped predicate(s).-    -- (TODO figure out some generics and/or TH to resolve that)-    predicateName :: Proxy# p -> Int -> ShowS+    -- Predicate names should aim to communicate the meaning of the predicate as+    -- clearly and concisely as possible.+    --+    -- Consider using @type-level-show@ to build this. However, note that GHC+    -- cannot figure out 'KnownSymbol' when there are type families in play, so+    -- you may need to put 'KnownSymbol' constraints in instance contexts.+    type PredicateName (d :: Natural) p :: Symbol+        -- ^ TODO d: the operator precedence of the enclosing context (a number+        --   from 0 to 11). Function application has precedence 10. --- | Fill out predicate metadata using its 'Typeable' instance.------ Do not use this for combinator predicates. Doing so will incur insidious--- 'Typeable' contexts for the wrapped predicate(s).-instance Typeable a => Predicate (Typeably a) where-    predicateName _ d = showsPrec d (typeRep (Proxy @a))+{- TODO+stuffing the KnownSymbol constraint into a Predicate superclass is handy, but+then we have to handle it in combinator predicates. probably _not_ doing so is+better, so I'm trying that first.+-} +-- | Reify predicate name.+predicateName+    :: forall p. (Predicate p, KnownSymbol (PredicateName 0 p)) => String+predicateName = symbolVal' (proxy# @(PredicateName 0 p))+ -- | Refine @a@ with predicate @p@. class Predicate p => Refine p a where     -- | Validate predicate @p@ for the given @a@.     --     -- 'Nothing' indicates success. 'Just' contains a validation failure.-    validate :: Proxy# p -> a -> Maybe (RefineFailure String)+    validate :: Proxy# p -> a -> Maybe RefineFailure  -- | Refine functor type @f@ with functor predicate @p@. --@@ -43,20 +53,20 @@ -- structure, and not the stored elements. class Predicate p => Refine1 p f where     -- | Validate predicate @p@ for the given @f a@.-    validate1 :: Proxy# p -> f a -> Maybe (RefineFailure String)+    validate1 :: Proxy# p -> f a -> Maybe RefineFailure  -- | Predicate validation failure.------ Polymorphic over the message type because I want to use 'Text', but want it--- doesn't have the convenient 'Show' internals that 'String' does.-data RefineFailure a = RefineFailure-  { refineFailurePredicate :: a-  -- ^ The predicate that failed.+data RefineFailure = RefineFailure+  { refineFailurePredicate :: TBL.Builder+  -- ^ The name of the predicate that failed.+  --+  -- Obtained via 'predicateName'. -  , refineFailureDetail    :: a-  -- ^ Failure clarification.+  , refineFailureDetail    :: TBL.Builder+  -- ^ Precise failure detail e.g. which of the inner predicates of an @And@+  --   combinator predicate failed. -  , refineFailureInner     :: [RefineFailure a]+  , refineFailureInner     :: [RefineFailure]   -- ^ Any wrapped errors, for combinator predicates.   --   -- What these are, and their order, should be noted in 'refineFailureDetail'.

@@ -6,45 +6,38 @@   (   -- * Re-exports     module Rerefined.Predicate-  , Typeably(..), Typeable   , proxy#+  , TBL.Builder+  , IsString -- TODO remove    -- * Predicate validation   , validateFail, validateBool--  -- * Predicate name-  , predicateName1, predicateName2+  , KnownPredicateName   ) where  import Rerefined.Predicate-import GHC.Exts ( Proxy#, proxy# )-import Data.Typeable.Typeably-import Data.Typeable ( Typeable )+import GHC.Exts ( Proxy#, proxy#, IsString(fromString) )+import GHC.TypeLits ( KnownSymbol )+import Data.Text.Builder.Linear qualified as TBL +-- TODO maybe move to main 'Rerefined.Predicate' module+type KnownPredicateName p = KnownSymbol (PredicateName 0 p)+ -- | Shortcut for returning a predicate validation failure. validateFail     :: forall p-    .  Predicate p-    => Proxy# p -> String -> [RefineFailure String]-    -> Maybe (RefineFailure String)-validateFail p msg es = Just $ RefineFailure (predicateName p 0 "") msg es+    .  (Predicate p, KnownPredicateName p)+    => Proxy# p -> TBL.Builder -> [RefineFailure]+    -> Maybe RefineFailure+validateFail _p msg es =+    Just $ RefineFailure (fromString $ predicateName @p) msg es  -- | Shortcut for simply validating a 'Bool'. validateBool-    :: Predicate p => Proxy# p -> String -> Bool-    -> Maybe (RefineFailure String)+    :: forall p+    .  (Predicate p, KnownPredicateName p)+    => Proxy# p -> TBL.Builder -> Bool+    -> Maybe RefineFailure validateBool p e = \case   True  -> Nothing   False -> validateFail p e []--predicateName1 :: forall p. Predicate p => String -> Int -> ShowS-predicateName1 pName d = showParen (d > 10) $-      showString pName . showChar ' '-    . predicateName (proxy# @p) 11--predicateName2-    :: forall l r. (Predicate l, Predicate r) => String -> Int -> ShowS-predicateName2 pName d = showParen (d > 10) $-      showString pName . showChar ' '-    . predicateName (proxy# @l) 11 . showChar ' '-    . predicateName (proxy# @r) 11

@@ -0,0 +1,13 @@+-- | Common utilities for binary combinator predicates.++module Rerefined.Predicate.Common.Binary where++import Rerefined.Predicate+import TypeLevelShow.Utils+import GHC.TypeNats++-- | Render a binary combinator predicate with an infix operator.+--+-- The operator must include the left and right spaces.+type PredicateNameBOp op prec d l r = ShowParen (d > prec)+    (PredicateName (prec+1) l ++ op ++ PredicateName (prec+1) r)

@@ -1,9 +1,10 @@+{-# LANGUAGE OverloadedStrings #-}+ module Rerefined.Predicate.Fail where  import Rerefined.Predicate.Common  -- | Always fails.-data Fail deriving Predicate via Typeably Fail--instance Refine Fail a where-    validate p _ = validateFail p "fail" []+data Fail+instance Predicate Fail where type PredicateName d Fail = "⊥"+instance Refine Fail a where validate p _ = validateFail p "fail" []

@@ -1,138 +1,41 @@-{-# LANGUAGE AllowAmbiguousTypes #-}--module Rerefined.Predicate.Logical where--import Rerefined.Predicate.Common-import Rerefined.Refined-import Rerefined.Refine.Unsafe---- | Logical binary operator.------ No need to disambiguate that these are binary operators, because there's only--- one logical unary operator 'Not'.-data LogicOp = And | Or | Nand | Nor | Xor | Xnor---- | A logical binary operation on two predicates.-data Logical (op :: LogicOp) l r---- TODO could do whatever we want here e.g. infix. (but idk what e.g. XNOR uses)-instance (Predicate l, Predicate r, ReifyLogicOp op)-  => Predicate (Logical op l r) where-    predicateName _ d = showParen (d > 10) $-          showString "Logical "-        . showString (reifyLogicOpPretty @op) . showChar ' '-        . predicateName (proxy# @l) 11 . showChar ' '-        . predicateName (proxy# @r) 11--instance (Refine l a, Refine r a, ReifyLogicOp op)-  => Refine (Logical op l r) a where-    validate p a =-        reifyLogicOp @op (validateFail p)-            (validate (proxy# @l) a)-            (validate (proxy# @r) a)---- | Reify a logical binary operator type tag.-class ReifyLogicOp (op :: LogicOp) where-    reifyLogicOpPretty :: String-    reifyLogicOp-        :: (String -> [a] -> Maybe a)-        -> Maybe a-        -> Maybe a-        -> Maybe a--instance ReifyLogicOp And where-    reifyLogicOpPretty = "And"-    reifyLogicOp fFail l r =-        case l of-          Nothing ->-            case r of-              Nothing -> Nothing-              Just er -> fFail "AND:  right failed"    [    er]-          Just el ->-            case r of-              Nothing -> fFail "AND:   left failed"    [el    ]-              Just er -> fFail "AND:    l&r failed"    [el, er]--instance ReifyLogicOp Or where-    reifyLogicOpPretty = "Or"-    reifyLogicOp fFail l r =-        case l of-          Nothing -> Nothing-          Just el ->-            case r of-              Nothing -> Nothing-              Just er -> fFail "OR:     l&r failed"    [el, er]--instance ReifyLogicOp Nand where-    reifyLogicOpPretty = "Nand"-    reifyLogicOp fFail l r =-        case l of-          Just _  -> Nothing-          Nothing ->-            case r of-              Just _  -> Nothing-              Nothing -> fFail "NAND:   l&r succeeded" [      ]--instance ReifyLogicOp Nor where-    reifyLogicOpPretty = "Nor"-    reifyLogicOp fFail l r =-        case l of-          Just el ->-            case r of-              Just _  -> Nothing-              Nothing -> fFail "NOR:  right succeeded" [el    ]-          Nothing ->-            case r of-              Just er -> fFail "NOR:   left succeeded" [    er]-              Nothing -> fFail "NOR:    l&r succeeded" [      ]--instance ReifyLogicOp Xor where-    reifyLogicOpPretty = "Xor"-    reifyLogicOp fFail l r =-        case l of-          Nothing ->-            case r of-              Just _  -> Nothing-              Nothing -> fFail "XOR:    l&r succeeded" [      ]-          Just el ->-            case r of-              Nothing -> Nothing-              Just er -> fFail "XOR:    l&r failed"    [el, er]+{-# LANGUAGE UndecidableInstances #-} -- TODO TMP -instance ReifyLogicOp Xnor where-    reifyLogicOpPretty = "Xnor"-    reifyLogicOp fFail l r =-        case l of-          Nothing ->-            case r of-              Nothing -> Nothing-              Just er -> fFail "XNOR: right failed"    [    er]-          Just el ->-            case r of-              Just _  -> Nothing-              Nothing -> fFail "XNOR:  left failed"    [el    ]+module Rerefined.Predicate.Logical+  ( And, Iff, If, Nand, Nor, Not, Or, Xor+  , NormalizeLogicalStep+  , NormalizeLogical1Step+  , Result(..), Idk1'+  ) where -data Not p+import Rerefined.Predicate.Logical.And+import Rerefined.Predicate.Logical.Iff+import Rerefined.Predicate.Logical.If+import Rerefined.Predicate.Logical.Nand+import Rerefined.Predicate.Logical.Nor+import Rerefined.Predicate.Logical.Not+import Rerefined.Predicate.Logical.Or+import Rerefined.Predicate.Logical.Xor -instance Predicate p => Predicate (Not p) where-    predicateName _ = predicateName1 @p "Not"+import Data.Kind ( Type )+-- left = continue, right = normalized+type NormalizeLogicalStep :: (kl -> kr -> Type) -> kl -> kr -> Result kl+type family NormalizeLogicalStep op l r where+    NormalizeLogicalStep Or   l l = Cont  l+    NormalizeLogicalStep And  l l = Cont  l+    NormalizeLogicalStep Nand l l = Cont1 (Not l)+    NormalizeLogicalStep op   l r = Done (op l r) -instance Refine p a => Refine (Not p) a where-    validate p a =-        case validate (proxy# @p) a of-          Just _  -> Nothing-          Nothing -> validateFail p "NOT: predicate succeeded" []+data Result kl = Done Type | Cont kl | Cont1 Type --- TODO principle of explosion? (p and not p -> anything)+type NormalizeLogical1Step :: (k -> Type) -> k -> Result k+type family NormalizeLogical1Step op p where+    NormalizeLogical1Step Not (Not p) = Cont p+    NormalizeLogical1Step op  p       = Done (op p) --- TODO-rerefineDeMorgans1-    :: Refined (Not (Logical Or  l r))       a-    -> Refined (Logical And (Not l) (Not r)) a-rerefineDeMorgans1 = unsafeRerefine+type family Idk1 res where+    Idk1 (Cont p) = Idk1' p+    Idk1 (Done p) = p --- TODO-rerefineDeMorgans2-    :: Refined (Not (Logical And l r))       a-    -> Refined (Logical Or  (Not l) (Not r)) a-rerefineDeMorgans2 = unsafeRerefine+type family Idk1' p where+    Idk1' (Not p) = Idk1 (NormalizeLogical1Step Not p)+    Idk1' p = p

@@ -0,0 +1,56 @@+{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName+{-# LANGUAGE OverloadedStrings #-} -- for builder++module Rerefined.Predicate.Logical.And where++import Rerefined.Predicate.Common.Binary+import Rerefined.Predicate.Common+import Rerefined.Refine.Unsafe+import Rerefined.Refined++-- | Logical conjunction. Also AND logic gate.+data And l r++-- | Precendence of 3 (matching 'Data.Bool.&&').+instance (Predicate l, Predicate r) => Predicate (And l r) where+    type PredicateName d (And l r) = PredicateNameBOp " ∧ " 3 d l r++instance (Refine l a, Refine r a, KnownPredicateName (And l r))+  => Refine (And l r) a where+    validate p a =+        case l of+          Nothing ->+            case r of+              Nothing -> Nothing+              Just er -> validateFail p "AND:  right failed"    [er    ]+          Just el ->+            case r of+              Nothing -> validateFail p "AND:   left failed"    [    el]+              Just er -> validateFail p "AND:    l&r failed"    [er, el]+      where+        l = validate (proxy# @l) a+        r = validate (proxy# @r) a++-- | 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

@@ -0,0 +1,19 @@+-- | Logical equivalences.++module Rerefined.Predicate.Logical.Equivalences where++{-++-- TODO+rerefineDeMorgans1+    :: Refined (Not (Logical Or  l r))       a+    -> Refined (Logical And (Not l) (Not r)) a+rerefineDeMorgans1 = unsafeRerefine++-- TODO+rerefineDeMorgans2+    :: Refined (Not (Logical And l r))       a+    -> Refined (Logical Or  (Not l) (Not r)) a+rerefineDeMorgans2 = unsafeRerefine++-}

@@ -0,0 +1,29 @@+{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName+{-# LANGUAGE OverloadedStrings #-} -- for builder++module Rerefined.Predicate.Logical.If where++import Rerefined.Predicate.Common.Binary+import Rerefined.Predicate.Common++-- | Logical implication. "If l then r".+data If l r++-- | Precendence of 4 (matching '==').+instance (Predicate l, Predicate r) => Predicate (If l r) where+    -- TODO double arrow? idk+    type PredicateName d (If l r) = PredicateNameBOp " → " 4 d l r++instance (Refine l a, Refine r a, KnownPredicateName (If l r))+  => Refine (If l r) a where+    validate p a =+        case l of+          Just _  -> Nothing+          Nothing ->+            case r of+              Nothing -> Nothing+              Just er ->+                validateFail p "IF: left succeeded, but right failed" [er]+      where+        l = validate (proxy# @l) a+        r = validate (proxy# @r) a

@@ -0,0 +1,33 @@+{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName+{-# LANGUAGE OverloadedStrings #-} -- for builder++module Rerefined.Predicate.Logical.Iff where++import Rerefined.Predicate.Common.Binary+import Rerefined.Predicate.Common++-- | Logical biconditional ("if and only if"). Also the XNOR logic gate, or+--   equivalence (loosely).+data Iff l r++-- | Precendence of 4 (matching '==').+instance (Predicate l, Predicate r) => Predicate (Iff l r) where+    type PredicateName d (Iff l r) = PredicateNameBOp " ↔ " 4 d l r++instance (Refine l a, Refine r a, KnownPredicateName (Iff l r))+  => Refine (Iff l r) a where+    validate p a =+        case l of+          Nothing ->+            case r of+              Nothing -> Nothing+              Just er ->+                validateFail p "IFF: left succeeded, but right failed" [er]+          Just el ->+            case r of+              Just _  -> Nothing+              Nothing ->+                validateFail p "IFF: left failed, but right succeeded" [el]+      where+        l = validate (proxy# @l) a+        r = validate (proxy# @r) a

@@ -0,0 +1,27 @@+{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName+{-# LANGUAGE OverloadedStrings #-} -- for builder++module Rerefined.Predicate.Logical.Nand where++import Rerefined.Predicate.Common.Binary+import Rerefined.Predicate.Common++-- | NAND logic gate. Also called the Sheffer stroke, or non-conjunction.+data Nand l r++-- | Precendence of 3 (matching 'Data.Bool.&&').+instance (Predicate l, Predicate r) => Predicate (Nand l r) where+    type PredicateName d (Nand l r) = PredicateNameBOp " ⊼ " 3 d l r++instance (Refine l a, Refine r a, KnownPredicateName (Nand l r))+  => Refine (Nand l r) a where+    validate p a =+        case l of+          Just _  -> Nothing+          Nothing ->+            case r of+              Just _  -> Nothing+              Nothing -> validateFail p "NAND: l&r succeeded" []+      where+        l = validate (proxy# @l) a+        r = validate (proxy# @r) a

@@ -0,0 +1,30 @@+{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName+{-# LANGUAGE OverloadedStrings #-} -- for builder++module Rerefined.Predicate.Logical.Nor where++import Rerefined.Predicate.Common.Binary+import Rerefined.Predicate.Common++-- | NOR logic gate. Also called non-disjunction, or joint denial.+data Nor l r++-- | Precendence of 2 (matching 'Data.Bool.||').+instance (Predicate l, Predicate r) => Predicate (Nor l r) where+    type PredicateName d (Nor l r) = PredicateNameBOp " ⊽ " 2 d l r++instance (Refine l a, Refine r a, KnownPredicateName (Nor l r))+  => Refine (Nor l r) a where+    validate p a =+        case l of+          Just _ ->+            case r of+              Just _  -> Nothing+              Nothing -> validateFail p "NOR: left succeeded"  []+          Nothing ->+            case r of+              Just _  -> validateFail p "NOR: right succeeded" []+              Nothing -> validateFail p "NOR: l&r succeeded"   []+      where+        l = validate (proxy# @l) a+        r = validate (proxy# @r) a

@@ -0,0 +1,22 @@+{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName+{-# LANGUAGE OverloadedStrings #-} -- for builder++module Rerefined.Predicate.Logical.Not where++import Rerefined.Predicate.Common+import TypeLevelShow.Utils++-- | Logical negation. Also NOT logic gate, or logical complement.+data Not p++-- | Precendence of 9 (one below function application).+instance Predicate p => Predicate (Not p) where+    type PredicateName d (Not p) = ShowParen (d > 9)+        ("¬ " ++ PredicateName 10 p)++instance (Refine p a, KnownPredicateName (Not p))+  => Refine (Not p) a where+    validate p a =+        case validate (proxy# @p) a of+          Just _  -> Nothing+          Nothing -> validateFail p "NOT: predicate succeeded" []

@@ -0,0 +1,27 @@+{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName+{-# LANGUAGE OverloadedStrings #-} -- for builder++module Rerefined.Predicate.Logical.Or where++import Rerefined.Predicate.Common.Binary+import Rerefined.Predicate.Common++-- | Logical disjunction. Also OR logic gate.+data Or l r++-- | Precendence of 2 (matching 'Data.Bool.||').+instance (Predicate l, Predicate r) => Predicate (Or l r) where+    type PredicateName d (Or l r) = PredicateNameBOp " ∨ " 2 d l r++instance (Refine l a, Refine r a, KnownPredicateName (Or l r))+  => Refine (Or l r) a where+    validate p a =+        case l of+          Nothing -> Nothing+          Just el ->+            case r of+              Nothing -> Nothing+              Just er -> validateFail p "OR: l&r failed" [er, el]+      where+        l = validate (proxy# @l) a+        r = validate (proxy# @r) a

@@ -0,0 +1,30 @@+{-# LANGUAGE UndecidableInstances #-} -- for easier PredicateName+{-# LANGUAGE OverloadedStrings #-} -- for builder++module Rerefined.Predicate.Logical.Xor where++import Rerefined.Predicate.Common.Binary+import Rerefined.Predicate.Common++-- | Logical exclusive disjunction. Also XOR logic gate.+data Xor l r++-- | Precendence of 4 (matching '==').+instance (Predicate l, Predicate r) => Predicate (Xor l r) where+    type PredicateName d (Xor l r) = PredicateNameBOp " ⊕ " 4 d l r++instance (Refine l a, Refine r a, KnownPredicateName (Xor l r))+  => Refine (Xor l r) a where+    validate p a =+        case l of+          Nothing ->+            case r of+              Just _  -> Nothing+              Nothing -> validateFail p "XOR: l&r succeeded" [      ]+          Just el ->+            case r of+              Nothing -> Nothing+              Just er -> validateFail p "XOR: l&r failed"    [er, el]+      where+        l = validate (proxy# @l) a+        r = validate (proxy# @r) a

@@ -1,8 +1,8 @@ module Rerefined.Predicate.Relational   ( CompareValue   , Sign(..)-  , RelOp(..)   , CompareLength+  , LTE, GTE   ) where  import Rerefined.Predicate.Relational.Internal

@@ -1,75 +1,111 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE UndecidableInstances #-} -- for weird TODO stuff+{-# LANGUAGE AllowAmbiguousTypes #-}  -- for ReifyRelOp+{-# LANGUAGE UndecidableInstances #-} -- for WidenRelOp -module Rerefined.Predicate.Relational.Internal where+{- | Relational operator definitions. -import Data.Typeable ( Typeable )+Haskell base exports the type 'Ordering', which is an enum that states the+result of comparing two 'Ord's. We can utilize this to define /relational+operators/: +* 'LT', 'EQ' and 'GT' already map to relational operators.+* The others can be defined by combining the above with 'Or'. e.g. @'LT' ``Or``+  'EQ'@ -> "less than or equal" ('<=')++What's the point? We save on definitions, and get to reuse well-known data types+which most users will have intuition for. We do have to contest with+commutativity, but this is an extremely minor concern which can only come up if+you don't use the provided type synonyms, or do lots of type-level predicate+manipulation. And we provide those swapped-order instances anyway!+-}++module Rerefined.Predicate.Relational.Internal where++import Rerefined.Predicate.Logical.Or import GHC.TypeNats import Data.Type.Ord ( OrdCond )+import GHC.TypeLits ( Symbol ) --- | Relational operator.------ There are three possible outcomes from 'compare'ing two terms, defined in--- 'Ordering'. However, we may instead compare terms using relational operators--- such as @>=@, which are more specific comparisons that return a 'Bool'.------ Constructor order is arbitrary due to @NEQ@, which obstructs ordering in a--- meaningful way.-data RelOp-  = LT' -- ^ '<'  less than-  | LTE -- ^ '<=' less than or equal to-  | EQ' -- ^ '=='              equal to-  | NEQ -- ^ '/=' less than or             greater than-  | GTE -- ^ '>='              equal to or greater than-  | GT' -- ^ '>'                           greater than+import Data.Kind ( Type ) +type LTE = LT `Or` EQ++-- | "not equal to" is equivalent to "strictly less than or greater than". We+--   could use 'Rerefined.Predicate.Logical.Not.Not', but sticking with just+--   'Or' keeps the internals simple.+type NEQ = LT `Or` GT++type GTE = GT `Or` EQ+ -- | Reify a relational operator type tag. ----- We stuff the 'Typeable' constraint in here because we need it for easy--- 'Rerefined.Predicate.Predicate' instances, and we don't want to expose the--- 'Typeable' constraint elsewhere.-class Typeable op => ReifyRelOp (op :: RelOp) where-    -- | The term-level relational operator that @op@ describes.-    reifyRelOp :: forall a. (Num a, Ord a) => a -> a -> Bool+-- Permitted operators are @Ordering@ constructors 'LT', 'EQ' and 'GT'; and+-- combinations of these using 'Or'.+class ReifyRelOp op where+    -- | Pretty @op@.+    type ShowRelOp op :: Symbol -    -- | Pretty operator.-    reifyRelOpPretty :: String+    -- | The term-level relational operator that @op@ describes.+    reifyRelOp :: forall a. Ord a => a -> a -> Bool -instance ReifyRelOp LT' where+instance ReifyRelOp LT where+    type ShowRelOp LT = "<"     reifyRelOp = (<)-    reifyRelOpPretty = "<"  instance ReifyRelOp LTE where+    type  ShowRelOp LTE = "<="     reifyRelOp = (<=)-    reifyRelOpPretty = "<=" -instance ReifyRelOp EQ' where+-- | Hidden instance. You won't see this if you use the type synonyms.+deriving via LTE instance ReifyRelOp (EQ `Or` LT)++instance ReifyRelOp EQ where+    type  ShowRelOp EQ = "=="     reifyRelOp = (==)-    reifyRelOpPretty = "=="  instance ReifyRelOp NEQ where+    type  ShowRelOp NEQ = "/="     reifyRelOp = (/=)-    reifyRelOpPretty = "/=" +-- | Hidden instance. You won't see this if you use the type synonyms.+deriving via NEQ instance ReifyRelOp (GT `Or` LT)+ instance ReifyRelOp GTE where+    type ShowRelOp GTE = ">="     reifyRelOp = (>=)-    reifyRelOpPretty = ">=" -instance ReifyRelOp GT' where+-- | Hidden instance. You won't see this if you use the type synonyms.+deriving via GTE instance ReifyRelOp (EQ `Or` GT)++instance ReifyRelOp GT where+    type ShowRelOp GT = ">"     reifyRelOp = (>)-    reifyRelOpPretty = ">" --- | Can we widen the given 'RelOp' from @n@ to @m@?-type family WidenRelOp (op :: RelOp) (n :: Natural) (m :: Natural) where+-- | Can we widen the given 'RelOp' on the given 'Natural' from @n@ to @m@?+type WidenRelOp :: k -> Natural -> Natural -> Bool+type family WidenRelOp op n m where     -- @n == m@? no problem     WidenRelOp op  n n = True      -- I'd love to simplify this, but 'CmpNat' is opaque.-    WidenRelOp LT' n m = OrdCond (CmpNat n m) True  True False+    WidenRelOp LT  n m = OrdCond (CmpNat n m) True  True False     WidenRelOp LTE n m = OrdCond (CmpNat n m) True  True False     WidenRelOp GTE n m = OrdCond (CmpNat n m) False True True-    WidenRelOp GT' n m = OrdCond (CmpNat n m) False True True+    WidenRelOp GT  n m = OrdCond (CmpNat n m) False True True +    -- | swapped LTE, lower down in equation list because less common+    WidenRelOp (EQ `Or` LT) n m =+        OrdCond (CmpNat n m) True  True False++    -- | swapped GTE, lower down in equation list because less common+    WidenRelOp (EQ `Or` GT) n m =+        OrdCond (CmpNat n m) False True True+     -- can't widen (==) or (/=)     WidenRelOp _   _ _ = False++-- this gets clumsier due to kinding clashes (k vs. Ordering)+type NormalizeOrRelOp :: Type -> Type+type family NormalizeOrRelOp op where+    NormalizeOrRelOp (EQ `Or` LT) = LTE+    NormalizeOrRelOp (GT `Or` LT) = NEQ+    NormalizeOrRelOp (EQ `Or` GT) = GTE

@@ -1,3 +1,6 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE UndecidableInstances #-} -- for GHC <= 9.4, WROE+ module Rerefined.Predicate.Relational.Length where  import Rerefined.Predicate.Common@@ -6,34 +9,45 @@ import Data.MonoTraversable ( MonoFoldable(olength) ) import GHC.Exts ( Proxy# ) -import Rerefined.Refined-import Rerefined.Refine.Unsafe ( unsafeRerefine )+import Rerefined.Refine.Unsafe import GHC.TypeError import Data.Kind ( type Constraint )+import TypeLevelShow.Utils+import TypeLevelShow.Natural+import Data.Text.Builder.Linear qualified as TBL  -- | Compare length to a type-level 'Natural' using the given 'RelOp'.-data CompareLength (op :: RelOp) (n :: Natural)-    deriving Predicate via Typeably (CompareLength op n)+data CompareLength op (n :: Natural) +-- | Precedence of 4 (matching base relational operators e.g. '>=').+instance Predicate (CompareLength op n) where+    type PredicateName d (CompareLength op n) = ShowParen (d > 4)+        ("Length " ++ ShowRelOp op ++ ShowChar ' ' ++ ShowNatDec n)+ -- | Compare the length of a 'Foldable' to a type-level 'Natural' using the --   given 'RelOp'.-instance (KnownNat n, Foldable f, ReifyRelOp op)-  => Refine1 (CompareLength op n) f where+instance+  ( KnownNat n, Foldable f, ReifyRelOp op+  , KnownPredicateName (CompareLength op n)+  ) => Refine1 (CompareLength op n) f where     validate1 p = validateCompareLength p . length  -- | Compare the length of a 'MonoFoldable' to a type-level 'Natural' using the --   given 'RelOp'.-instance (KnownNat n, MonoFoldable a, ReifyRelOp op)-  => Refine (CompareLength op n) a where+instance+  ( KnownNat n, MonoFoldable a, ReifyRelOp op+  , KnownPredicateName (CompareLength op n)+  ) => Refine (CompareLength op n) a where     validate p = validateCompareLength p . olength  validateCompareLength-    :: forall op n. (KnownNat n, ReifyRelOp op)-    => Proxy# (CompareLength op n) -> Int -> Maybe (RefineFailure String)+    :: forall op n+    .  ( KnownNat n, ReifyRelOp op+       , KnownPredicateName (CompareLength op n)+    ) => Proxy# (CompareLength op n) -> Int -> Maybe RefineFailure validateCompareLength p len =-    validateBool p ("length not "<>reifyRelOpPretty @op<>" "<>show n)-        (reifyRelOp @op len (fromIntegral n))-  where n = natVal' (proxy# @n)+    validateBool p ("length: "<>TBL.fromDec n) (reifyRelOp @op len n)+  where n = fromIntegral (natVal' (proxy# @n))  -- | Widen a length comparison predicate. --@@ -51,9 +65,25 @@     -> Refined (CompareLength op m) a widenCompareLength = unsafeRerefine +-- | Widen a length comparison predicate.+--+-- Only valid widenings are permitted, checked at compile time.+--+-- Example: Given a >= 1, we know also that a >= 0. Thus, this function allows+-- you to turn a @Refined1 (CompareLength GTE 1) f a@ into a @Refined1+-- (CompareLength GTE 0) f a@.+--+-- TODO improve type error here+widenCompareLength1+    :: forall m op n f a+    .  WROE op n m+    => Refined1 (CompareLength op n) f a+    -> Refined1 (CompareLength op m) f a+widenCompareLength1 = unsafeRerefine1+ type WROE op n m = WROE' op n m (WidenRelOp op n m)-type WROE' :: RelOp -> Natural -> Natural -> Bool -> Constraint-type family WROE' (op :: RelOp) (n :: Natural) (m :: Natural) (b :: Bool) where+type WROE' :: k -> Natural -> Natural -> Bool -> Constraint+type family WROE' op n m b where     WROE' op n m True  = ()     WROE' op n m False = TypeError       (      Text "can't widen relational equation "

@@ -1,44 +1,42 @@-{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE UndecidableInstances #-} -- for PredicateName+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE AllowAmbiguousTypes #-} -- for signPretty  module Rerefined.Predicate.Relational.Value where  import Rerefined.Predicate.Common import Rerefined.Predicate.Relational.Internal import GHC.TypeNats ( Natural, KnownNat, natVal' )+import TypeLevelShow.Utils+import TypeLevelShow.Natural+import GHC.TypeLits ( Symbol )  -- | Compare value to a type-level 'Natural' using the given 'RelOp'.-data CompareValue (op :: RelOp) (sign :: Sign) (n :: Natural)-    deriving Predicate via Typeably (CompareValue op sign n)--- TODO I could write custom predicateNames here if I wanted to override how--- they display. But I don't mind the expanded type synonyms. @CompareValue--- 'CBOpLT 10@ still makes sense to me, especially with the extra message.------ I should simplify op names, but not sure what to, since I can't use LT/EQ/GT.-{--instance KnownNat n => Predicate (LessThan n) where-    predicateName d = showParen (d > 10) $-        showString "LessThan " . showsPrec 11 (natVal' (proxy# :: Proxy# n))--}+data CompareValue op (sign :: Sign) (n :: Natural) ---type LessThan n = CompareValue LT' n+-- | Precedence of 4 (matching base relational operators e.g. '>=').+instance Predicate (CompareValue op sign n) where+    type PredicateName d (CompareValue op sign n) = ShowParen (d > 4)+        (    "Value " ++ ShowRelOp op ++ ShowChar ' '+          ++ ShowSign sign ++ ShowNatDec n )  instance   ( KnownNat n, Num a, Ord a-  , ReifyRelOp op, ReifySignedNat sign n, ReifySign sign+  , ReifyRelOp op, ReifySignedNat sign n+  , KnownPredicateName (CompareValue op sign n)   ) => Refine (CompareValue op sign n) a where     -- note that we show the reified 'Natural' rather than the coerced numeric     -- type, as otherwise we'd need a @'Show' a@     validate p a =         validateBool p-            ("value not "<>reifyRelOpPretty @op<>" "<>signPretty @sign<>show n)+            ("bad value")             (reifyRelOp @op a (reifySignedNat @sign @n))-      where n = natVal' (proxy# @n)  data Sign = Pos | Neg -class Typeable sign => ReifySign (sign :: Sign) where signPretty :: String-instance ReifySign Pos where signPretty = ""-instance ReifySign Neg where signPretty = "-"+type family ShowSign (sign :: Sign) :: Symbol where+    ShowSign Pos = ""+    ShowSign Neg = "-"  -- TODO do I add any KnownNat constraints anywhere here class ReifySignedNat (sign :: Sign) (n :: Natural) where

@@ -1,9 +1,10 @@+{-# LANGUAGE OverloadedStrings #-}+ module Rerefined.Predicate.Succeed where  import Rerefined.Predicate.Common  -- | The unit predicate. Always succeeds.-data Succeed deriving Predicate via Typeably Succeed--instance Refine Succeed a where-    validate _ _ = Nothing+data Succeed+instance Predicate Succeed where type PredicateName d Succeed = "⊤"+instance Refine Succeed a where validate _ _ = Nothing

@@ -7,14 +7,13 @@   , Fail    -- * Logical-  , Not-  , Logical+  , And, Iff, If, Nand, Nor, Not, Or, Xor    -- * Relational   , CompareValue   , Sign(..)-  , RelOp(..)   , CompareLength+  , LTE, GTE   ) where  import Rerefined.Predicate.Succeed

@@ -1,3 +0,0 @@-module Rerefined.Predicates.RefinedShim where---- TODO cba

@@ -15,17 +15,19 @@   -- * Errors   , type RefineFailure   , prettyRefineFailure+  , prettyRefineFailure'   ) where  import Rerefined.Refined-import Rerefined.Refined1 import Rerefined.Predicate-import GHC.Exts ( proxy#, IsString )+import GHC.Exts ( proxy# )+import Data.Text ( Text )+import Data.Text.Builder.Linear qualified as TBL  -- | Refine @a@ with predicate @p@. refine     :: forall p a. Refine p a-    => a -> Either (RefineFailure String) (Refined p a)+    => a -> Either RefineFailure (Refined p a) refine a =     case validate (proxy# @p) a of       Nothing -> Right (Refined a)@@ -37,23 +39,48 @@ -- | Refine @f a@ with functor predicate @p@. refine1     :: forall p f a. Refine1 p f-    => f a -> Either (RefineFailure String) (Refined1 p f a)+    => f a -> Either RefineFailure (Refined1 p f a) refine1 fa =     case validate1 (proxy# @p) fa of       Nothing -> Right (Refined1 fa)       Just e  -> Left e --- TODO needs work. boring & idk how to format nicely. and extra \n at start-prettyRefineFailure :: (Semigroup a, IsString a) => RefineFailure a -> a-prettyRefineFailure = go (0 :: Int) . (\e -> [e])+{- TODO+* got an extra \n at start oops+* make it look better lol+* make tail-call recursive? need to ferry more indents around though+-}+prettyRefineFailure :: RefineFailure -> Text+prettyRefineFailure = TBL.runBuilder . go (0 :: Int) . (\e -> [e])   where     go n = \case-      []     -> ""+      []     -> mempty       (e:es) ->-           "\n" <> indent n     <> refineFailurePredicate e-        <> "\n" <> indent (n+2) <> refineFailureDetail    e-        <> go (n+2) (refineFailureInner e)-        <> go n es+        let bPred   = TBL.fromChar '\n' <> indent n <> refineFailurePredicate e+            bDetail = TBL.fromChar '\n' <> indent (n+2) <> refineFailureDetail e+         in bPred <> bDetail <> go (n+2) (refineFailureInner e) <> go n es     indent = \case-      0 -> ""-      n -> " " <> indent (n-1)+      0 -> mempty+      n -> TBL.fromChar ' ' <> indent (n-1)++-- TODO this requires switching inner errors so that last is first lol x)+-- also we only <> right. maybe that's useful for perf+-- to remove newline at start we need to start in a special mode so we know not+-- to add the first newline at bPred. but I cba it will be messier and I want to+-- replace this ASAP when someone comes up with a good pretty error format+prettyRefineFailure' :: RefineFailure -> Text+prettyRefineFailure' = \e -> TBL.runBuilder $ go mempty [(0 :: Int, e)]+  where+    go b = \case+      []            -> b+      ((n, e) : es) ->+        let bPred   = TBL.fromChar '\n' <> indent n <> refineFailurePredicate e+            bDetail = TBL.fromChar '\n' <> indent (n+2) <> refineFailureDetail e+            b'      = b <> bPred <> bDetail+         in go b' (idk (n+2) es (refineFailureInner e))+    indent = \case+      0 -> mempty+      n -> TBL.fromChar ' ' <> indent (n-1)+    idk n rs = \case+      []   -> rs+      l:ls -> idk n ((n, l):rs) ls

@@ -6,6 +6,7 @@ import Rerefined.Refine import Rerefined.Predicate import Language.Haskell.TH.Syntax qualified as TH+import Data.Text qualified as Text  -- | Refine @a@ with predicate @p@ at compile time via Template Haskell. refineTH@@ -25,5 +26,6 @@ refine1TH = either refineTHFail TH.liftTyped . refine1 @p @f  -- | Template Haskell refinement failure helper.-refineTHFail :: forall a m. MonadFail m => RefineFailure String -> TH.Code m a-refineTHFail = TH.liftCode . fail . prettyRefineFailure+refineTHFail+    :: forall a m. MonadFail m => RefineFailure -> TH.Code m a+refineTHFail = TH.liftCode . fail . Text.unpack . prettyRefineFailure

@@ -23,7 +23,6 @@   ) where  import Rerefined.Refined-import Rerefined.Refined1  -- | Construct a 'Refined' without validating the predicate @p@. --

@@ -1,18 +1,48 @@--- | 'Refined' definition.+-- | 'Refined' and 'Refined1' definitions for refined values. ----- Not intended for external use. For unsafe refines, use+-- Not intended for external use. For unsafe refining, use -- 'Rerefined.Refine.Unsafe'. -module Rerefined.Refined where+module Rerefined.Refined+  (+  -- * @Refined@+    Refined(..)+  , unrefine +  -- * @Refined1@+  , Refined1(..)+  , unrefine1+  , squashRefined1+  ) where+ import Language.Haskell.TH.Syntax ( Lift )  -- | @a@ refined with predicate @p@. newtype Refined p a = Refined a-    deriving stock (Lift, Show) -- TODO Show? useful but meh?+    deriving stock (Lift, Show)  -- | Strip the refinement from a 'Refined'. -- -- This is kept as a separate function for prettier @'Show' 'Refined'@ output. unrefine :: Refined p a -> a unrefine (Refined a) = a++-- | @f a@ refined with predicate @p@.+--+-- We may derive legal 'Functor', 'Traversable' instances for this as+-- 'Rerefined.Predicate.Refine1' guarantees that the predicate only applies to+-- the functor structure. That is, you _may_ alter a 'Refined1' without+-- re-asserting its predicate, provided your changes are made without altering+-- the structure/shape of @f@ (e.g. 'fmap', 'traverse').+newtype Refined1 p f a = Refined1 (f a)+    deriving stock (Functor, Foldable, Traversable, Lift, Show)++-- | Strip the refinement from a 'Refined1'.+--+-- This is kept as a separate function for prettier @'Show' 'Refined1'@ output.+unrefine1 :: Refined1 p f a -> f a+unrefine1 (Refined1 fa) = fa++-- | Squash a 'Refined1' into a 'Refined'. Essentially forget the @f@.+squashRefined1 :: Refined1 p f a -> Refined p (f a)+squashRefined1 = Refined . unrefine1

@@ -1,18 +0,0 @@--- | 'Refined1' definition.------ Not intended for external use. For unsafe refines, use--- 'Rerefined.Refine.Unsafe'.--module Rerefined.Refined1 where--import Language.Haskell.TH.Syntax ( Lift )---- | @f a@ refined with predicate @p@.-newtype Refined1 p f a = Refined1 (f a)-    deriving stock (Functor, Lift, Show) -- TODO Show? useful but meh?---- | Strip the refinement from a 'Refined1'.------ This is kept as a separate function for prettier @'Show' 'Refined1'@ output.-unrefine1 :: Refined1 p f a -> f a-unrefine1 (Refined1 fa) = fa