{-# LANGUAGE GHC2024 #-}
-- base
import GHC.TypeLits (KnownNat (natSing), SNat, natVal, fromSNat, withSomeSNat)
-- constraints
import           Data.Constraint              (Dict, (\\))
import           Data.Constraint.Unsafe       (unsafeAxiom)

class KnownNat n => ValidUINTn n

instance ValidUINTn 1
instance ValidUINTn 2
instance ValidUINTn 3
instance ValidUINTn 4

data UINTn where
  UINTn :: ValidUINTn n => SNat n -> UINTn

instance Show UINTn where
  show (UINTn sn) = "UINT" <> show (natVal sn * 8)
  -- the following works:
  -- show (UINTn sn) = "UINT" <> show sn

getValidUINTn :: Integer -> Maybe UINTn
getValidUINTn sn = withSomeSNat sn $ \case
  Just (n :: SNat n) -> let n' = fromSNat n
                        in if n' >= 1 && n' <= 4 -- aren't you convinced by now it is ValidINTn?
                           then Just (UINTn n \\ (unsafeAxiom :: Dict (ValidUINTn n)))
                           else Nothing

main = do
  print $ show (UINTn (natSing @2)) 
  print $ getValidUINTn 4
  print $ getValidUINTn 5