Main.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
import Unboxable
import Mod
import Data.Coerce

-- Defining Unboxable instance is as good as exporting the data constructor!
castUnboxable :: Unboxable a => Rep a -> a
castUnboxable = coerce

mkArbitraryMod :: Int -> Mod m
mkArbitraryMod = castUnboxable

main = do
  let x, y :: Mod 37
      x = mkMod 42
      y = mkArbitraryMod 42
  print x
  print (x == y)
  print (checkInvariant x, checkInvariant y)

Mod.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Mod (Mod, mkMod, checkInvariant) where
import GHC.TypeLits (Nat, KnownNat, natVal)
import Unboxable

-- Invariant: the value x satisfies 0 <= x < m
newtype Mod (m :: Nat) = Mod Int -- the data constructor is not exported
  deriving (Eq, Show)

mkMod :: KnownNat m => Int -> Mod m
mkMod x = let m = Mod (x `mod` fromIntegral (natVal m))
          in m

-- All values of Mod should satisfy this condition...
checkInvariant :: KnownNat m => Mod m -> Bool
checkInvariant m@(Mod x) = 0 <= x && x < fromIntegral (natVal m)

instance Unboxable (Mod m) where
  type Rep (Mod m) = Int

Unboxable.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
module Unboxable where
import Data.Coerce

-- A simplified version of 'Unboxable' class
class Coercible a (Rep a) => Unboxable a where
  type Rep a