It's more accurate to say that Idris can guess an implementation of the function, but it's not the only possible implementation with that type. There's nothing in the type to stop the function from reversing one or both of the lists before the zipping stage, for example. More generally, it could randomize the order of elements in one or both of the supplied lists.
It's interactive, though, and it's extremely fun to use. It gives you the feeling that you're solving a puzzle, and like a good puzzle game, it can do the obvious bits for you.
It is a serious shortcoming that even when you pay the complexity cost of dependent types, you still can't specify the intent in this case. I mean, the semantics of "zip" can't be specified with a type. You can define a "sorted list" or "ordered list" type, but you cannot enforce maintainance of the natural, arbitrary order of list elements. In this sense dependent types are both too complex to reason about and simultaneously not powerful enough to fully specify the function.
rzipWith :: (forall a. f a -> g a -> h a) -> Rec f as -> Rec g as -> Rec h as
zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith f as bs = recToVec (rzipWith f' as' bs') where
as' = vecToRec (fmap Const as)
bs' = vecToRec (fmap Const bs)
f' (Const a) (Const b) = Const (f a b)
vecToRec :: Vec n (f a) -> Rec f (Replicate n a)
recToVec :: Rec (Const a) as -> Vec (Length as) a
Right, for instance I wouldn't be surprised if "the least amount of work" here amounted to reversing both lists as you zip.
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:
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.