{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Refined.Length where
import Refined (Predicate(..))
import Refined (EqualTo)
import Refined.LessThanEq (LessThanEq)
import Data.CharLength (CharLength(..))
import GHC.TypeLits (Nat)
-- | The length of an input
data Length p
instance (CharLength x, Predicate p Int) => Predicate (Length p) x where
validate _ x =
showString "Length of string: " <$>
validate (undefined :: p) (charLength x)
type LengthEq (n :: Nat) =
Length (EqualTo n)
type LengthMax (n :: Nat) =
Length (LessThanEq n)