diff --git a/src/TypeUnary/Nat.hs b/src/TypeUnary/Nat.hs
--- a/src/TypeUnary/Nat.hs
+++ b/src/TypeUnary/Nat.hs
@@ -23,6 +23,7 @@
   , IsNat(..)
   -- * Inequality proofs and indices
   , (:<:)(..), Index(..), succI, index0, index1, index2, index3
+  , coerceToIndex
   ) where
 
 import Prelude hiding (foldr,sum)
@@ -110,14 +111,14 @@
   ZLess :: Z :<: S n
   SLess :: m :<: n -> S m :<: S n
 
--- data Index :: * -> * where
---   Index :: (n :<: lim) -> Nat n -> Index lim
-
--- or
-
 -- | A number under the given limit, with proof
 data Index lim = forall n. IsNat n => Index (n :<: lim) (Nat n)
 
+-- Equivalently,
+-- 
+--   data Index :: * -> * where
+--     Index :: (n :<: lim) -> Nat n -> Index lim
+
 -- TODO: Consider removing the Nat n field, since it's computable from
 -- IsNat n or n :<: lim.
 
@@ -138,6 +139,21 @@
 
 index3 :: Index (N4 :+: m)
 index3 = succI index2
+
+-- | Index generation from integer. Can fail dynamically if the integer is
+-- too large.
+coerceToIndex :: (Integral i, IsNat m) => i -> Index m
+coerceToIndex = coerceToIndex' nat
+
+coerceToIndex' :: Integral i => Nat m -> i -> Index m
+coerceToIndex' mOrig niOrig = loop mOrig niOrig
+ where
+   loop :: Integral i => Nat m -> i -> Index m
+   loop Zero _        = error $ "coerceToIndex: out of bounds: "
+                                ++ show niOrig ++ " should be less than "
+                                ++ show mOrig
+   loop (Succ _)   0  = Index ZLess Zero
+   loop (Succ m') ni' = succI (loop m' (ni'-1))
 
 {--------------------------------------------------------------------
     IsNat
diff --git a/src/TypeUnary/Vec.hs b/src/TypeUnary/Vec.hs
--- a/src/TypeUnary/Vec.hs
+++ b/src/TypeUnary/Vec.hs
@@ -31,6 +31,7 @@
   , get, get0, get1, get2, get3
   , update
   , set, set0, set1, set2, set3
+  , getI, setI
   , swizzle, split, deleteV, elemsV
   , ToVec(..)
   ) where
@@ -355,26 +356,22 @@
 set2 = set index2
 set3 = set index3
 
+-- | Variant of 'get' in which the index size is checked at run-time
+-- instead of compile-time.
+getI :: (IsNat n, Integral i) => i -> Vec n a -> a
+getI = get . coerceToIndex
 
+-- | Variant of 'set' in which the index size is checked at run-time
+-- instead of compile-time.
+setI :: (IsNat n, Integral i) => i -> a -> Vec n a -> Vec n a
+setI = set . coerceToIndex
+
+
 -- | Swizzling.  Extract multiple elements simultaneously.
 swizzle :: Vec n (Index m) -> Vec m a -> Vec n a
 swizzle ZVec        _ = ZVec
 swizzle (ix :< ixs) v = get ix v :< swizzle ixs v
 
-{-
--- 'a' :< 'b' :< 'c' :< ZVec
-t1 :: Three Char
-t1 = elemsV "abc"
-     -- 'a' :< 'b' :< 'c' :< ZVec
-
-t2 :: Four (Index N3)
-t2 = elemsV [index2, index0 ,index1, index2]
-
--- 'c' :< 'a' :< 'b' :< 'c' :< ZVec
-t3 :: Four Char
-t3 = swizzle t2 t1
--}
-
 -- | Split a vector
 split :: IsNat n => Vec (n :+: m) a -> (Vec n a, Vec m a)
 split = split' nat
@@ -443,6 +440,20 @@
 elemsV' Zero (_:_)        = error "elemsV: too many elements"
 elemsV' (Succ _) []       = error "elemsV: too few elements"
 elemsV' (Succ n) (a : as) = a :< elemsV' n as
+
+{-
+-- 'a' :< 'b' :< 'c' :< ZVec
+t1 :: Three Char
+t1 = elemsV "abc"
+     -- 'a' :< 'b' :< 'c' :< ZVec
+
+t2 :: Four (Index N3)
+t2 = elemsV [index2, index0 ,index1, index2]
+
+-- 'c' :< 'a' :< 'b' :< 'c' :< ZVec
+t3 :: Four Char
+t3 = swizzle t2 t1
+-}
 
 
 {--------------------------------------------------------------------
diff --git a/type-unary.cabal b/type-unary.cabal
--- a/type-unary.cabal
+++ b/type-unary.cabal
@@ -1,5 +1,5 @@
 Name:                type-unary
-Version:             0.1.14
+Version:             0.1.15
 Cabal-Version:       >= 1.2
 Synopsis:            
   Type-level and typed unary natural numbers, inequality proofs, vectors