rerefined (empty) → 0.1.0

raw patch · 20 files changed

+810/−0 lines, 20 filesdep +basedep +mono-traversabledep +template-haskell

Dependencies added: base, mono-traversable, template-haskell, typeably

Files

• CHANGELOG.md +4/−0
• LICENSE +20/−0
• README.md +92/−0
• rerefined.cabal +66/−0
• src/Rerefined/Predicate.hs +63/−0
• src/Rerefined/Predicate/Common.hs +50/−0
• src/Rerefined/Predicate/Fail.hs +9/−0
• src/Rerefined/Predicate/Logical.hs +138/−0
• src/Rerefined/Predicate/Relational.hs +10/−0
• src/Rerefined/Predicate/Relational/Internal.hs +75/−0
• src/Rerefined/Predicate/Relational/Length.hs +63/−0
• src/Rerefined/Predicate/Relational/Value.hs +51/−0
• src/Rerefined/Predicate/Succeed.hs +9/−0
• src/Rerefined/Predicates.hs +23/−0
• src/Rerefined/Predicates/RefinedShim.hs +3/−0
• src/Rerefined/Refine.hs +44/−0
• src/Rerefined/Refine/TH.hs +31/−0
• src/Rerefined/Refine/Unsafe.hs +33/−0
• src/Rerefined/Refined.hs +13/−0
• src/Rerefined/Refined1.hs +13/−0

@@ -0,0 +1,4 @@+## 0.1.0 (2024-04-30)+Initial release.++* rewrite of Nikita Volkov's refined library

@@ -0,0 +1,20 @@+Copyright (c) 2024 Ben Orchard (@raehik) <thefirstmuffinman@gmail.com>++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

@@ -0,0 +1,92 @@+# rerefined+[refined-nv-gh]:      https://github.com/nikita-volkov/refined+[refined-nv-hackage]: https://hackage.haskell.org/package/refined+[strongweak-hackage]: https://hackage.haskell.org/package/strongweak+[binrep-hackage]:     https://hackage.haskell.org/package/binrep+[refined1-hackage]:   https://hackage.haskell.org/package/refined1++Rewrite of Nikita Volkov's [refined][refined-nv-hackage] library.++* same concept+* same performance+* more instances+* better ergonomics (no insidious `Typeable` constraints)+* internals: fewer dependencies (no `aeson`), better errors, more concise++## Why?+I used the original [refined][refined-nv-hackage] library fairly extensively to+power other libraries (see [strongweak][strongweak-hackage],+[binrep][binrep-hackage]), though I moved to a fork [refined1][refined1-hackage]+some time ago to provide a feature I needed. I think the library has some flaws+and I want to contribute, but my tiny tweaks are still pending after a few+years. A good excuse to rewrite from the ground up.++All source code is original.++## Major changes from original refined+### Simplified errors+refined encoded the logical predicates in its error type. This doesn't enable+any further analysis, just turns a non-sum type into a sum type and complicates+consumption. Furthermore, this error type is first transformed into another+recursive ADT, which is then pretty printed. This is unnecessary (even mentioned+in the code).++rerefined has a single-constructor error type which can be easily and+efficiently turned into a `String` in a single pass.++### No insidious `Typeable` contexts+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!++### Cleaner design+What do `LessThan`, `GreaterThan`, `EqualTo` etc. have in common? They're all+relational binary operators where one value is a pre-filled `Natural`. rerefined+packs all of these into a single predicate that takes a type-level relational+operator. Only one instance for the same amount of code, and much easier to+reason about.++We take this even further and allow passing a type-level sign, to enable+comparing negative values.++We take this _even_ further and use the same relational operator definitions to+define length comparisons, where the other value is taken from the input's+length (rather than its numeric value). This does not take a sign, since length+must be non-negative.++### More instances+You know that length comparison predicate above? It has a _single instance_ for+each of `Refined1` and `Refined`:++```haskell+-- | 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+    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+    validate p = validateCompareLength p . olength+```++We get a ton more instances for a ton less code. (Note that mono-foldable has a+surprisingly small footprint, as most of its transitive dependencies are core+libraries.)++## License+Provided under the MIT license. See `LICENSE` for license text.

@@ -0,0 +1,66 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.35.2.+--+-- see: https://github.com/sol/hpack++name:           rerefined+version:        0.1.0+synopsis:       Refinement types, again+description:    Please see README.md.+category:       Types, Data+homepage:       https://github.com/raehik/rerefined#readme+bug-reports:    https://github.com/raehik/rerefined/issues+author:         Ben Orchard+maintainer:     Ben Orchard <thefirstmuffinman@gmail.com>+license:        MIT+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    CHANGELOG.md++source-repository head+  type: git+  location: https://github.com/raehik/rerefined++library+  exposed-modules:+      Rerefined.Predicate+      Rerefined.Predicate.Common+      Rerefined.Predicate.Fail+      Rerefined.Predicate.Logical+      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:+      src+  default-extensions:+      LambdaCase+      NoStarIsType+      DerivingVia+      DeriveAnyClass+      GADTs+      RoleAnnotations+      DefaultSignatures+      TypeFamilies+      DataKinds+      MagicHash+  ghc-options: -Wall -Wno-unticked-promoted-constructors+  build-depends:+      base >=4.16 && <5+    , mono-traversable >=1.0.17.0 && <1.1+    , template-haskell+    , typeably >=0.1.0 && <0.2+  default-language: GHC2021

@@ -0,0 +1,63 @@+-- | Base definitions for refinement predicates.++module Rerefined.Predicate+  ( Refine(validate)+  , Refine1(validate1)+  , RefineFailure(..)+  , Predicate(predicateName)+  ) where++import GHC.Exts ( Proxy# )+import Data.Typeable ( Typeable, typeRep )+import Data.Typeable.Typeably+import Data.Proxy ( Proxy(Proxy) )++-- | Types which define refinements on other types.+class Predicate p where+    -- | The predicate name, as a 'Show'-like (for good bracketing).+    --+    -- 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++-- | 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))++-- | 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)++-- | Refine functor type @f@ with functor predicate @p@.+--+-- By not making the contained type accessible, we ensure refinements apply+-- @forall a. f a@. That is, refinements here apply only to the functor+-- 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)++-- | 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.++  , refineFailureDetail    :: a+  -- ^ Failure clarification.++  , refineFailureInner     :: [RefineFailure a]+  -- ^ Any wrapped errors, for combinator predicates.+  --+  -- What these are, and their order, should be noted in 'refineFailureDetail'.+  }

@@ -0,0 +1,50 @@+{-# LANGUAGE AllowAmbiguousTypes #-}++-- | Handy utilities for defining predicates.++module Rerefined.Predicate.Common+  (+  -- * Re-exports+    module Rerefined.Predicate+  , Typeably(..), Typeable+  , proxy#++  -- * Predicate validation+  , validateFail, validateBool++  -- * Predicate name+  , predicateName1, predicateName2+  ) where++import Rerefined.Predicate+import GHC.Exts ( Proxy#, proxy# )+import Data.Typeable.Typeably+import Data.Typeable ( Typeable )++-- | 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++-- | Shortcut for simply validating a 'Bool'.+validateBool+    :: Predicate p => Proxy# p -> String -> Bool+    -> Maybe (RefineFailure String)+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,9 @@+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" []

@@ -0,0 +1,138 @@+{-# 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]++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    ]++data Not p++instance Predicate p => Predicate (Not p) where+    predicateName _ = predicateName1 @p "Not"++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" []++-- TODO principle of explosion? (p and not p -> anything)++-- 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,10 @@+module Rerefined.Predicate.Relational+  ( CompareValue+  , Sign(..)+  , RelOp(..)+  , CompareLength+  ) where++import Rerefined.Predicate.Relational.Internal+import Rerefined.Predicate.Relational.Value+import Rerefined.Predicate.Relational.Length

@@ -0,0 +1,75 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE UndecidableInstances #-} -- for weird TODO stuff++module Rerefined.Predicate.Relational.Internal where++import Data.Typeable ( Typeable )++import GHC.TypeNats+import Data.Type.Ord ( OrdCond )++-- | 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++-- | 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++    -- | Pretty operator.+    reifyRelOpPretty :: String++instance ReifyRelOp LT' where+    reifyRelOp = (<)+    reifyRelOpPretty = "<"++instance ReifyRelOp LTE where+    reifyRelOp = (<=)+    reifyRelOpPretty = "<="++instance ReifyRelOp EQ' where+    reifyRelOp = (==)+    reifyRelOpPretty = "=="++instance ReifyRelOp NEQ where+    reifyRelOp = (/=)+    reifyRelOpPretty = "/="++instance ReifyRelOp GTE where+    reifyRelOp = (>=)+    reifyRelOpPretty = ">="++instance ReifyRelOp GT' where+    reifyRelOp = (>)+    reifyRelOpPretty = ">"++-- | Can we widen the given 'RelOp' from @n@ to @m@?+type family WidenRelOp (op :: RelOp) (n :: Natural) (m :: Natural) 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 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++    -- can't widen (==) or (/=)+    WidenRelOp _   _ _ = False

@@ -0,0 +1,63 @@+module Rerefined.Predicate.Relational.Length where++import Rerefined.Predicate.Common+import Rerefined.Predicate.Relational.Internal+import GHC.TypeNats ( Natural, KnownNat, natVal' )+import Data.MonoTraversable ( MonoFoldable(olength) )+import GHC.Exts ( Proxy# )++import Rerefined.Refined+import Rerefined.Refine.Unsafe ( unsafeRerefine )+import GHC.TypeError+import Data.Kind ( type Constraint )++-- | Compare length to a type-level 'Natural' using the given 'RelOp'.+data CompareLength (op :: RelOp) (n :: Natural)+    deriving Predicate via Typeably (CompareLength op 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+    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+    validate p = validateCompareLength p . olength++validateCompareLength+    :: forall op n. (KnownNat n, ReifyRelOp op)+    => Proxy# (CompareLength op n) -> Int -> Maybe (RefineFailure String)+validateCompareLength p len =+    validateBool p ("length not "<>reifyRelOpPretty @op<>" "<>show n)+        (reifyRelOp @op len (fromIntegral n))+  where n = natVal' (proxy# @n)++-- | 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 @Refined (CompareLength GTE 1) a@ into a @Refined+-- (CompareLength GTE 0) a@.+--+-- TODO improve type error here+widenCompareLength+    :: forall m op n a+    .  WROE op n m+    => Refined (CompareLength op n) a+    -> Refined (CompareLength op m) a+widenCompareLength = unsafeRerefine++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+    WROE' op n m True  = ()+    WROE' op n m False = TypeError+      (      Text "can't widen relational equation "+        :$$: ShowType op :<>: Text " " :<>: ShowType n+        :$$: Text "to"+        :$$: ShowType op :<>: Text " " :<>: ShowType m+      )

@@ -0,0 +1,51 @@+{-# LANGUAGE AllowAmbiguousTypes #-}++module Rerefined.Predicate.Relational.Value where++import Rerefined.Predicate.Common+import Rerefined.Predicate.Relational.Internal+import GHC.TypeNats ( Natural, KnownNat, natVal' )++-- | 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))+-}++--type LessThan n = CompareValue LT' n++instance+  ( KnownNat n, Num a, Ord a+  , ReifyRelOp op, ReifySignedNat sign n, ReifySign sign+  ) => 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)+            (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 = "-"++-- TODO do I add any KnownNat constraints anywhere here+class ReifySignedNat (sign :: Sign) (n :: Natural) where+    reifySignedNat :: (Num a, KnownNat n) => a++instance ReifySignedNat Pos n where+    reifySignedNat = fromIntegral (natVal' (proxy# @n))++instance ReifySignedNat Neg n where+    reifySignedNat = negate (fromIntegral (natVal' (proxy# @n)))

@@ -0,0 +1,9 @@+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

@@ -0,0 +1,23 @@+-- | Predicate re-exports, for when you're heavily using refinement types.++module Rerefined.Predicates+  (+  -- * Base+    Succeed+  , Fail++  -- * Logical+  , Not+  , Logical++  -- * Relational+  , CompareValue+  , Sign(..)+  , RelOp(..)+  , CompareLength+  ) where++import Rerefined.Predicate.Succeed+import Rerefined.Predicate.Fail+import Rerefined.Predicate.Logical+import Rerefined.Predicate.Relational

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

@@ -0,0 +1,44 @@+{-# LANGUAGE OverloadedStrings, AllowAmbiguousTypes #-}++module Rerefined.Refine where++import Rerefined.Refined+import Rerefined.Refined1+import Rerefined.Predicate+import GHC.Exts ( proxy#, IsString )++-- | Refine @a@ with predicate @p@.+refine+    :: forall p a. Refine p a+    => a -> Either (RefineFailure String) (Refined p a)+refine a =+    case validate (proxy# @p) a of+      Nothing -> Right (Refined a)+      Just e  -> Left e++-- reifyPredicate is just a weaker version of validate without proxy.+-- Maybe the latter is useful, though...?++-- | Refine @f a@ with functor predicate @p@.+refine1+    :: forall p f a. Refine1 p f+    => f a -> Either (RefineFailure String) (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])+  where+    go n = \case+      []     -> ""+      (e:es) ->+           "\n" <> indent n     <> refineFailurePredicate e+        <> "\n" <> indent (n+2) <> refineFailureDetail    e+        <> go (n+2) (refineFailureInner e)+        <> go n es+    indent = \case+      0 -> ""+      n -> " " <> indent (n-1)

@@ -0,0 +1,31 @@+module Rerefined.Refine.TH+  ( refineTH+  , refine1TH+  ) where++import Rerefined.Refine+import Rerefined.Predicate+import Rerefined.Refined+import Rerefined.Refined1+import Language.Haskell.TH.Syntax qualified as TH++-- | Refine @a@ with predicate @p@ at compile time via Template Haskell.+refineTH+    :: forall p a m+    .  (Refine p a, TH.Lift a, TH.Quote m, MonadFail m)+    => a+    -> TH.Code m (Refined p a)+refineTH = either refineTHFail TH.liftTyped . refine @p @a++-- | Refine @f a@ with functor predicate @p@ at compile time via Template+--   Haskell.+refine1TH+    :: forall p f a m+    .  (Refine1 p f, TH.Lift (f a), TH.Quote m, MonadFail m)+    => f a+    -> TH.Code m (Refined1 p f a)+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

@@ -0,0 +1,33 @@+{- | Unsafe refining.++Sometimes, you know that your value satisfies some predicate before validating.+For those cases, we permit skipping validation and obtaining a refined value+"for free".++You should be certain that your value cannot possibly fail the predicate you are+skipping. A good practice is to annotate all call sites with an explanation of+why the usage is safe.+-}++module Rerefined.Refine.Unsafe where++import Rerefined.Refined+import Rerefined.Refined1++-- | Construct a 'Refined' without validating the predicate @p@.+--+-- Unsafe. Use only when you can manually prove that the predicate holds.+unsafeRefine :: a -> Refined p a+unsafeRefine = Refined++-- | Construct a 'Refined1' without validating the predicate @p@.+--+-- Unsafe. Use only when you can manually prove that the predicate holds.+unsafeRefine1 :: f a -> Refined1 p f a+unsafeRefine1 = Refined1++-- | Replace a 'Refined''s predicate without validating the new prdicate @pNew@.+--+-- Unsafe. Use only when you can manually prove that the new predicate holds.+unsafeRerefine :: forall pNew pOld a. Refined pOld a -> Refined pNew a+unsafeRerefine = Refined . unrefine

@@ -0,0 +1,13 @@+module Rerefined.Refined 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?++-- | 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

@@ -0,0 +1,13 @@+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 (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