Duplicate pattern cases have an unclear error message

[MarcelineVQ]

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