[ fix ] False positives checking for conflicts in coverage checking

[dunhamsteve]

Description

This fixes #3477. Idris considers 2 = length xs as empty while checking missing cases in coverage checking, and it incorrectly accepts this as covering:

test : (xs : List Int) ->  2 = length xs -> (Int, Int)
test (x1 :: x2 :: x3 :: []) pf = (x1, x2)

There are two changes here:

I removed the clearDefs in conflictNF to allow the length xs to expand when xs is known. Let me know if there is a reason we don't allow expansions here. It passes tests and it seems to be necessary to enable Idris to automatically use the 2 = length xs.

Without this change, the following impossible clauses are required:

test : (xs : List Int) ->  2 = length xs -> (Int, Int)
test (x1 :: x2 :: []) pf = (x1, x2)
test (x1 :: Nil) Refl impossible
test (x1 :: x2 :: x3 :: _) Refl impossible

The second change addresses the root cause. When checking for clashes between types in conflictMatch, idris checks if the heads clash, and if not it proceeds to check the arguments. This is a problem when S (S Z) is compared to length xs. S and length do not clash, but it is not correct to then compare S Z against xs. To remedy this, it is now only checking the spines in the case of matching data or type constructors. The helper function returns Nothing to indicate the spine should be checked.

Krivine.idr was relying on this bug. The code was covering, but coverage checking was accepting it for the wrong reason. It was discounting the other case when looking at Element (EvalContext{}) _ vs (::) (Arr{}) ctx (here :: is a function, not a constructor). Element vs (::) was not clashing, so it proceeded to compare the arguments and saw that EvalContext{} and Arr{} clashed (values headed by different constructors). After this change, it needed an impossible clause to unblock the (::).

I've also added a test case, fixed a typo in a comment, and added a log message that I use do diagnose these impossible issues. This will break code that relies on false positives in coverage, but given that the rest of papers and frex are uneffected, I suspect that is rare.

[gallais]

Can you please document the meaning of this Maybe? Or should we even define
e.g. data ClashingDecision = Distinct | Same | Incomparable
with the idea that we are only checking the arguments if the heads are Same?

[dunhamsteve]

I was on the fence about whether to use an enum or not. Coming back to this a week later and having to get my bearings again, I think it would be clearer if I did that.