As the workhorse example, consider the length-indexed Vector:

    data Vec : Nat -> Type -> Type

Each Vec has its length in its type. You get a type error if you try the following:

    f : Vec 3 Int -> Int
    f [1, 2, 3, 4] -- error: wanted a Vec 3 Int, found a Vec 4 Int

and with that, consider the following program:

    import Data.Vect
    
    readInts : (n : Nat) -> IO (Vect n Int)
    readInts 0 = pure []
    readInts (S n) = do
      x <- getLine
      rest <- readInts n
      pure $ (cast x) :: rest
    
    main : IO ()
    main = do
      length <- getLine
      ints <- readInts (fromInteger . cast $ length)
      pure ()

The above program doesn't know what the type of `ints` is in the do-block precisely. It has a length specified by the user! But we can reason about its length - and the type system would ensure that its length is propagated and handled properly everywhere we try to use it.