3 ms·
This is true, I should have mentioned it, although my point still applies to HM style type inference as well.
by gnulinux 6y ago
This is true, I should have mentioned it, although my point still applies to HM style type inference as well.
- cannabis_sam 6y agoTo 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)