[ regression ] `Uninhabited (LTE 1 0)` will no longer be found

[stefan-hoeck]

PR #3225 introduced an implementation of Uninhabited (LTE (S n) n) to Data.Nat in base. This implementation overlaps with Uninhabited (LTE (S k) Z), which was already there, for the case k = 0. Thus, Uninhabited (LTE 1 0) will no longer be found by proof search.

I'm not sure how we should proceed in such a case. The two implementations of Uninhabited serve different purposes, so they both have their raison d'etre, but the case of LTE 1 0 is common enough that this is an issue. Since this is used in my own idris2-bytestring library, the pack collection currently fails to build. Fixing idris2-bytestring will be straight forward, so that's what I'm going to do now.

[gallais]

Cf. #3228

[stefan-hoeck]

Cf. #3228 Thanks. I didn't see that. I'll leave this open until the PR is merged.