Basic totality/coverage checking failure

[MarcelineVQ]

Idris ver 1.3.2-git:9549d9cb9

Steps to Reproduce

Check the following for totality via: :total foo

data Id a = MkId a
foo : (f : List a) -> Id (NonEmpty f) -> List a
foo (x :: xs) (MkId IsNonEmpty) = []

Expected Behavior

Expect foo to be covering and total.

Observed Behavior

Idris reports that foo does not cover all cases and :missing shows that the [] case for f is missing.

Writing

foo : (f : List a) -> NonEmpty f -> List a
foo (x :: xs) IsNonEmpty = []

is covering/total as one should expect, it is surprising for a straightforward wrapper to cause this.

This issue was discovered while checking totality on the following and minimized to Id for the example.

foo : (f : List a) -> (g : List a) -> Either (NonEmpty f) (NonEmpty g) -> List a
foo (x :: xs) ys (Left IsNonEmpty) = []
foo xs (y :: ys) (Right IsNonEmpty) = []