-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Integer singletons with flexible representation
--   
--   This provides singletons-style witnesses for type-level integers, and
--   some limited arithmetic operations on them. Instead of working with
--   (invisible, implicitly-passed) <a>KnownNat</a> instances, you can work
--   with (visible, explicitly-mentioned) <a>SNumber</a> values, and can
--   freely convert between the two forms.
--   
--   This primarily exists in support of <a>dependent-literals-plugin</a>.
@package snumber
@version 0.2.0


-- | Runtime witnesses of type-level integers.
module Data.SNumber

-- | <tt>SNumber a n</tt> is a runtime representation of the value of
--   <tt>n</tt>.
--   
--   For <tt>N# n :: SNumber a n</tt> and <tt>N# m :: SNumber a m</tt>, the
--   following must hold:
--   
--   <ul>
--   <li><tt>n ~ m</tt> iff <tt>n == m</tt> (according to the <a>Eq</a>
--   instance of <tt>a</tt>).</li>
--   <li><tt>CmpInteger m n ~ 'LT</tt> iff <tt>compare m n == LT</tt>
--   (according to <a>Ord</a>).</li>
--   <li><tt>CmpInteger m n ~ 'EQ</tt> iff <tt>compare m n == EQ</tt>.</li>
--   <li><tt>CmpInteger m n ~ 'GT</tt> iff <tt>compare m n == GT</tt>.</li>
--   <li><pre>toInteger n == integerVal @n</pre></li>
--   </ul>
--   
--   These are exactly the set of things we're willing to
--   <a>unsafeCoerce</a> proofs for. It is <i>unsafe</i> to construct an
--   <a>SNumber</a> that violates these by any means.
--   
--   Note that the first requirement means that you must never construct
--   <tt>N# 0 :: SNumber _ ('Neg 0)</tt>, because that would prove that
--   <tt>'Neg 0 ~ 'Pos 0</tt>. In practice, we largely ignore the existence
--   of <tt>'Neg 0</tt>: <a>trySNumber</a> (and, by extension, the instance
--   derivation via <a>KnownInteger</a>) will throw a runtime error when
--   trying to construct <tt>'Neg 0</tt>, and <a>SafeSNumber</a> instances
--   explicitly exclude <tt>'Neg 0</tt> with type-level checks.
--   
--   There are six main ways to introduce an <a>SNumber</a>, from the
--   cartesian product of several choices
--   
--   <ul>
--   <li>How do you validate that the value is in-bounds for the
--   representation type?<ul><li>If by runtime checks, the function name
--   has a "try" infix.</li><li>If by trusting the caller blindly, the
--   function name has an "unsafe" prefix and an "Unchecked"
--   infix.</li><li>If by type-level bounds checks, the function name has
--   neither of these.</li></ul></li>
--   <li>How do you validate that the runtime Integer value matches the
--   type-level Integer?<ul><li>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 <a>SNumber</a> from a runtime value rather than
--   deriving it from KnownNat.</li><li>If by getting it from a KnownNat
--   instance, the function name doesn't have that infix.</li></ul></li>
--   </ul>
--   
--   Thus:
--   
--   <ul>
--   <li><a>snumber</a>: type-level checks, safe <tt>KnownNat</tt>.</li>
--   <li><a>trySNumber</a>: runtime checks, safe <tt>KnownNat</tt>.</li>
--   <li><a>unsafeUncheckedSNumber</a>: no checks, safe
--   <tt>KnownNat</tt>.</li>
--   <li><a>unsafeMkSNumber</a>: type-level checks, unsafe <tt>Integer</tt>
--   parameter.</li>
--   <li><a>unsafeTryMkSNumber</a>: runtime checks, unsafe <tt>Integer</tt>
--   parameter.</li>
--   <li><a>unsafeUncheckedMkSNumber</a>: no checks, unsafe <tt>a</tt>
--   parameter. a.k.a. <a>N#</a>.</li>
--   </ul>
--   
--   Finally, there's one other way to get an <a>SNumber</a>: by asking the
--   constraint solver to give you one, with a <a>KnownSNumber</a> class
--   and its <a>snumberVal</a> method. Currently, this will be solved
--   automatically from <a>KnownNat</a> by using <a>trySNumber</a>, and of
--   course it can be solved from a matching instance in the function's
--   context (which compiles to an <tt>a</tt> parameter for
--   <tt>KnownSNumber a n</tt>).
data SNumber a (n :: Integer)

-- | Treat <a>SNumber</a> as if it were a GADT containing a
--   <a>KnownSNumber</a> instance.
pattern SNumber :: forall (n :: Integer) a. SNumberRepr a => KnownSNumber a n => SNumber a n

-- | Create an <a>SNumber</a> for <tt>n</tt>, with no safety measures
--   whatsoever.
--   
--   This pattern is identical to the newtype constructor of <a>SNumber</a>
--   except that it isn't actualy a newtype constructor, so having it in
--   scope doesn't allow unsound coercions across <a>SNumber</a> types.
pattern N# :: forall (n :: Integer) a. a -> SNumber a n

-- | A unidirectional pattern for matching <a>SNumber</a>s.
--   
--   This allows the pseudo-field-selector <a>unSNumber</a> to be exported
--   bundled with <a>SNumber</a>, so it can be imported by
--   <tt>SNumber(..)</tt> as if it were a normal field selector of a record
--   definition. If this were done as part of <a>N#</a>, it'd allow
--   unsafely changing an <a>SNumber</a>'s representation without using any
--   identifiers that indicate unsafety, by way of record update syntax.
pattern SN :: forall (n :: Integer) a. a -> SNumber a n

-- | The 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 <a>Integral</a>, <a>Ord</a>, and <a>Eq</a> instances
--   uphold the requirements of <a>SNumber</a>, for any integer <tt>n</tt>
--   that satisfies <tt>SafeSNumber a n</tt>.
--   
--   Furthermore, it requires that every value of <tt>a</tt> is an integer,
--   i.e. that <tt>forall x :: a. exists y :: Integer. x == fromInteger y,
--   toInteger x == y</tt>. This ensures we can wrap any <tt>a</tt> in
--   <tt>SomeSNumberVal</tt> and be sure it corresponds to a valid
--   <tt>K.Integer</tt>.
class Integral a => SNumberRepr a where {
    
    -- | <tt>SafeSNumber a n</tt> witnesses that <tt><a>N#</a> n</tt> is a
    --   valid <tt><a>SNumber</a> a n</tt>.
    type family SafeSNumber a :: Integer -> Constraint;
}

-- | Construct an <a>SNumber</a>, doing all validation at the type level.
--   
--   This is completely safe and cannot raise runtime errors.
snumber :: forall n a. (SNumberRepr a, SafeSNumber a n, KnownInteger n) => SNumber a n

-- | Create an <a>SNumber</a> for <tt>n</tt>, if it's faithfully
--   represented by <tt>a</tt>.
--   
--   This is completely safe, but it may raise runtime errors, because it
--   tests at runtime whether <tt>a</tt> can represent <tt>n</tt>
--   correctly.
trySNumber :: forall n a. (SNumberRepr a, KnownInteger n) => Maybe (SNumber a n)

-- | Create an <a>SNumber</a> from a <a>KnownInteger</a> constraint without
--   any checks.
--   
--   This will cause type unsoundness if the value is not correctly
--   represented by <tt>a</tt> or if the instances of <tt>a</tt> do not
--   behave according to the safety requirements described on
--   <a>SNumber</a>.
unsafeUncheckedSNumber :: forall n a. (Num a, KnownInteger n) => SNumber a n

-- | Semi-safely construct an <a>SNumber</a> as if by <a>N#</a>.
--   
--   Callers must ensure that the <tt>a</tt> argument is <tt>fromInteger
--   (integerVal </tt>n)<tt> (semantically, not syntactically:
--   </tt>unsafeSNumber <tt>('Pos 42) 42</tt> is fine and is in fact the
--   intended use case).
--   
--   The extra constraint here compared to <a>N#</a> ensures that if you
--   write <tt>unsafeMkSNumber @n (fromInteger n)</tt>, the result is
--   either a valid <a>SNumber</a> or a type error. In particular, the
--   cases this rules out are those where <tt>toInteger (fromInteger n ::
--   a) /= n</tt> or where <tt>fromInteger m :: a == fromInteger n</tt>
--   does not imply <tt>m == n</tt>.
unsafeMkSNumber :: forall n a. SafeSNumber a n => a -> SNumber a n

-- | Create an <a>SNumber</a> for <tt>n</tt>, if it's faithfully
--   represented by <tt>a</tt>.
--   
--   As with <a>unsafeMkSNumber</a>, this trusts you to pass <tt>integerVal
--   @n</tt>, and violating that will lead to type unsoundness.
--   
--   This tests at runtime whether <tt>a</tt> represents <tt>n</tt>
--   correctly.
unsafeTryMkSNumber :: forall n a. SNumberRepr a => Integer -> Maybe (SNumber a n)

-- | Create an <a>SNumber</a> for <tt>n</tt>, with no safety measures
--   whatsoever.
unsafeUncheckedMkSNumber :: forall n a. a -> SNumber a n

-- | An <a>SNumber</a> with an existential <a>Integer</a> type parameter.
data SomeSNumber a
SomeSNumber :: SNumber a n -> SomeSNumber a

-- | Create an <tt><a>SNumber</a> a</tt> from any value of type <tt>a</tt>.
--   
--   Since <a>SNumberRepr</a> guarantees every <tt>a</tt> value is an
--   integer, we can freely wrap up a value in an <a>SNumber</a> with
--   existential <a>Integer</a> type parameter.
someSNumberVal :: SNumberRepr a => a -> SomeSNumber a

-- | Like <a>someSNumberVal</a>, but in quantified CPS style rather than
--   GADT style.
withSNumber :: SNumberRepr a => a -> (forall n. SNumber a n -> r) -> r

-- | Ordering results carrying evidence of type-level ordering relations.
data SOrdering m n
[SLT] :: CmpInteger m n ~ 'LT => SOrdering m n

-- | This doesn't currently prove m ~ n, but since we've forbidden SNumbers
--   of <tt>'Neg 0</tt>, it probably could.
[SEQ] :: CmpInteger m n ~ 'EQ => SOrdering m n
[SGT] :: CmpInteger m n ~ 'GT => SOrdering m n

-- | Compare two type-level <a>Integer</a>s using their runtime witnesses.
compareSNumber :: forall m n a. Ord a => SNumber a m -> SNumber a n -> SOrdering m n

-- | Test equality of two type-level <a>Integer</a>s using their runtime
--   witnesses.
sameSNumber :: Eq a => SNumber a m -> SNumber a n -> Maybe (m :~: n)

-- | Arithmetic ops with overflow detection.
--   
--   Laws:
--   
--   <ul>
--   <li><pre>overflowAdd x y = (False, xy) =&gt; toInteger xy ===
--   toInteger x + toInteger y</pre></li>
--   <li><pre>overflowSub x y = (False, xy) =&gt; toInteger xy ===
--   toInteger x - toInteger y</pre></li>
--   <li><pre>overflowMul x y = (False, xy) =&gt; toInteger xy ===
--   toInteger x * toInteger y</pre></li>
--   </ul>
--   
--   This is used for arithmetic on <a>SNumber</a> runtime values, so
--   creating incorrect instances is type-unsafe.
class Integral a => OverflowArith a
overflowAdd :: OverflowArith a => a -> a -> (Bool, a)
overflowSub :: OverflowArith a => a -> a -> (Bool, a)
overflowMul :: OverflowArith a => a -> a -> (Bool, a)

-- | Compute a runtime witness of <tt>m + n</tt>, or <a>Nothing</a>.
tryAdd :: (SNumberRepr a, OverflowArith a) => SNumber a m -> SNumber a n -> Maybe (SNumber a (m + n))

-- | Compute a runtime witness of <tt>m - n</tt>, or <a>Nothing</a>.
trySub :: (SNumberRepr a, OverflowArith a) => SNumber a m -> SNumber a n -> Maybe (SNumber a (m - n))

-- | Compute a runtime witness of <tt>m * n</tt>, or <a>Nothing</a>.
tryMul :: (SNumberRepr a, OverflowArith a) => SNumber a m -> SNumber a n -> Maybe (SNumber a (m * n))
data UnrepresentableSNumber
UnrepresentableSNumber :: String -> Integer -> Integer -> UnrepresentableSNumber

-- | Compute a runtime witness of <tt>m + n</tt>, or throw.
chkAdd :: (SNumberRepr a, OverflowArith a, HasCallStack) => SNumber a m -> SNumber a n -> SNumber a (m + n)

-- | Compute a runtime witness of <tt>m - n</tt>, or throw.
chkSub :: (SNumberRepr a, OverflowArith a, HasCallStack) => SNumber a m -> SNumber a n -> SNumber a (m - n)

-- | Compute a runtime witness of <tt>m * n</tt>, or throw.
chkMul :: (SNumberRepr a, OverflowArith a, HasCallStack) => SNumber a m -> SNumber a n -> SNumber a (m * n)

-- | Compute a runtime witness of exact division.
--   
--   We could provide division in terms of <a>Div</a> instead, but
--   <a>Kinds.Integer</a> doesn't currently have division.
divExact :: SNumberRepr a => SNumber a (m * n) -> SNumber a n -> SNumber a m

-- | Like <a>KnownNat</a>, but represented by <tt>a</tt> instead of
--   <a>Natural</a>.
--   
--   This is currently solved automatically from <a>KnownNat</a> via
--   runtime checks, to ease migration (we can incrementally strengthen
--   <a>KnownNat</a> constraints to <a>KnownSNumber</a> constraints), but
--   in the future it may be changed to use <a>SafeSNumber</a>, which will
--   rule out runtime failures but will require additional proofs in order
--   to solve via <a>KnownNat</a>. For statically known <a>Integer</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 <a>SNumber</a>
--   explicitly.
class KnownSNumber a n

-- | Implementation of <a>snumberVal</a>.
--   
--   This has an inconvenient type variable order because it derives from
--   the order they appear in the class head.
snumberVal_ :: KnownSNumber a n => SNumber a n

-- | Implementation of <a>snumberVal</a>.
--   
--   This has an inconvenient type variable order because it derives from
--   the order they appear in the class head.
snumberVal_ :: (KnownSNumber a n, SNumberRepr a, KnownInteger n) => SNumber a n

-- | Get an <a>SNumber</a> out of the context from <a>KnownSNumber</a> or
--   <a>KnownNat</a>.
--   
--   This has the number as its first type parameter, for TypeApplications
--   convenience.
snumberVal :: forall n a. KnownSNumber a n => SNumber a n

-- | Stash an <a>SNumber</a> at the type level as a <a>KnownSNumber</a>
--   instance.
reifySNumber :: forall a n r. SNumber a n -> (KnownSNumber a n => r) -> r

-- | Use a positive <a>SNumber</a> to introduce a <a>KnownNat</a> instance.
reifySNumberAsNat :: forall n r a. Integral a => SNumber a ('Pos n) -> (KnownNat n => r) -> r

-- | The number of bits in the present system's <a>Int</a> type.
type IntBits = 64

-- | The smallest representable <a>Int</a> value.
type IntMin = 'Neg (2 ^ (IntBits - 1))

-- | One more than the largest representable <a>Int</a> value.
type IntMaxP1 = 'Pos (2 ^ (IntBits - 1))

-- | The number of bits in the present system's <a>Word</a> type.
type WordBits = 64

-- | One more than the largest representable <a>Word</a> value.
type WordMaxP1 = 'Pos (2 ^ WordBits)
instance GHC.Show.Show a => GHC.Show.Show (Data.SNumber.SNumber a n)
instance GHC.Show.Show Data.SNumber.UnrepresentableSNumber
instance GHC.Exception.Type.Exception Data.SNumber.UnrepresentableSNumber
instance Data.SNumber.OverflowArith GHC.Types.Word
instance Data.SNumber.OverflowArith GHC.Types.Int
instance Data.SNumber.OverflowArith GHC.Natural.Natural
instance Data.SNumber.OverflowArith GHC.Integer.Type.Integer
instance (Data.SNumber.SNumberRepr a, Kinds.Integer.KnownInteger n) => Data.SNumber.KnownSNumber a n
instance Data.SNumber.SNumberRepr GHC.Types.Int
instance Data.SNumber.SNumberRepr GHC.Types.Word
instance Data.SNumber.SNumberRepr GHC.Integer.Type.Integer
instance Data.SNumber.SNumberRepr GHC.Natural.Natural
instance (Data.SNumber.Internal.IsAtLeastMinBound ('Kinds.Integer.Neg (2 GHC.TypeNats.^ (w Kinds.Num.- 1))) (Data.SNumber.SignedReprRangeErr w repr a) n, Data.SNumber.Internal.IsLessThanMaxBound ('Kinds.Integer.Pos (2 GHC.TypeNats.^ (w Kinds.Num.- 1))) (Data.SNumber.SignedReprRangeErr w repr a) n, Data.SNumber.Internal.ForbidNegZero n) => Data.SNumber.LitIsSignedBits w repr a n
instance (Data.SNumber.Internal.IsAtLeastMinBound ('Kinds.Integer.Pos 0) (Data.SNumber.Internal.NegativeReprUnsignedErr repr a) n, Data.SNumber.Internal.IsLessThanMaxBound ('Kinds.Integer.Pos (2 GHC.TypeNats.^ w)) (Data.SNumber.Internal.OutOfReprRangeErr ('Kinds.Integer.Pos 0) ('Kinds.Integer.Pos (2 GHC.TypeNats.^ w)) repr a) n, Data.SNumber.Internal.ForbidNegZero n) => Data.SNumber.LitIsUnsignedBits w repr a n
instance Data.SNumber.Internal.ForbidNegZero n => Data.SNumber.LitIsAnything n