So dependent types. Unfortunately, not decidable.<p><a href="https://cs.stackexchange.com/questions/12691/what-makes-type-inference-for-dependent-types-undecidable" rel="nofollow">https://cs.stackexchange.com/questions/12691/what-makes-type...</a><p>In general I am torn between the enthusiasm people like the author bring to the table and their apparent lack of due diligence regarding a discipline that has been subject to thorough research for decades.