h$%$,9      !"#$%&'()*+,-./012345678None ./> 9:;<=None&'(-/9<>?#$snumber&An exception for overflows in checked  arithmetic.snumber'Arithmetic ops with overflow detection.Laws: overflowAdd x y = (False, xy) => toInteger xy === toInteger x + toInteger y overflowSub x y = (False, xy) => toInteger xy === toInteger x - toInteger y overflowMul x y = (False, xy) => toInteger xy === toInteger x * toInteger yThis is used for arithmetic on  runtime values, so creating incorrect instances is type-unsafe.snumberAn  with an existential > type parameter.snumberLike ?, but represented by a instead of @.,This is currently solved automatically from ? via runtime checks, to ease migration (we can incrementally strengthen ? constraints to ; constraints), but in the future it may be changed to use  , which will rule out runtime failures but will require additional proofs in order to solve via ?. For statically known A+s, these proofs will be entirely automatic.This class is meant to be used primarily in instance contexts; for standalone functions, it's probably better to pass an  explicitly. snumberImplementation of .This has an inconvenient type variable order because it derives from the order they appear in the class head; see . snumberThe class of types that are suitable for use as integer value witnesses.Implementing an instance of this class amounts to asserting that the type and its B, C, and D' instances uphold the requirements of , for any integer n that satisfies SafeSNumber a n.-Furthermore, it requires that every value of a is an integer, i.e. that forall x :: a. exists y :: Integer. x == fromInteger y, toInteger x == y . This ensures we can wrap any a in SomeSNumberVal( and be sure it corresponds to a valid  K.Integer. snumberSafeSNumber a n witnesses that  n is a valid  a n. snumber(One more than the largest representable E value. snumberThe smallest representable E value.snumber+The number of bits in the present system's E type.snumber(One more than the largest representable F value.snumber+The number of bits in the present system's F type.snumber SNumber a n- is a runtime representation of the value of n.For N# n :: SNumber a n and N# m :: SNumber a m, the following must hold:n ~ m iff n == m (according to the D instance of a).CmpInteger m n ~ 'LT iff compare m n == LT (according to C).CmpInteger m n ~ 'EQ iff compare m n == EQ.CmpInteger m n ~ 'GT iff compare m n == GT.toInteger n == integerVal @n.a upholds the C laws.5These are exactly the set of things we're willing to G proofs for. It is unsafe to construct an # that violates these by any means.Note that the first requirement means that you must never construct N# 0 :: SNumber _ ('Neg 0)!, because that would prove that 'Neg 0 ~ 'Pos 04. In practice, we largely ignore the existence of 'Neg 0: 2 (and, by extension, the instance derivation via H7) will throw a runtime error when trying to construct 'Neg 0, and   instances explicitly exclude 'Neg 0 with type-level checks.(There are six main ways to introduce an 0, from the cartesian product of several choicesHow do you validate that the value is in-bounds for the representation type?:If by runtime checks, the function name has a "try" infix.If by trusting the caller blindly, the function name has an "unsafe" prefix and an "Unchecked" infix.If by type-level bounds checks, the function name has neither of these.How do you validate that the runtime Integer value matches the type-level Integer?If by trusting the user to pass in the right Integer, the function has an "unsafe" prefix and a "Mk" infix: we're "making" the > from a runtime value rather than deriving it from KnownNat.If by getting it from a KnownNat instance, the function name doesn't have that infix.Thus:: type-level checks, safe KnownNat.: runtime checks, safe KnownNat.: no checks, safe KnownNat.: type-level checks, unsafe Integer parameter.: runtime checks, unsafe Integer parameter.: no checks, unsafe a parameter. a.k.a. .)Finally, there's one other way to get an ;: by asking the constraint solver to give you one, with a  class and its = method. Currently, this will be solved automatically from ? by using , and of course it can be solved from a matching instance in the function's context (which compiles to an a parameter for KnownSNumber a n).snumberTreat # as if it were a GADT containing a  instance.snumber&A unidirectional pattern for matching s.&This allows the pseudo-field-selector  to be exported bundled with , so it can be imported by  SNumber(..) as if it were a normal field selector of a record definition. If this were done as part of ", it'd allow unsafely changing an 's representation without using any identifiers that indicate unsafety, by way of record update syntax.snumber Create an  for n%, with no safety measures whatsoever.8This pattern is identical to the newtype constructor of  except that it isn't actualy a newtype constructor, so having it in scope doesn't allow unsound coercions across  types.snumber Construct an ), doing all validation at the type level.8This is completely safe and cannot raise runtime errors.snumber Create an  for n$, if it's faithfully represented by a.This is completely safe, but it may raise runtime errors, because it tests at runtime whether a can represent n correctly.snumber Create an  from a H constraint without any checks.This will cause type unsoundness if the value is not correctly represented by a or if the instances of a do not behave according to the safety requirements described on .snumberSemi-safely construct an  as if by .Callers must ensure that the a argument is fromInteger (integerVal n)$ (semantically, not syntactically: unsafeSNumber  ('Pos 42) 420 is fine and is in fact the intended use case).&The extra constraint here compared to  ensures that if you write "unsafeMkSNumber @n (fromInteger n) , the result is either a valid  or a type error. In particular, the cases this rules out are those where #toInteger (fromInteger n :: a) /= n or where #fromInteger m :: a == fromInteger n does not imply m == n.snumber Create an  for n$, if it's faithfully represented by a.As with , this trusts you to pass  integerVal @n4, and violating that will lead to type unsoundness.This tests at runtime whether a represents n correctly.snumber Create an  for n%, with no safety measures whatsoever.snumberGet an  out of the context from  or ?.This has the number as its first type parameter, for TypeApplications convenience.snumberCompare two type-level A s using their runtime witnesses.snumber Test equality of two type-level A s using their runtime witnesses.snumber Stash an  at the type level as a  instance. snumberUse a positive  to introduce a ? instance.!snumber Create an  a from any value of type a.Since   guarantees every a; value is an integer, we can freely wrap up a value in an  with existential > type parameter."snumberLike !5, but in quantified CPS style rather than GADT style.#snumberCompute a runtime witness of m + n, or I.$snumberCompute a runtime witness of m - n, or I.%snumberCompute a runtime witness of m * n, or I.&snumberCompute a runtime witness of m + n , or throw.'snumberCompute a runtime witness of m - n , or throw.(snumberCompute a runtime witness of m * n , or throw.)snumber,Compute a runtime witness of exact division.&We could provide division in terms of  instead, but  Kinds.Integer! doesn't currently have division.*  !"#$%&'()- !"#$%&'()          !"#$%&'()*+,-./0123456789:;<=>?@ABCDCEFGHBCIJKLMKLNKOPKOQCRS@ATCUV$snumber-0.3.0-CU452RBLmquDM3Nl0is4ZC Data.SNumberData.SNumber.Internal GHC.TypeNatsDivUnrepresentableSNumber OverflowArith overflowAdd overflowSub overflowMul SomeSNumber KnownSNumber snumberVal_ SNumberRepr SafeSNumberIntMaxP1IntMinIntBits WordMaxP1WordBitsSNumberSN unSNumberN#snumber trySNumberunsafeUncheckedSNumberunsafeMkSNumberunsafeTryMkSNumberunsafeUncheckedMkSNumber snumberValcompareSNumber sameSNumber reifySNumberreifySNumberAsNatsomeSNumberVal withSNumbertryAddtrySubtryMulchkAddchkSubchkMuldivExact$fLitIsAnythingn$fLitIsUnsignedBitswrepran$fLitIsSignedBitswrepran$fSNumberReprNatural$fSNumberReprInteger$fSNumberReprWord$fSNumberReprInt$fKnownSNumberan$fOverflowArithInteger$fOverflowArithNatural$fOverflowArithInt$fOverflowArithWord!$fExceptionUnrepresentableSNumber$fShowUnrepresentableSNumber $fShowSNumber ForbidNegZeroIsAtLeastMinBoundIsLessThanMaxBoundOutOfReprRangeErrNegativeReprUnsignedErr*numeric-kinds-0.2.0-2yQHYXCEVnBD7f0Jssg8X2 Kinds.IntegerIntegerbaseKnownNat GHC.NaturalNaturalinteger-wired-inGHC.Integer.TypeGHC.RealIntegralghc-prim GHC.ClassesOrdEq GHC.TypesIntWord Unsafe.Coerce unsafeCoerce KnownInteger GHC.MaybeNothing