search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

Duplicate pattern cases have an unclear error message #315

Open MarcelineVQ opened 4 years ago

MarcelineVQ commented 4 years ago

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