DependentLiterals.Bounds

Bounds Checks

Error Messages

type OutOfRangeMsg min maxp1 a n = (('Text "Literal out of range " :<>: ShowRange min maxp1) :<>: 'Text ":") :$$: ('Text " " :<>: ShowTypedNum a n)

Error Message Utilities

type ShowTypedNum a n = (ShowNum n :<>: 'Text " :: ") :<>: 'ShowType a

type ShowRange min maxp1 = ((('Text "(" :<>: ShowNum min) :<>: 'Text "..") :<>: ShowNum (maxp1 - 'Pos 1)) :<>: 'Text ")"

Error Constraints

class OutOfRangeErr (min :: Integer) (maxp1 :: Integer) (a :: Type) (n :: Integer)

Instances

(TypeError (OutOfRangeMsg min maxp1 a n) :: Constraint) => OutOfRangeErr min maxp1 a n

Defined in DependentLiterals.Bounds

Inequality Assertions

class n < maxp1 => CheckLessThanMaxBound (msg :: ErrorMessage) (maxp1 :: Integer) (a :: Type) (n :: Integer)

Instances

AssertNotApart msg (n <? maxp1) 'True => CheckLessThanMaxBound msg maxp1 a n

Defined in DependentLiterals.Bounds

class n >= min => CheckAtLeastMinBound (msg :: ErrorMessage) (min :: Integer) (a :: Type) (n :: Integer)

Instances

AssertNotApart msg (n >=? min) 'True => CheckAtLeastMinBound msg min a n

Defined in DependentLiterals.Bounds

class a ~ b => AssertEq (c :: Constraint) a b

Instances

AssertEq c (a :: k) (a :: k)

Defined in DependentLiterals.Bounds

type AssertNotApart msg a b = AssertNotApart_ msg (Eql a b) a b

Implementation Details

type family ShowNum (n :: Integer) where ...

Equations

ShowNum ('Pos n) = 'ShowType n

ShowNum ('Neg n) = 'Text "-" :<>: 'ShowType n

class a ~ b => AssertNotApart_ (msg :: ErrorMessage) eq a b

Instances

FailedToProveEq (TypeError msg :: Constraint) a b => AssertNotApart_ msg 'False (a :: k) (b :: k)

Defined in DependentLiterals.Bounds

a ~ b => AssertNotApart_ msg 'True (a :: k) (b :: k)

Defined in DependentLiterals.Bounds

type family Eql a b :: Bool where ...

Equations

Eql a a = 'True

Eql a b = 'False

class a ~ b => FailedToProveEq (err :: Constraint) a b

If you tried to prove a constraint and failed, and want to issue a custom error message for it explicitly, write something like this.

Given "class _c => FailedToProveC (err :: Constraint) ...", "FailedToProveC (TypeError ...)" is a constraint that pretends to prove c but instead throws a type error.