Rerefined.Predicate.Relational.Length

Documentation

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

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

Instances

(KnownNat n, Foldable f, ReifyRelOp op) => Refine1 (CompareLength op n :: Type) (f :: Type -> Type)

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

Defined in Rerefined.Predicate.Relational.Length

Methods

validate1 :: forall (a :: k1). Proxy# (CompareLength op n) -> f a -> Maybe (RefineFailure String)

(Typeable op, KnownNat n) => Predicate (CompareLength op n :: Type)

Defined in Rerefined.Predicate.Relational.Length

Methods

predicateName :: Proxy# (CompareLength op n) -> Int -> ShowS

(KnownNat n, MonoFoldable a, ReifyRelOp op) => Refine (CompareLength op n :: Type) a

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

Defined in Rerefined.Predicate.Relational.Length

Methods

validate :: Proxy# (CompareLength op n) -> a -> Maybe (RefineFailure String)

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

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

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

type WROE op n m = WROE' op n m (WidenRelOp op n m)

type family WROE' (op :: RelOp) (n :: Natural) (m :: Natural) (b :: Bool) where ...

Equations

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))