Copyright	(c) Viktor Dukhovni 2026
License	BSD-3-Clause
Maintainer	ietf-dane@dukhovni.org
Stability	unstable
Safe Haskell	None
Language	GHC2024

Net.DNSBase.Nat16

Contents

16-bit type-level naturals for Opaque RData

Description

A 16-bit-constrained variant of Nat: the Nat16 constraint carries enough type-level evidence to retrieve the numeric codepoint at runtime via natToWord16. Used to index the fallback OpaqueRData / OpaqueOption / OpaqueSPV carriers so that values for different RR option SVCB-parameter codepoints inhabit distinct types even though they share a single underlying representation. withNat16 brings a runtime Word16 value into scope as a Nat16-instantiated type variable.

Synopsis

type Nat = Natural
type Nat16 (n :: Nat) = (KnownNat n, CmpNat n 65536 ~ 'LT)
class Typeable (a :: k)
natToWord16 :: forall (n :: Nat) -> KnownNat n => Word16
withNat16 :: Word16 -> (forall (n :: Nat) -> Nat16 n => r) -> r

16-bit type-level naturals for Opaque RData

type Nat = Natural #

A type synonym for Natural.

Previously, this was an opaque data type, but it was changed to a type synonym.

Since: base-4.16.0.0

type Nat16 (n :: Nat) = (KnownNat n, CmpNat n 65536 ~ 'LT) Source #

class Typeable (a :: k) #

The class Typeable allows a concrete representation of a type to be calculated.

Minimal complete definition

typeRep#

natToWord16 :: forall (n :: Nat) -> KnownNat n => Word16 Source #

Convert 16-bit type-level natural to corresponding RRTYPE.

withNat16 :: Word16 -> (forall (n :: Nat) -> Nat16 n => r) -> r Source #

Convert RRTYPE to 16-bit natural SomeNat singleton.