Match with duplicate variables
Opened this issue · 1 comments
BrunoDutertre commented
Not sure what's intended but nothing is checking for duplicate variables in a match pattern.
So this is allowed:
(declare sort type)
(declare term type)
(declare cons (! t term (! u term term)))
(declare Bool sort)
(program bad ((t term)) sort (match t ((cons x x) Bool)))
Unfortunately, allowing this can lead to bad results for the same reason as in issue #67:
(declare sort type)
(declare term type)
(declare cons (! t term (! u term term)))
(declare Bool sort)
(declare x type)
(program bad ((t term)) sort (match t ((cons x x) Bool)))
(declare b x)
This fails to check.
ajreynol commented
We should disallow duplicate variables here.