I've been learning the dependently typed functional language Idris over the past few weeks. The type-safe zip over Vects (linked lists with a length in the type) is a canonical example of compile-time proof that they must be the same length:

    zip : Vect n a -> Vect n b -> Vect n (a, b)

This type specifies that both Vects must be length n. If they are not equal in length, the code will not compile. In fact, this type is so narrowly specified that Idris can infer the entire implementation of the function from it.

Don't dependent types happen at run-time?

Dependent types in Idris occur at compile time and are erased as part of compilation. At runtime, those Vects do not carry around any length information.

It seems like you would have to solve the halting problem for them to work at compile time.

Idris addresses this by having a totality checker. Every function in Idris is marked as either total (known to halt, barring any bugs in the totality checker) or partial (possibly not halting). Only total functions are allowed in types. For example, the function append:

    append : Vect m a -> Vect n a -> Vect (m + n) a

This type uses addition as a type level function. Since (+) for natural numbers (which m and n are) is proven to be total when Idris compiles the library where it's defined, Idris allows it to be used as a type level function.

So how does the totality checker work? Wouldn't that purport to solve the halting problem? No, the totality checker in Idris isn't magic, it's conservative about what it considers to be total. In order for it to declare a function total, it must identify at least one argument that progresses towards a base case at every step. It can do this even with mutually recursive functions.

In practice, if you write an interactive program in Idris, you can make every function total except for main, which presumably contains an infinite loop that checks for input forever.