The removeLast() function signature would be UntypedCollection (S n) -> UntypedCollection n (S n) stands for successor of n. (Think of (S n) as n+1) Given thi

The removeLast() function signature would be UntypedCollection (S n) -> UntypedCollection n (S n) stands for successor of n. (Think of (S n) as n+1) Given this, you can't call removeLast() on an UntypedCollection Z (empty collection) because the types wouldn't match. So it's not by magic - the compiler knows the number of elements in the collection, because that value is part of the type. That's the entire point of dependent types - you get to have any value as part of a type. The part that becomes tiresome very quickly - is convincing the type checker that what you want is valid. You have to provide proofs for the most trivial things (2+1 = 1+2) and the way it is currently achieved, is not programmer friendly.