What is the preferred alternative to Fin from Idris in Haskell

I would like to have a type which can contain values 0 to n, where n lives on the type level.

I was trying something like:

import GHC.TypeLits
import Data.Proxy

newtype FiniteNat n = FiniteNat { toInteger :: Integer }

smartConstructFiniteNat :: (KnownNat n) => Proxy n -> Integer -> Maybe (FiniteNat (Proxy n))
smartConstructFiniteNat pn i 
  | 0 <= i && i < n = Just (FiniteNat i)
  | otherwise       = Nothing
  where n = natVal pn

which works basically, but it's not really satisfying somehow. Is there a "standard" solution, or even a library to achieve this? There is a lot of fuss about dependenty typed list-lengths, but I was unable to find something exactly for this. Also - I assume using GHC.TypeLits is necessary, because my n can take on rather large values, so inductive definition would probably be very slow.