Integral package:finite-typelits

This class asserts that the value of n is known at runtime, and that it is representable in type a (which should be a SaneIntegral). At runtime it acts like an implicit parameter of type a, much like KnownNat is an implicit parameter of type Integer.
A class of datatypes that faithfully represent a sub-range of Integer that includes 0. A valid instance must obey the following laws: fromInteger must be a retract of toInteger:
fromInteger (toInteger a) == a
Restricted to the range [0, Limit] (with Nothing understood as positive infinity), fromInteger must be an inverse of toInteger:
limited i ==> toInteger (fromInteger i) == i
where:
limited i = case limit of
Just l -> 0 <= i && i <= l
Nothing -> 0 <= i
WARNING: violating the above constraint in particular breaks type safety. The implementations of Ord, Enum, Num, Integral must be compatible with that of Integer, whenever all arguments and results fall within [0, Limit], for example:
limited i && limited j && limited k && (i * j == k) ==> (fromInteger i * fromInteger j == fromInteger k)
Methods modAdd, modSub, and modMul implement modular addition, multiplication, and subtraction. The default implementation is via Integer, but a faster implementation can be provided instead. If provided, the implementation must be correct for moduli in range [1, Limit]. WARNING: a naive implementaton is prone to arithmetic overflow and may produce invalid results for moduli close to Limit.
Recover a KnownNat constraint from a KnownIntegral constraint.