dependent-literals-0.1.1.0: Provides library support for pseudo-dependently-typed int literals.
Safe HaskellNone
LanguageHaskell2010

DependentLiterals.Bounds

Synopsis

Bounds Checks

Error Messages

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

Error Message Utilities

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

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

Error Constraints

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

Instances

Instances details
(TypeError (OutOfRangeMsg min maxp1 a n) :: Constraint) => OutOfRangeErr min maxp1 a n Source # 
Instance details

Defined in DependentLiterals.Bounds

Inequality Assertions

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

Instances

Instances details
AssertNotApart msg (Cmp n maxp1) 'LT => CheckLessThanMaxBound msg maxp1 a n Source # 
Instance details

Defined in DependentLiterals.Bounds

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

Instances

Instances details
AssertNotApart msg (n >=? min) 'True => CheckAtLeastMinBound msg min a n Source # 
Instance details

Defined in DependentLiterals.Bounds

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

Instances

Instances details
AssertEq c (a :: k) (a :: k) Source # 
Instance details

Defined in DependentLiterals.Bounds

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

Implementation Details

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

Equations

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

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

Instances

Instances details
FailedToProveEq (TypeError msg :: Constraint) a b => AssertNotApart_ msg 'False (a :: k) (b :: k) Source # 
Instance details

Defined in DependentLiterals.Bounds

a ~ b => AssertNotApart_ msg 'True (a :: k) (b :: k) Source # 
Instance details

Defined in DependentLiterals.Bounds

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

Equations

Eql a a = 'True 
Eql a b = 'False 

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

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.