diff --git a/finite-typelits.cabal b/finite-typelits.cabal
--- a/finite-typelits.cabal
+++ b/finite-typelits.cabal
@@ -1,5 +1,5 @@
 name:                finite-typelits
-version:             0.2.0.1
+version:             0.2.1.0
 synopsis:            A type inhabited by finitely many values, indexed by type-level naturals
 description:         A type inhabited by finitely many values, indexed by type-level naturals.
 homepage:            https://github.com/mniip/finite-typelits
diff --git a/src/Data/Finite/Integral.hs b/src/Data/Finite/Integral.hs
--- a/src/Data/Finite/Integral.hs
+++ b/src/Data/Finite/Integral.hs
@@ -33,6 +33,7 @@
         combineSum, combineZero, combineProduct, combineOne, combineExponential,
         separateSum, separateZero, separateProduct, separateOne,
         separateExponential,
+        castFinite,
         isValidFinite
     )
     where
@@ -344,6 +345,13 @@
             where n' = n `div` m
         m = intVal (Proxy :: Proxy m)
 {-# INLINABLE separateExponential #-}
+
+-- | Convert a 'Finite' between different 'SaneIntegral' numeric types.
+castFinite
+    :: forall b a n. (SaneIntegral a, SaneIntegral b, Limited b n)
+    => Finite a n -> Finite b n
+castFinite (Finite x) = Finite $ fromIntegral x
+{-# INLINABLE castFinite #-}
 
 -- | Verifies that a given 'Finite' is valid. Should always return 'True' unless
 -- you bring the @Data.Finite.Internal.Finite@ constructor into the scope, or
diff --git a/src/Data/Finite/Internal/Integral.hs b/src/Data/Finite/Internal/Integral.hs
--- a/src/Data/Finite/Internal/Integral.hs
+++ b/src/Data/Finite/Internal/Integral.hs
@@ -10,6 +10,7 @@
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -106,6 +107,17 @@
     modMul n a b = fromInteger
         (modMul (toInteger n) (toInteger a) (toInteger b) :: Integer)
 
+    -- | Unsafely obtain evidence that @n <= Limit a@. When 'Limit' is 'Nothing'
+    -- there is no evidence to obtain, and @\\_ _ k -> k@ is a valid
+    -- implementation. When 'Limit' is a 'Just', the default implementation
+    -- should work.
+    unsafeWithLimited :: proxy1 a -> proxy2 n -> (Limited a n => r) -> r
+    default unsafeWithLimited
+        :: forall n r lim proxy1 proxy2. (Limit a ~ 'Just lim)
+        => proxy1 a -> proxy2 n -> (Limited a n => r) -> r
+    unsafeWithLimited _ _ k = case unsafeCoerce Refl :: (n <=? lim) :~: 'True of
+        Refl -> k
+
 instance SaneIntegral Integer where
     type Limit Integer = 'Nothing
     modAdd n a b = case a + b of
@@ -113,6 +125,7 @@
         r -> r
     modSub n a b = if a >= b then a - b else n - b + a
     modMul n a b = (a * b) `mod` n
+    unsafeWithLimited _ _ k = k
 
 #if MIN_VERSION_base(4,8,0)
 instance SaneIntegral Natural where
@@ -122,6 +135,7 @@
         r -> r
     modSub n a b = if a >= b then a - b else n - b + a
     modMul n a b = (a * b) `mod` n
+    unsafeWithLimited _ _ k = k
 #endif
 
 instance SaneIntegral Word where
@@ -252,7 +266,7 @@
     :: forall a n r proxy1 proxy2. (SaneIntegral a, KnownIntegral a n)
     => proxy1 a -> proxy2 n -> (KnownNat n => r) -> r
 withIntegral _ _ k = case someNatVal n of
-    Nothing -> error $ "withIntegral: got KnowIntegral instance dictionary "
+    Nothing -> error $ "withIntegral: got KnownIntegral instance dictionary "
         ++ " for which toInteger returns " ++ show n
     Just (SomeNat (_ :: Proxy m)) -> case unsafeCoerce Refl :: n :~: m of
         Refl -> k
@@ -261,10 +275,10 @@
 
 -- | Recover a 'Limited' constraint from a 'KnownIntegral' constraint.
 withLimited
-    :: forall a n r lim proxy1 proxy2. (Limit a ~ 'Just lim, KnownIntegral a n)
+    :: forall a n r proxy1 proxy2. (SaneIntegral a, KnownIntegral a n)
     => proxy1 a -> proxy2 n -> (Limited a n => r) -> r
-withLimited _ _ k = case unsafeCoerce Refl :: (n <=? lim) :~: 'True of
-    Refl -> k
+withLimited = unsafeWithLimited
+  where _n = intVal_ :: Tagged n a
 {-# INLINABLE withLimited #-}
 
 -- | Finite number type. The type @'Finite' a n@ is inhabited by exactly @n@
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -11,6 +12,7 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 module Main where
 
 import Control.Exception
@@ -96,23 +98,26 @@
 data SLimited a where
     SLimited :: (Limited a n, KnownNat n) => Proxy n -> SLimited a
 
-mkLimited
-    :: forall a lim. (Limit a ~ 'Just lim, KnownNat lim)
-    => Integer -> Maybe (SLimited a)
-mkLimited n = case someNatVal n of
-    Just (SomeNat (p :: Proxy b))
-        | n <= natVal @lim Proxy
-        , Refl :: (b <=? lim) :~: 'True <- unsafeCoerce Refl
-        -> Just $ SLimited p
-    _ -> Nothing
+class MkSLimited (lim :: Maybe Nat) where
+    mkSLimited
+        :: forall a. (SaneIntegral a, Limit a ~ lim)
+        => Integer -> Maybe (SLimited a)
 
-mkUnlimited
-    :: forall a. Limit a ~ 'Nothing
-    => Integer -> Maybe (SLimited a)
-mkUnlimited n = case someNatVal n of
-    Just (SomeNat p) -> Just $ SLimited p
-    _ -> Nothing
+instance KnownNat lim => MkSLimited ('Just lim) where
+    mkSLimited
+        :: forall a. (SaneIntegral a, Limit a ~ 'Just lim)
+        => Integer -> Maybe (SLimited a)
+    mkSLimited n = case someNatVal n of
+        Just (SomeNat p)
+            | n <= natVal @lim Proxy
+            -> Just $ unsafeWithLimited (Proxy @a) p $ SLimited p
+        _ -> Nothing
 
+instance MkSLimited 'Nothing where
+    mkSLimited n = case someNatVal n of
+        Just (SomeNat p) -> Just $ SLimited p
+        _ -> Nothing
+
 genSmall, genOver7, genOver8, genOver15, genOver16, genOver31, genOver32,
     genOver63, genOver64, genOverI, genOverW, genUnder7, genUnder8, genUnder15,
     genUnder16, genUnder32, genUnder63, genUnder64, genUnderI, genUnderW
@@ -139,14 +144,19 @@
 genUnderI = ((toInteger (maxBound @Int) -) <$> genSmall) `suchThat` (>= 0)
 genUnderW = ((toInteger (maxBound @Word) -) <$> genSmall) `suchThat` (>= 0)
 
+shrinkSLimited
+    :: (SaneIntegral a, MkSLimited (Limit a), Arbitrary a)
+    => SLimited a -> [SLimited a]
+shrinkSLimited (SLimited p) = mapMaybe mkSLimited $ shrink $ natVal p
+
 instance Arbitrary (SLimited Integer) where
     arbitrary = oneof
         [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
         , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
         , genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI
         , genOverI, genUnderW, genOverW ]
-        `suchThatMap` mkUnlimited
-    shrink (SLimited p) = mapMaybe mkUnlimited $ shrink $ natVal p
+        `suchThatMap` mkSLimited
+    shrink = shrinkSLimited
 
 instance Arbitrary (SLimited Natural) where
     arbitrary = oneof
@@ -154,8 +164,8 @@
         , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
         , genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI
         , genOverI, genUnderW, genOverW ]
-        `suchThatMap` mkUnlimited
-    shrink (SLimited p) = mapMaybe mkUnlimited $ shrink $ natVal p
+        `suchThatMap` mkSLimited
+    shrink = shrinkSLimited
 
 instance Arbitrary (SLimited Word) where
     arbitrary = oneof
@@ -163,55 +173,55 @@
         , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
         , genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI
         , genOverI, genUnderW ]
-        `suchThatMap` mkLimited
-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p
+        `suchThatMap` mkSLimited
+    shrink = shrinkSLimited
 
 instance Arbitrary (SLimited Int) where
     arbitrary = oneof
         [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
         , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
         , genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI ]
-        `suchThatMap` mkLimited
-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p
+        `suchThatMap` mkSLimited
+    shrink = shrinkSLimited
 
 instance Arbitrary (SLimited Word8) where
     arbitrary = oneof
         [ genSmall, genUnder7, genOver7, genUnder8 ]
-        `suchThatMap` mkLimited
-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p
+        `suchThatMap` mkSLimited
+    shrink = shrinkSLimited
 
 instance Arbitrary (SLimited Int8) where
     arbitrary = oneof
         [ genSmall, genUnder7 ]
-        `suchThatMap` mkLimited
-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p
+        `suchThatMap` mkSLimited
+    shrink = shrinkSLimited
 
 instance Arbitrary (SLimited Word16) where
     arbitrary = oneof
         [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
         , genOver15, genUnder16 ]
-        `suchThatMap` mkLimited
-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p
+        `suchThatMap` mkSLimited
+    shrink = shrinkSLimited
 
 instance Arbitrary (SLimited Int16) where
     arbitrary = oneof
         [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15 ]
-        `suchThatMap` mkLimited
-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p
+        `suchThatMap` mkSLimited
+    shrink = shrinkSLimited
 
 instance Arbitrary (SLimited Word32) where
     arbitrary = oneof
         [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
         , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32 ]
-        `suchThatMap` mkLimited
-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p
+        `suchThatMap` mkSLimited
+    shrink = shrinkSLimited
 
 instance Arbitrary (SLimited Int32) where
     arbitrary = oneof
         [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
         , genOver15, genUnder16, genOver16, genUnder31 ]
-        `suchThatMap` mkLimited
-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p
+        `suchThatMap` mkSLimited
+    shrink = shrinkSLimited
 
 instance Arbitrary (SLimited Word64) where
     arbitrary = oneof
@@ -219,65 +229,22 @@
         , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
         , genOver32, genUnder63, genOver63, genUnder64, genOverI, genUnderW
         , genOverW ]
-        `suchThatMap` mkLimited
-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p
+        `suchThatMap` mkSLimited
+    shrink = shrinkSLimited
 
 instance Arbitrary (SLimited Int64) where
     arbitrary = oneof
         [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
         , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
         , genOver32, genUnder63, genUnderI, genOverI, genUnderW, genOverW ]
-        `suchThatMap` mkLimited
-    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p
+        `suchThatMap` mkSLimited
+    shrink = shrinkSLimited
 
 newtype SmallLimited a = SmallLimited { getSmallLimited :: SLimited a }
 
-instance Arbitrary (SmallLimited Integer) where
-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkUnlimited
-    shrink = map SmallLimited . shrink . getSmallLimited
-
-instance Arbitrary (SmallLimited Natural) where
-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkUnlimited
-    shrink = map SmallLimited . shrink . getSmallLimited
-
-instance Arbitrary (SmallLimited Word) where
-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited
-    shrink = map SmallLimited . shrink . getSmallLimited
-
-instance Arbitrary (SmallLimited Int) where
-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited
-    shrink = map SmallLimited . shrink . getSmallLimited
-
-instance Arbitrary (SmallLimited Word8) where
-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited
-    shrink = map SmallLimited . shrink . getSmallLimited
-
-instance Arbitrary (SmallLimited Int8) where
-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited
-    shrink = map SmallLimited . shrink . getSmallLimited
-
-instance Arbitrary (SmallLimited Word16) where
-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited
-    shrink = map SmallLimited . shrink . getSmallLimited
-
-instance Arbitrary (SmallLimited Int16) where
-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited
-    shrink = map SmallLimited . shrink . getSmallLimited
-
-instance Arbitrary (SmallLimited Word32) where
-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited
-    shrink = map SmallLimited . shrink . getSmallLimited
-
-instance Arbitrary (SmallLimited Int32) where
-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited
-    shrink = map SmallLimited . shrink . getSmallLimited
-
-instance Arbitrary (SmallLimited Word64) where
-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited
-    shrink = map SmallLimited . shrink . getSmallLimited
-
-instance Arbitrary (SmallLimited Int64) where
-    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited
+instance (SaneIntegral a, MkSLimited (Limit a), Arbitrary (SLimited a))
+    => Arbitrary (SmallLimited a) where
+    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkSLimited
     shrink = map SmallLimited . shrink . getSmallLimited
 
 type Good a =
@@ -288,7 +255,7 @@
     , SaneIntegral a
     , Arbitrary a
     , Arbitrary (SLimited a)
-    , Arbitrary (SmallLimited a)
+    , MkSLimited (Limit a)
     , CoArbitrary a
     )
 
@@ -357,23 +324,10 @@
     (map getSmallLimited . shrink . SmallLimited)
 
 unsafeWithKnownIntegral
-    :: forall n a. (SaneIntegral a, Typeable a)
+    :: forall n a. (SaneIntegral a, MkSLimited (Limit a), Typeable a)
     => Integer -> ((KnownNat n, Limited a n) => Property) -> Property
 unsafeWithKnownIntegral n prop
-    | Just (Refl :: a :~: Integer) <- cast (Refl @a)
-    , Just (SLimited (_ :: Proxy n')) <- mkUnlimited @a n
-    , Refl <- unsafeCoerce Refl :: n :~: n'
-    = prop
-    | Just (Refl :: a :~: Natural) <- cast (Refl @a)
-    , Just (SLimited (_ :: Proxy n')) <- mkUnlimited @a n
-    , Refl <- unsafeCoerce Refl :: n :~: n'
-    = prop
-    | Just (Refl :: a :~: Word) <- cast (Refl @a)
-    , Just (SLimited (_ :: Proxy n')) <- mkLimited @a n
-    , Refl <- unsafeCoerce Refl :: n :~: n'
-    = prop
-    | Just (Refl :: a :~: Int) <- cast (Refl @a)
-    , Just (SLimited (_ :: Proxy n')) <- mkLimited @a n
+    | Just (SLimited (_ :: Proxy n')) <- mkSLimited @_ @a n
     , Refl <- unsafeCoerce Refl :: n :~: n'
     = prop
     | otherwise = discard
@@ -1113,6 +1067,27 @@
     property $ \(Big f :: Big a (m ^ n)) ->
     f `seq` -- could be discard
         combineExponential (separateExponential @n @m @a f) === f
+
+prop_valid_castFinite = forType $ \(_ :: Proxy b) ->
+    forType $ \(_ :: Proxy a) ->
+    forPositiveLimit @b $ \n (_ :: Proxy n) ->
+    unsafeWithKnownIntegral @n @a n $
+    property $ \(Edgy x :: Edgy a n) ->
+        isValidFinite $ castFinite @b x
+prop_sym_castFinite = forType $ \(_ :: Proxy a) ->
+    forType $ \(_ :: Proxy b) ->
+    forPositiveLimit @a $ \n (_ :: Proxy n) ->
+    unsafeWithKnownIntegral @n @b n $
+    property $ \(Edgy x :: Edgy b n) ->
+        castFinite @b (castFinite @a x) === x
+prop_trans_castFinite = forType $ \(_ :: Proxy a) ->
+    forType $ \(_ :: Proxy b) ->
+    forType $ \(_ :: Proxy c) ->
+    forPositiveLimit @a $ \n (_ :: Proxy n) ->
+    unsafeWithKnownIntegral @n @b n $
+    unsafeWithKnownIntegral @n @c n $
+    property $ \(Edgy x :: Edgy a n) ->
+        castFinite @c (castFinite @b x) === castFinite @c x
 
 return []
 main = $quickCheckAll >>= \case