If I understand it, this video series mentioned that idris2 currently has some type-in-type problems, so that one can exploit it to prove false claims. I am not familiar with the concept, and am concerned whether I should learn idris2 as a proof assistant/language. The speaker said then that it will probably be fixed sometime in the future, but it is not clear whether that has happened (as of 0.6.0).
So my questions are:
What's a good example of the type-in-type problem that leads to a falsely proved claim?
If one uses idris2 as a proof language, is there a way to use it carefully (in a disciplined way) to avoid the "type-in-type" problem?