@mcc Disregarding my previous promise to know what I am talking about:
For your code that starts with

listEq : List (Eq a) -> List (Eq a) -> Bool

I think the interface restriction needs to be written like this:

listEq : Eq a => List a -> List a -> Bool

For your specialized integer code, I think you need to capitalize your int as Int or maybe Integer (so List int should be List Int)

Both these suggestions based on what I skimmed at https://idris2.readthedocs.io/en/latest/tutorial/interfaces.html

As for the covering, I don't know.

I really like following you Idris 2 adventure, I wish to learn it myself some day.

I remember my intense struggles and frustration when learning Haskell a long while ago.