It's probably worth distinguishing between "compiler bugs" and "fundamental theoretical problems". From what I've seen of Idris 2 development, sometimes what lo

It's probably worth distinguishing between "compiler bugs" and "fundamental theoretical problems". From what I've seen of Idris 2 development, sometimes what looks like the former turns out to be the latter. But what I find really cool is that the theoretical problems are not necessarily unsolvable, and there seems to be a steady stream of new theoretical results that find their way into compilers. So even if we are a very long way off from these languages gaining wide adoption, it's exciting to see that progress is in fact being made, even if it's slow.