Arend is inconsistent

[anshwad10]

I found a proof of Empty in Arend without any axioms:

\import Logic

\data Bad : \Prop
  | mkBad (\Pi {P : \Prop} -> P -> P)

\func bad : Bad => mkBad \lam x => x

\func noBad (b : Bad) : Empty \elim b
  | mkBad f => noBad (f bad)

\func uh-oh : Empty => noBad bad

Agda also had a similar problem with impredicativity and it was fixed by disallowing recursion in inductive types in Prop. Perhaps something similar can be implemented for Arend?

[anshwad10]

Specifically, the definition of noBad could be rejected by the termination checker.

[anshwad10]

It has been fixed in 1.11, the definition of noBad no longer typechecks