DependentLiterals

Top-level module exporting the key DependentLiterals functionality.

Int Literals

class HasIntLiterals a

The main class providing dependent-literals functionality.

Instances of this can have integral literals and numeric patterns with -fplugin=DependentLiterals.Plugin.

This class exposes the internal unsafe machinery of the library; a safer and less error-prone way to get instances for it is via SNum or StockLit.

Minimal complete definition

unsafeFromInteger, unsafeMatchInteger

Instances

HasIntLiterals Double

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion Double :: Type -> Integer -> Constraint

type LitConstraint Double :: Integer -> Constraint

type LitAssertion Double :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion Double b n, ReprAssertion Double b n) => Proxy b -> Tagged n Integer -> Double

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion Double b n => Proxy b -> Tagged n Integer -> Double -> CMaybe (LitConstraint Double n)

HasIntLiterals Float

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion Float :: Type -> Integer -> Constraint

type LitConstraint Float :: Integer -> Constraint

type LitAssertion Float :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion Float b n, ReprAssertion Float b n) => Proxy b -> Tagged n Integer -> Float

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion Float b n => Proxy b -> Tagged n Integer -> Float -> CMaybe (LitConstraint Float n)

HasIntLiterals Int

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion Int :: Type -> Integer -> Constraint

type LitConstraint Int :: Integer -> Constraint

type LitAssertion Int :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion Int b n, ReprAssertion Int b n) => Proxy b -> Tagged n Integer -> Int

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion Int b n => Proxy b -> Tagged n Integer -> Int -> CMaybe (LitConstraint Int n)

HasIntLiterals Int8

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion Int8 :: Type -> Integer -> Constraint

type LitConstraint Int8 :: Integer -> Constraint

type LitAssertion Int8 :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion Int8 b n, ReprAssertion Int8 b n) => Proxy b -> Tagged n Integer -> Int8

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion Int8 b n => Proxy b -> Tagged n Integer -> Int8 -> CMaybe (LitConstraint Int8 n)

HasIntLiterals Int16

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion Int16 :: Type -> Integer -> Constraint

type LitConstraint Int16 :: Integer -> Constraint

type LitAssertion Int16 :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion Int16 b n, ReprAssertion Int16 b n) => Proxy b -> Tagged n Integer -> Int16

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion Int16 b n => Proxy b -> Tagged n Integer -> Int16 -> CMaybe (LitConstraint Int16 n)

HasIntLiterals Int32

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion Int32 :: Type -> Integer -> Constraint

type LitConstraint Int32 :: Integer -> Constraint

type LitAssertion Int32 :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion Int32 b n, ReprAssertion Int32 b n) => Proxy b -> Tagged n Integer -> Int32

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion Int32 b n => Proxy b -> Tagged n Integer -> Int32 -> CMaybe (LitConstraint Int32 n)

HasIntLiterals Int64

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion Int64 :: Type -> Integer -> Constraint

type LitConstraint Int64 :: Integer -> Constraint

type LitAssertion Int64 :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion Int64 b n, ReprAssertion Int64 b n) => Proxy b -> Tagged n Integer -> Int64

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion Int64 b n => Proxy b -> Tagged n Integer -> Int64 -> CMaybe (LitConstraint Int64 n)

HasIntLiterals Integer

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion Integer :: Type -> Integer -> Constraint

type LitConstraint Integer :: Integer -> Constraint

type LitAssertion Integer :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer0) b. (LitAssertion Integer b n, ReprAssertion Integer b n) => Proxy b -> Tagged n Integer -> Integer

unsafeMatchInteger :: forall (n :: Integer0) b. ReprAssertion Integer b n => Proxy b -> Tagged n Integer -> Integer -> CMaybe (LitConstraint Integer n)

HasIntLiterals Natural

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion Natural :: Type -> Integer -> Constraint

type LitConstraint Natural :: Integer -> Constraint

type LitAssertion Natural :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion Natural b n, ReprAssertion Natural b n) => Proxy b -> Tagged n Integer -> Natural

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion Natural b n => Proxy b -> Tagged n Integer -> Natural -> CMaybe (LitConstraint Natural n)

HasIntLiterals Word

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion Word :: Type -> Integer -> Constraint

type LitConstraint Word :: Integer -> Constraint

type LitAssertion Word :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion Word b n, ReprAssertion Word b n) => Proxy b -> Tagged n Integer -> Word

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion Word b n => Proxy b -> Tagged n Integer -> Word -> CMaybe (LitConstraint Word n)

HasIntLiterals Word8

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion Word8 :: Type -> Integer -> Constraint

type LitConstraint Word8 :: Integer -> Constraint

type LitAssertion Word8 :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion Word8 b n, ReprAssertion Word8 b n) => Proxy b -> Tagged n Integer -> Word8

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion Word8 b n => Proxy b -> Tagged n Integer -> Word8 -> CMaybe (LitConstraint Word8 n)

HasIntLiterals Word16

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion Word16 :: Type -> Integer -> Constraint

type LitConstraint Word16 :: Integer -> Constraint

type LitAssertion Word16 :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion Word16 b n, ReprAssertion Word16 b n) => Proxy b -> Tagged n Integer -> Word16

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion Word16 b n => Proxy b -> Tagged n Integer -> Word16 -> CMaybe (LitConstraint Word16 n)

HasIntLiterals Word32

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion Word32 :: Type -> Integer -> Constraint

type LitConstraint Word32 :: Integer -> Constraint

type LitAssertion Word32 :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion Word32 b n, ReprAssertion Word32 b n) => Proxy b -> Tagged n Integer -> Word32

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion Word32 b n => Proxy b -> Tagged n Integer -> Word32 -> CMaybe (LitConstraint Word32 n)

HasIntLiterals Word64

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion Word64 :: Type -> Integer -> Constraint

type LitConstraint Word64 :: Integer -> Constraint

type LitAssertion Word64 :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion Word64 b n, ReprAssertion Word64 b n) => Proxy b -> Tagged n Integer -> Word64

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion Word64 b n => Proxy b -> Tagged n Integer -> Word64 -> CMaybe (LitConstraint Word64 n)

HasIntLiterals CChar

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CChar :: Type -> Integer -> Constraint

type LitConstraint CChar :: Integer -> Constraint

type LitAssertion CChar :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CChar b n, ReprAssertion CChar b n) => Proxy b -> Tagged n Integer -> CChar

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CChar b n => Proxy b -> Tagged n Integer -> CChar -> CMaybe (LitConstraint CChar n)

HasIntLiterals CSChar

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CSChar :: Type -> Integer -> Constraint

type LitConstraint CSChar :: Integer -> Constraint

type LitAssertion CSChar :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CSChar b n, ReprAssertion CSChar b n) => Proxy b -> Tagged n Integer -> CSChar

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CSChar b n => Proxy b -> Tagged n Integer -> CSChar -> CMaybe (LitConstraint CSChar n)

HasIntLiterals CUChar

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CUChar :: Type -> Integer -> Constraint

type LitConstraint CUChar :: Integer -> Constraint

type LitAssertion CUChar :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CUChar b n, ReprAssertion CUChar b n) => Proxy b -> Tagged n Integer -> CUChar

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CUChar b n => Proxy b -> Tagged n Integer -> CUChar -> CMaybe (LitConstraint CUChar n)

HasIntLiterals CShort

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CShort :: Type -> Integer -> Constraint

type LitConstraint CShort :: Integer -> Constraint

type LitAssertion CShort :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CShort b n, ReprAssertion CShort b n) => Proxy b -> Tagged n Integer -> CShort

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CShort b n => Proxy b -> Tagged n Integer -> CShort -> CMaybe (LitConstraint CShort n)

HasIntLiterals CUShort

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CUShort :: Type -> Integer -> Constraint

type LitConstraint CUShort :: Integer -> Constraint

type LitAssertion CUShort :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CUShort b n, ReprAssertion CUShort b n) => Proxy b -> Tagged n Integer -> CUShort

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CUShort b n => Proxy b -> Tagged n Integer -> CUShort -> CMaybe (LitConstraint CUShort n)

HasIntLiterals CInt

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CInt :: Type -> Integer -> Constraint

type LitConstraint CInt :: Integer -> Constraint

type LitAssertion CInt :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CInt b n, ReprAssertion CInt b n) => Proxy b -> Tagged n Integer -> CInt

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CInt b n => Proxy b -> Tagged n Integer -> CInt -> CMaybe (LitConstraint CInt n)

HasIntLiterals CUInt

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CUInt :: Type -> Integer -> Constraint

type LitConstraint CUInt :: Integer -> Constraint

type LitAssertion CUInt :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CUInt b n, ReprAssertion CUInt b n) => Proxy b -> Tagged n Integer -> CUInt

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CUInt b n => Proxy b -> Tagged n Integer -> CUInt -> CMaybe (LitConstraint CUInt n)

HasIntLiterals CLong

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CLong :: Type -> Integer -> Constraint

type LitConstraint CLong :: Integer -> Constraint

type LitAssertion CLong :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CLong b n, ReprAssertion CLong b n) => Proxy b -> Tagged n Integer -> CLong

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CLong b n => Proxy b -> Tagged n Integer -> CLong -> CMaybe (LitConstraint CLong n)

HasIntLiterals CULong

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CULong :: Type -> Integer -> Constraint

type LitConstraint CULong :: Integer -> Constraint

type LitAssertion CULong :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CULong b n, ReprAssertion CULong b n) => Proxy b -> Tagged n Integer -> CULong

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CULong b n => Proxy b -> Tagged n Integer -> CULong -> CMaybe (LitConstraint CULong n)

HasIntLiterals CLLong

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CLLong :: Type -> Integer -> Constraint

type LitConstraint CLLong :: Integer -> Constraint

type LitAssertion CLLong :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CLLong b n, ReprAssertion CLLong b n) => Proxy b -> Tagged n Integer -> CLLong

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CLLong b n => Proxy b -> Tagged n Integer -> CLLong -> CMaybe (LitConstraint CLLong n)

HasIntLiterals CULLong

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CULLong :: Type -> Integer -> Constraint

type LitConstraint CULLong :: Integer -> Constraint

type LitAssertion CULLong :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CULLong b n, ReprAssertion CULLong b n) => Proxy b -> Tagged n Integer -> CULLong

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CULLong b n => Proxy b -> Tagged n Integer -> CULLong -> CMaybe (LitConstraint CULLong n)

HasIntLiterals CBool

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CBool :: Type -> Integer -> Constraint

type LitConstraint CBool :: Integer -> Constraint

type LitAssertion CBool :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CBool b n, ReprAssertion CBool b n) => Proxy b -> Tagged n Integer -> CBool

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CBool b n => Proxy b -> Tagged n Integer -> CBool -> CMaybe (LitConstraint CBool n)

HasIntLiterals CPtrdiff

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CPtrdiff :: Type -> Integer -> Constraint

type LitConstraint CPtrdiff :: Integer -> Constraint

type LitAssertion CPtrdiff :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CPtrdiff b n, ReprAssertion CPtrdiff b n) => Proxy b -> Tagged n Integer -> CPtrdiff

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CPtrdiff b n => Proxy b -> Tagged n Integer -> CPtrdiff -> CMaybe (LitConstraint CPtrdiff n)

HasIntLiterals CSize

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CSize :: Type -> Integer -> Constraint

type LitConstraint CSize :: Integer -> Constraint

type LitAssertion CSize :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CSize b n, ReprAssertion CSize b n) => Proxy b -> Tagged n Integer -> CSize

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CSize b n => Proxy b -> Tagged n Integer -> CSize -> CMaybe (LitConstraint CSize n)

HasIntLiterals CWchar

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CWchar :: Type -> Integer -> Constraint

type LitConstraint CWchar :: Integer -> Constraint

type LitAssertion CWchar :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CWchar b n, ReprAssertion CWchar b n) => Proxy b -> Tagged n Integer -> CWchar

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CWchar b n => Proxy b -> Tagged n Integer -> CWchar -> CMaybe (LitConstraint CWchar n)

HasIntLiterals CSigAtomic

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CSigAtomic :: Type -> Integer -> Constraint

type LitConstraint CSigAtomic :: Integer -> Constraint

type LitAssertion CSigAtomic :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CSigAtomic b n, ReprAssertion CSigAtomic b n) => Proxy b -> Tagged n Integer -> CSigAtomic

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CSigAtomic b n => Proxy b -> Tagged n Integer -> CSigAtomic -> CMaybe (LitConstraint CSigAtomic n)

HasIntLiterals CClock

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CClock :: Type -> Integer -> Constraint

type LitConstraint CClock :: Integer -> Constraint

type LitAssertion CClock :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CClock b n, ReprAssertion CClock b n) => Proxy b -> Tagged n Integer -> CClock

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CClock b n => Proxy b -> Tagged n Integer -> CClock -> CMaybe (LitConstraint CClock n)

HasIntLiterals CTime

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CTime :: Type -> Integer -> Constraint

type LitConstraint CTime :: Integer -> Constraint

type LitAssertion CTime :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CTime b n, ReprAssertion CTime b n) => Proxy b -> Tagged n Integer -> CTime

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CTime b n => Proxy b -> Tagged n Integer -> CTime -> CMaybe (LitConstraint CTime n)

HasIntLiterals CUSeconds

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CUSeconds :: Type -> Integer -> Constraint

type LitConstraint CUSeconds :: Integer -> Constraint

type LitAssertion CUSeconds :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CUSeconds b n, ReprAssertion CUSeconds b n) => Proxy b -> Tagged n Integer -> CUSeconds

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CUSeconds b n => Proxy b -> Tagged n Integer -> CUSeconds -> CMaybe (LitConstraint CUSeconds n)

HasIntLiterals CSUSeconds

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CSUSeconds :: Type -> Integer -> Constraint

type LitConstraint CSUSeconds :: Integer -> Constraint

type LitAssertion CSUSeconds :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CSUSeconds b n, ReprAssertion CSUSeconds b n) => Proxy b -> Tagged n Integer -> CSUSeconds

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CSUSeconds b n => Proxy b -> Tagged n Integer -> CSUSeconds -> CMaybe (LitConstraint CSUSeconds n)

HasIntLiterals CIntPtr

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CIntPtr :: Type -> Integer -> Constraint

type LitConstraint CIntPtr :: Integer -> Constraint

type LitAssertion CIntPtr :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CIntPtr b n, ReprAssertion CIntPtr b n) => Proxy b -> Tagged n Integer -> CIntPtr

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CIntPtr b n => Proxy b -> Tagged n Integer -> CIntPtr -> CMaybe (LitConstraint CIntPtr n)

HasIntLiterals CUIntPtr

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CUIntPtr :: Type -> Integer -> Constraint

type LitConstraint CUIntPtr :: Integer -> Constraint

type LitAssertion CUIntPtr :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CUIntPtr b n, ReprAssertion CUIntPtr b n) => Proxy b -> Tagged n Integer -> CUIntPtr

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CUIntPtr b n => Proxy b -> Tagged n Integer -> CUIntPtr -> CMaybe (LitConstraint CUIntPtr n)

HasIntLiterals CIntMax

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CIntMax :: Type -> Integer -> Constraint

type LitConstraint CIntMax :: Integer -> Constraint

type LitAssertion CIntMax :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CIntMax b n, ReprAssertion CIntMax b n) => Proxy b -> Tagged n Integer -> CIntMax

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CIntMax b n => Proxy b -> Tagged n Integer -> CIntMax -> CMaybe (LitConstraint CIntMax n)

HasIntLiterals CUIntMax

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion CUIntMax :: Type -> Integer -> Constraint

type LitConstraint CUIntMax :: Integer -> Constraint

type LitAssertion CUIntMax :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion CUIntMax b n, ReprAssertion CUIntMax b n) => Proxy b -> Tagged n Integer -> CUIntMax

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion CUIntMax b n => Proxy b -> Tagged n Integer -> CUIntMax -> CMaybe (LitConstraint CUIntMax n)

Integral a => HasIntLiterals (Ratio a)

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion (Ratio a) :: Type -> Integer -> Constraint

type LitConstraint (Ratio a) :: Integer -> Constraint

type LitAssertion (Ratio a) :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (Ratio a) b n, ReprAssertion (Ratio a) b n) => Proxy b -> Tagged n Integer -> Ratio a

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (Ratio a) b n => Proxy b -> Tagged n Integer -> Ratio a -> CMaybe (LitConstraint (Ratio a) n)

(Eq a, Num a) => HasIntLiterals (Min a)

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion (Min a) :: Type -> Integer -> Constraint

type LitConstraint (Min a) :: Integer -> Constraint

type LitAssertion (Min a) :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (Min a) b n, ReprAssertion (Min a) b n) => Proxy b -> Tagged n Integer -> Min a

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (Min a) b n => Proxy b -> Tagged n Integer -> Min a -> CMaybe (LitConstraint (Min a) n)

(Eq a, Num a) => HasIntLiterals (Max a)

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion (Max a) :: Type -> Integer -> Constraint

type LitConstraint (Max a) :: Integer -> Constraint

type LitAssertion (Max a) :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (Max a) b n, ReprAssertion (Max a) b n) => Proxy b -> Tagged n Integer -> Max a

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (Max a) b n => Proxy b -> Tagged n Integer -> Max a -> CMaybe (LitConstraint (Max a) n)

(Eq a, Num a) => HasIntLiterals (Identity a)

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion (Identity a) :: Type -> Integer -> Constraint

type LitConstraint (Identity a) :: Integer -> Constraint

type LitAssertion (Identity a) :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (Identity a) b n, ReprAssertion (Identity a) b n) => Proxy b -> Tagged n Integer -> Identity a

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (Identity a) b n => Proxy b -> Tagged n Integer -> Identity a -> CMaybe (LitConstraint (Identity a) n)

(Eq a, Num a) => HasIntLiterals (Sum a)

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion (Sum a) :: Type -> Integer -> Constraint

type LitConstraint (Sum a) :: Integer -> Constraint

type LitAssertion (Sum a) :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (Sum a) b n, ReprAssertion (Sum a) b n) => Proxy b -> Tagged n Integer -> Sum a

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (Sum a) b n => Proxy b -> Tagged n Integer -> Sum a -> CMaybe (LitConstraint (Sum a) n)

(Eq a, Num a) => HasIntLiterals (Product a)

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion (Product a) :: Type -> Integer -> Constraint

type LitConstraint (Product a) :: Integer -> Constraint

type LitAssertion (Product a) :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (Product a) b n, ReprAssertion (Product a) b n) => Proxy b -> Tagged n Integer -> Product a

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (Product a) b n => Proxy b -> Tagged n Integer -> Product a -> CMaybe (LitConstraint (Product a) n)

HasIntLiterals (Fin n)

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion (Fin n) :: Type -> Integer -> Constraint

type LitConstraint (Fin n) :: Integer -> Constraint

type LitAssertion (Fin n) :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n0 :: Integer) b. (LitAssertion (Fin n) b n0, ReprAssertion (Fin n) b n0) => Proxy b -> Tagged n0 Integer -> Fin n

unsafeMatchInteger :: forall (n0 :: Integer) b. ReprAssertion (Fin n) b n0 => Proxy b -> Tagged n0 Integer -> Fin n -> CMaybe (LitConstraint (Fin n) n0)

HasIntLiterals (SInt n)

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion (SInt n) :: Type -> Integer -> Constraint

type LitConstraint (SInt n) :: Integer -> Constraint

type LitAssertion (SInt n) :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n0 :: Integer) b. (LitAssertion (SInt n) b n0, ReprAssertion (SInt n) b n0) => Proxy b -> Tagged n0 Integer -> SInt n

unsafeMatchInteger :: forall (n0 :: Integer) b. ReprAssertion (SInt n) b n0 => Proxy b -> Tagged n0 Integer -> SInt n -> CMaybe (LitConstraint (SInt n) n0)

(Eq a, Num a) => HasIntLiterals (StockLit a)

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion (StockLit a) :: Type -> Integer -> Constraint

type LitConstraint (StockLit a) :: Integer -> Constraint

type LitAssertion (StockLit a) :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (StockLit a) b n, ReprAssertion (StockLit a) b n) => Proxy b -> Tagged n Integer -> StockLit a

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (StockLit a) b n => Proxy b -> Tagged n Integer -> StockLit a -> CMaybe (LitConstraint (StockLit a) n)

(Eq a, Num a) => HasIntLiterals (SNumber a n)

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion (SNumber a n) :: Type -> Integer -> Constraint

type LitConstraint (SNumber a n) :: Integer -> Constraint

type LitAssertion (SNumber a n) :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n0 :: Integer) b. (LitAssertion (SNumber a n) b n0, ReprAssertion (SNumber a n) b n0) => Proxy b -> Tagged n0 Integer -> SNumber a n

unsafeMatchInteger :: forall (n0 :: Integer) b. ReprAssertion (SNumber a n) b n0 => Proxy b -> Tagged n0 Integer -> SNumber a n -> CMaybe (LitConstraint (SNumber a n) n0)

(Eq a, Num a) => HasIntLiterals (Wrapped Num a)

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion (Wrapped Num a) :: Type -> Integer -> Constraint

type LitConstraint (Wrapped Num a) :: Integer -> Constraint

type LitAssertion (Wrapped Num a) :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (Wrapped Num a) b n, ReprAssertion (Wrapped Num a) b n) => Proxy b -> Tagged n Integer -> Wrapped Num a

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (Wrapped Num a) b n => Proxy b -> Tagged n Integer -> Wrapped Num a -> CMaybe (LitConstraint (Wrapped Num a) n)

(Eq (SNumRepr a), Num (SNumRepr a), SNum a) => HasIntLiterals (SNumLit c a)

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion (SNumLit c a) :: Type -> Integer -> Constraint

type LitConstraint (SNumLit c a) :: Integer -> Constraint

type LitAssertion (SNumLit c a) :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (SNumLit c a) b n, ReprAssertion (SNumLit c a) b n) => Proxy b -> Tagged n Integer -> SNumLit c a

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (SNumLit c a) b n => Proxy b -> Tagged n Integer -> SNumLit c a -> CMaybe (LitConstraint (SNumLit c a) n)

(Eq a, Num a) => HasIntLiterals (Const a b)

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion (Const a b) :: Type -> Integer -> Constraint

type LitConstraint (Const a b) :: Integer -> Constraint

type LitAssertion (Const a b) :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b0. (LitAssertion (Const a b) b0 n, ReprAssertion (Const a b) b0 n) => Proxy b0 -> Tagged n Integer -> Const a b

unsafeMatchInteger :: forall (n :: Integer) b0. ReprAssertion (Const a b) b0 n => Proxy b0 -> Tagged n Integer -> Const a b -> CMaybe (LitConstraint (Const a b) n)

type AllowsIntLiteral n a = (LitAssertion a a (ToInteger n), ReprAssertion a a (ToInteger n))

A constraint alias showing that the particular value n is valid for a.

With this in context along with HasIntLiterals a, you can use an integral literal value n at type a. See also IntLiteral.

type IntLiteral n a = (HasIntLiterals a, AllowsIntLiteral n a)

A convenient form of IntLiteral when only one value is needed.

This is a constraint tuple, so using this multiple times in a signature creates a bit of constraint pollution; for tidier signatures, use one HasIntLiterals and several AllowsIntLiterals.

valueOf :: forall n a. (IntLiteral (ToInteger n) a, KnownInteger (ToInteger n)) => a

Get the value of a type-level number at runtime, as if it were a literal.

That is, when DependentLiterals is enabled, 42 and valueOf @42 are the same thing. (When it's not enabled, 42 is just fromInteger 42).

Basic Literals

type HasBasicLiterals a = (HasIntLiterals a, LitAssertion a ~ NoAssertion, ReprAssertion a ~ NoAssertion)

A constraint alias that asserts you can use any integral literal.

This can be useful in polymorphic contexts when you don't want to list out constraints for every literal value you need, and are willing to accept that some types with stronger compile-time validation will be excluded.

newtype StockLit a

Use Wrapped Num directly instead.

The HasIntLiterals instance of Wrapped Num results in integral literals and patterns that behave like the stock literals would have, according to the underlying type's Num instance.

For use with -XDerivingVia. This calls through to the fromIntegral of the underlying Num instance for the final conversion. If the type in question has a Num instance and it's acceptable for literals to overflow (or if the type is supported by -Woverflowed-literals), this is a good way to get an instance.

This is suitable for DerivingVia and tends to work as a deriving clause, so:

    newtype MyType = MyType Int
      deriving (Eq, Num)
      deriving HasIntLiterals via Wrapped Num MyType

Note in this case you could just as well say deriving HasIntLiterals to get a GeneralizedNewtypeDeriving instance that consumes Int literals and coerces them, but if you wrote a custom Num instance, via Wrapped Num MyType will respect it.

Constructors

StockLit a

Instances

(Eq a, Num a) => HasIntLiterals (StockLit a)

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion (StockLit a) :: Type -> Integer -> Constraint

type LitConstraint (StockLit a) :: Integer -> Constraint

type LitAssertion (StockLit a) :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (StockLit a) b n, ReprAssertion (StockLit a) b n) => Proxy b -> Tagged n Integer -> StockLit a

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (StockLit a) b n => Proxy b -> Tagged n Integer -> StockLit a -> CMaybe (LitConstraint (StockLit a) n)

type ReprAssertion (StockLit a)

Defined in DependentLiterals.Int

type ReprAssertion (StockLit a) = ReprAssertion (Wrapped Num a)

type LitConstraint (StockLit a)

Defined in DependentLiterals.Int

type LitConstraint (StockLit a) = LitConstraint (Wrapped Num a)

type LitAssertion (StockLit a)

Defined in DependentLiterals.Int

type LitAssertion (StockLit a) = LitAssertion (Wrapped Num a)

Dependent Literals

class SNum a where

A user-facing dependent numeric typeclass.

This gives an isomorphism between a and exists n. SNumber (SNumRepr a) n given that SNumConstraint a n holds.

To get instances of HasIntLiterals without interacting with the unsafe parts of the library, implement this class and lift it to HasIntLiterals with deriving HasIntLiterals via SNumLit MyAssertionClass MyType.

Associated Types

type SNumRepr a :: Type

The underlying numerical representation type.

type SNumConstraint a :: Integer -> Constraint

The constraint on literal values to validate/refine a.

Methods

fromSNum :: Satisfying (SNumConstraint a) (SNumber (SNumRepr a)) -> a

Conversion from SNumber with a proof of SNumConstraint into a.

Used for interpreting integral literals.

intoSNum :: a -> Satisfying (SNumConstraint a) (SNumber (SNumRepr a))

Conversion from a into SNumber with a proof of 'SNumConstraint.'

Used for providing proofs on successful pattern matches.

Instances

SNum (Fin n)

Defined in DependentLiterals.Int

Associated Types

type SNumRepr (Fin n)

type SNumConstraint (Fin n) :: Integer -> Constraint

Methods

fromSNum :: Satisfying (SNumConstraint (Fin n)) (SNumber (SNumRepr (Fin n))) -> Fin n

intoSNum :: Fin n -> Satisfying (SNumConstraint (Fin n)) (SNumber (SNumRepr (Fin n)))

SNum (SInt n)

Defined in DependentLiterals.Int

Associated Types

type SNumRepr (SInt n)

type SNumConstraint (SInt n) :: Integer -> Constraint

Methods

fromSNum :: Satisfying (SNumConstraint (SInt n)) (SNumber (SNumRepr (SInt n))) -> SInt n

intoSNum :: SInt n -> Satisfying (SNumConstraint (SInt n)) (SNumber (SNumRepr (SInt n)))

SNum (SNumber a n)

Defined in DependentLiterals.Int

Associated Types

type SNumRepr (SNumber a n)

type SNumConstraint (SNumber a n) :: Integer -> Constraint

Methods

fromSNum :: Satisfying (SNumConstraint (SNumber a n)) (SNumber (SNumRepr (SNumber a n))) -> SNumber a n

intoSNum :: SNumber a n -> Satisfying (SNumConstraint (SNumber a n)) (SNumber (SNumRepr (SNumber a n)))

newtype SNumLit (c :: Type -> Integer -> Constraint) a

A newtype carrying a HasIntLiterals instance for use with DerivingVia.

Constructors

SNumLit a

Instances

(Eq (SNumRepr a), Num (SNumRepr a), SNum a) => HasIntLiterals (SNumLit c a)

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion (SNumLit c a) :: Type -> Integer -> Constraint

type LitConstraint (SNumLit c a) :: Integer -> Constraint

type LitAssertion (SNumLit c a) :: Type -> Integer -> Constraint

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (SNumLit c a) b n, ReprAssertion (SNumLit c a) b n) => Proxy b -> Tagged n Integer -> SNumLit c a

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (SNumLit c a) b n => Proxy b -> Tagged n Integer -> SNumLit c a -> CMaybe (LitConstraint (SNumLit c a) n)

type ReprAssertion (SNumLit c a)

Defined in DependentLiterals.Int

type ReprAssertion (SNumLit c a)

type LitConstraint (SNumLit c a)

Defined in DependentLiterals.Int

type LitConstraint (SNumLit c a) = SNumConstraint a

type LitAssertion (SNumLit c a)

Defined in DependentLiterals.Int

type LitAssertion (SNumLit c a)