[kaba0]

It is not possible, normal types can only prove so-called trivial properties (from Rice’s theorem). Every non-trivial property is unprovable in the general case.

Dependent-type systems can express more things (e.g. they can represent a concat function that takes two lists of n and m length, and return a list of length n+m), but proving those properties are hard and may not scale well. There are trade offs, like one might not have to actually prove the properties, just having them as facts may also be good enough.

[UncleMeat]

Types can only decide trivial properties. But that's fine. We can accept false positives (valid programs that nevertheless type incorrectly and are rejected by the compiler). You still get very powerful reasoning with this.

Dependent types are also equally stymied by Rice's Thm. Both are static techniques. Path based type reasoning doesn't do anything to solve the halting problem. It just means more expressive types.