Safe Haskell	None
Language	GHC2021

Rerefined.Predicate.Relational.Length

Synopsis

data CompareLength (op :: RelOp) (n :: Natural)
validateCompareLength :: forall (op :: RelOp) (n :: Nat). (KnownNat n, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Proxy# (CompareLength op n) -> Int -> Maybe RefineFailure
widenCompareLength :: forall (m :: Natural) (op :: RelOp) (n :: Natural) a. WROE op n m => Refined (CompareLength op n) a -> Refined (CompareLength op m) a
widenCompareLength1 :: forall {k1} (m :: Natural) (op :: RelOp) (n :: Natural) (f :: k1 -> Type) (a :: k1). WROE op n m => Refined1 (CompareLength op n) f a -> Refined1 (CompareLength op m) f a
type WROE (op :: RelOp) (n :: Natural) (m :: Natural) = WROE' op n m (WidenRelOp op n m)
type family WROE' (op :: k) (n :: Natural) (m :: Natural) (b :: Bool) where ...

Documentation

data CompareLength (op :: RelOp) (n :: Natural) Source #

Compare length to a type-level Natural using the given RelOp.

Instances

Instances details

(KnownNat n, Foldable f, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Refine1 (CompareLength op n :: Type) (f :: Type -> Type) Source #	Compare the length of a `Foldable` to a type-level `Natural` using the given `RelOp`.
Instance details Defined in Rerefined.Predicate.Relational.Length Methods validate1 :: Proxy# (CompareLength op n) -> f a -> Maybe RefineFailure Source #
Predicate (CompareLength op n :: Type) Source #	Precedence of 4 (matching base relational operators e.g. `>=`).
Instance details Defined in Rerefined.Predicate.Relational.Length
(KnownNat n, MonoFoldable a, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Refine (CompareLength op n :: Type) a Source #	Compare the length of a `MonoFoldable` to a type-level `Natural` using the given `RelOp`.
Instance details Defined in Rerefined.Predicate.Relational.Length Methods validate :: Proxy# (CompareLength op n) -> a -> Maybe RefineFailure Source #
type PredicateName d (CompareLength op n :: Type) Source #
Instance details Defined in Rerefined.Predicate.Relational.Length type PredicateName d (CompareLength op n :: Type) = ShowParen (d > 4) ((("Length " ++ ShowRelOp op) ++ ShowChar ' ') ++ ShowNatDec n)

validateCompareLength :: forall (op :: RelOp) (n :: Nat). (KnownNat n, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Proxy# (CompareLength op n) -> Int -> Maybe RefineFailure Source #

widenCompareLength :: forall (m :: Natural) (op :: RelOp) (n :: Natural) a. WROE op n m => Refined (CompareLength op n) a -> Refined (CompareLength op m) a Source #

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

widenCompareLength1 :: forall {k1} (m :: Natural) (op :: RelOp) (n :: Natural) (f :: k1 -> Type) (a :: k1). WROE op n m => Refined1 (CompareLength op n) f a -> Refined1 (CompareLength op m) f a Source #

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

type WROE (op :: RelOp) (n :: Natural) (m :: Natural) = WROE' op n m (WidenRelOp op n m) Source #

type family WROE' (op :: k) (n :: Natural) (m :: Natural) (b :: Bool) where ... Source #

Equations

WROE' (op :: k) n m 'True = ()
WROE' (op :: t) n m 'False = TypeError ((('Text "can't widen relational equation " ':$$: (('ShowType op ':<>: 'Text " ") ':<>: 'ShowType n)) ':$$: 'Text "to") ':$$: (('ShowType op ':<>: 'Text " ") ':<>: 'ShowType m)) :: Constraint