Bounded TypeNats (e.g. to range of Word16)

Learn
5

GHC.TypeLits.cmpNat!

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE
  MagicHash,
  DataKinds,
  AllowAmbiguousTypes,
  GADTs,
  BlockArguments
#-}

module Main where

import GHC.TypeLits
import GHC.Exts
import Data.Proxy
import Data.Word
import Data.Maybe

...

wordToNat16 :: Word16 -> SomeNat16
wordToNat16 w = fromJust do
  SomeNat n <- someNatVal (fromIntegral w)
  case cmpNat n (Proxy @65536) of
    LTI -> Just (SomeNat16 n)
    EQI -> Nothing
    GTI -> Nothing