To a point at least, HM type inference is decidable, but type inference in haskell with certain extensions or in agda (at least with certain pragmas) is not. T

To a point at least, HM type inference is decidable, but type inference in haskell with certain extensions or in agda (at least with certain pragmas) is not. The possibility of a diverging type-level function would require the type inference algorithm to solve the halting problem. (As I understand it at least, been a while since I got into the details)