{-# LANGUAGE UndecidableInstances #-}
module Data.Type.BitRecords.Assert
( type Assert, type Assertion, type Check
, type (?::)
, type (@&&)
, type NatLE
, type NatGE
, type NatIn
, type LengthIn
, type CountElementsForLengthIn
) where
import GHC.TypeLits
import Data.Kind (type Type)
import Data.Type.Bool
type (?::) x cond = Assert cond x
infixr 0 ?::
type family Assert (cond :: Assertion a) (x :: a) :: a where
Assert cond x = ProcessCheckResult (Check cond x) x
type Assertion a = TyFun a (Maybe ErrorMessage) -> Type
type family Check (f :: Assertion a) (x :: a) :: Maybe ErrorMessage
type family ProcessCheckResult (r :: Maybe ErrorMessage) (x :: a) :: a where
ProcessCheckResult 'Nothing x = x
ProcessCheckResult ('Just blah) x =
TypeError ('Text "Assertion on value " ':<>: 'ShowType x ':<>: 'Text " failed:" ':$$: blah)
data TyFun :: Type -> Type -> Type
data (@&&) :: Assertion a -> Assertion a -> Assertion a
type instance Check (a1 @&& a2) x =
(ProcessCheckResult (Check a2 x)
(ProcessCheckResult (Check a1 x) x))
data NatGE :: Nat -> Assertion Nat
type instance Check (NatGE n) x =
If (n <=? x) 'Nothing ('Just ( 'Text "Natural too small: " ':<>: 'ShowType x
':$$: 'Text "Required: >=" ':<>: 'ShowType n))
data NatLE :: Nat -> Assertion Nat
type instance Check (NatLE n) x =
If (x <=? n) 'Nothing ('Just ( 'Text "Natural too big: " ':<>: 'ShowType x
':$$: 'Text "Required: <=" ':<>: 'ShowType n))
data NatIn :: Nat -> Nat -> Assertion Nat
type instance Check (NatIn from to) n =
CheckNatInRange (n <=? to) (from <=? n) from to n
type family
CheckNatInRange
(lt :: Bool) (gt :: Bool) (from :: Nat) (to :: Nat) (n :: Nat) :: Maybe ErrorMessage where
CheckNatInRange 'True 'True from to x = 'Nothing
CheckNatInRange c1 c2 from to x =
'Just ('Text "Natural out of range: " ':<>: 'ShowType x
':<>: 'Text " not in "
':<>: 'ShowType from ':<>: 'Text " .. " ':<>: 'ShowType to)
data LengthIn :: Nat -> Nat -> Assertion a
type instance Check (LengthIn from to) xs = Check (NatIn from to) (CountElementsForLengthIn xs)
type family CountElementsForLengthIn (xs :: k) :: Nat
type instance CountElementsForLengthIn ('[]) = 0
type instance CountElementsForLengthIn (x ': xs) = 1 + CountElementsForLengthIn xs