Duplicate pattern cases have an unclear error message

[edwinb]

Issue by MarcelineVQ
Thursday Apr 23, 2020 at 18:12 GMT
Originally opened as edwinb/Idris2-boot#315

---

Duplicate pattern cases have a very unclear error message.
Ran into this while writing a tree but the simpler case is shown here.

Steps to Reproduce

typecheck:

module Main

foo1 : Maybe a -> ()
foo1 Nothing = ()
foo1 Nothing = ()

foo2 : Maybe a -> ()
foo2 d = case d of
  Nothing => ()
  Nothing => ()

Expected Behavior

Expect to see an error about an unreachable case or a duplicate case for both foo versions.
Even once we have coverage checking and these were labeled partial an unreachable case warning/error seems like a good idea.

Observed Behavior

Test.idr:3:1--4:1:Attempt to match on erased argument ? in foo1
Test.idr:8:10--10:16:Attempt to match on erased argument ? in case block in foo2

[edwinb]

This seems to be an effect of the old way of checking erasure, which is now done at a higher level. It ends up with this being the error message when the case tree compiler reaches the end of a clause still with multiple options (it's in Core.CaseBuilder). I suppose what it should do instead is display a warning.

[edwinb]

I've changed the match compiler so that it warns on overlapping patterns. Erased patterns are checked earlier now.