De Bruijn indexing as in "http://www.cs.ru.nl/~james/RESEARCH/haskell2004.pdf" but with statically checked finite indices.

IAmNotAFiniteNumber.hs

{-# LANGUAGE 
    DataKinds, GADTs, TypeFamilies,
    ScopedTypeVariables, LambdaCase, 
    TemplateHaskell, StandaloneDeriving,
    DeriveFunctor, DeriveFoldable, DeriveTraversable, TypeOperators #-}

import Data.Singletons.TH
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)

$(singletons [d|
    data Nat = Zero | Succ Nat

    (+) :: Nat -> Nat -> Nat
    Zero   + b = b
    Succ a + b = Succ (a + b)
    |])

data Fin :: Nat -> * where
    FZero :: Fin (Succ n)
    FSucc :: Fin n -> Fin (Succ n)

deriving instance Show (Fin n)
deriving instance Eq   (Fin n)
deriving instance Ord  (Fin n)

tighten :: SNat n -> Fin (Succ n) -> Maybe (Fin n)
tighten SZero     FZero     = Nothing
tighten (SSucc n) FZero     = Just FZero
tighten (SSucc n) (FSucc f) = fmap FSucc (tighten n f)
tighten _         _         = error "The impossible has happened."

-- The relaxing functions could be replaced with unsafeCoerce.
-- I nevertheless attempted to optimize their usage here
-- (because unsafeCoerce is unsightly).
relax1 :: Fin n -> Fin (Succ n)
relax1 FZero     = FZero
relax1 (FSucc f) = FSucc (relax1 f)

relaxn :: SNat m -> Fin n -> Fin (n :+ m)
relaxn n FZero     = FZero
relaxn n (FSucc f) = FSucc (relaxn n f)

relaxExp :: SNat m -> Exp n a -> Exp (n :+ m) a
relaxExp n (B i)            = B (relaxn n i)
relaxExp n (App a b)        = App (relaxExp n a) (relaxExp n b)
relaxExp n (Lam (Scope xs)) = Lam (Scope (relaxExp n xs))
relaxExp n (F f)            = F f

newtype Scope (n :: Nat) (a :: *) = Scope (Exp (Succ n) a)
    deriving (Eq, Ord, Show, Functor, Foldable, Traversable)

data Exp (n :: Nat) (a :: *) = 
      F a
    | B (Fin n)
    | App (Exp n a) (Exp n a)
    | Lam (Scope n a)
      deriving (Eq, Ord, Show, Functor, Foldable, Traversable)

abstract :: forall a. Eq a => a -> Exp Zero a -> Scope Zero a
abstract x xs = Scope (sub FZero xs) where

    sub :: Fin (Succ n) -> Exp n a -> Exp (Succ n) a
    sub i (F y) | y == x    = B i
                | otherwise = F y
    sub _ (B i)             = B (relax1 i)
    sub i (App a b)         = App (sub i a) (sub i b)
    sub i (Lam (Scope xs')) = Lam (Scope (sub (FSucc i) xs'))

instantiate :: forall a. Exp Zero a -> Scope Zero a -> Exp Zero a
instantiate x (Scope xs) = sub SZero xs where

    sub :: SNat n -> Exp (Succ n) a -> Exp n a
    sub n (F y)            = F y
    sub n (App a b)        = App (sub n a) (sub n b)
    sub n (B i)            = maybe (relaxExp n x) B (tighten n i)
    sub n (Lam (Scope xs)) = Lam (Scope (sub (SSucc n) xs))

main = print $ abstract 100 (Lam $ Scope $ App (F 100) (Lam $ Scope $ App (B fin1) (F 100)))

fin0 = FZero
fin1 = FSucc fin0
fin2 = FSucc fin1
fin3 = FSucc fin2
fin4 = FSucc fin3
fin5 = FSucc fin4

nat0 = SZero
nat1 = SSucc nat0
nat2 = SSucc nat1
nat3 = SSucc nat2
nat4 = SSucc nat3
nat5 = SSucc nat4