Compile time enforced finite lists

This can be done with Liquid Haskell, which provides termination checks.
Type signatures look like this in Liquid Haskell:

{-@ (function name) :: (refinement) [/ (termination metric)] @-}

The termination metric is an integer vector that is supposed to decrease each recursive call (lexicographical ordering). If not specified, LH will use the first integer argument as the termination metric.
Termination checking can be disabled with lazy annotation {-@ lazy (function name) @-}:

{-@ lazy inf @-}
inf x = x : inf x

Yep, just use an existential to forget the finite length afterwards:

data NonDependentList a where NonDependentList :: DependentList n a -> NonDependentList a

Of course, take and drop will have some boilerplate...

take :: Int -> NDL a -> NDL a
take n (NDL Nil) = NDL Nil
take n (NDL (Cons a as)) = case take (n-1) (NDL as) of
    NDL as' -> NDL (Cons a as')

But you still can't make an infinite one:

ones = NDL (Cons 1 (case ones of NDL os -> os)) -- existential escapes its scope