prop rules malfunction when overlaps exist

[GoogleCodeExporter]

Consider this program:

$ cat issue107.prg
prop Issue107 :: Nat ~> * where
  Base :: Issue107 2t
  Step :: Issue107 n -> Issue107 (1+n)t

test :: Issue107 n => Nat' n -> Nat' n
test n = n

When I try the 'test' function I get the correct error for 0v and 1v, but for 
2v I'd expect no error. Instead I get:

prompt> test 2v

There is no solution to [Issue107 2t] because
The proposition: (Issue107 0t) is refutable.

Obviously 'Base' would provide a proof, but it is not considered, because the 
range of 'Step' also matches, and directs the proof down the wrong lane.
Reordering the constructors does not help either.

A workaround is to declare 'Step' thus:

Step :: Issue107 (2+n)t -> Issue107 (3+n)t

Which makes the rules akin to inductively sequential.

Original issue reported on code.google.com by ggr...@gmail.com on 28 Aug 2012 at 10:41

[GoogleCodeExporter]

r1706 fixes this.

Original comment by ggr...@gmail.com on 23 Aug 2013 at 11:19

• Changed state: Fixed
• Added labels: Milestone-Release1.5.3

[GoogleCodeExporter]

Support for suppressing duplicated refutations is added in r1744.

Original comment by ggr...@gmail.com on 26 Aug 2013 at 3:38

[GoogleCodeExporter]

r1719 added the `##bounds` pragma.

Original comment by ggr...@gmail.com on 26 Aug 2013 at 4:32