[K-Bug] Broken "Non-exhausive match" warning

[virgil-serbanuta]

What component is the issue in?

Front-End

Which command

• kompile
• kast
• krun
• kprove
• kprovex
• ksearch

What K Version?

K version: v7.1.104-0-g34892bf1cc Build date: Mi aug 14 01:57:38 EEST 2024

Operating System

Linux

K Definitions (If Possible)

a.k:

module A
    syntax Item ::= "item"
    syntax ItemList ::= List{Item, ","}

    syntax ItemList ::= reverse(ItemList)  [function, total]
                      | #reverse(ItemList, ItemList)  [function, total]
    rule reverse(L:ItemList) => #reverse(L, .ItemList)
    rule #reverse(.ItemList, R) => R
    rule #reverse((P:Item , L:ItemList), R)
        => #reverse(L, (P , R))

    syntax A  ::= "a"
                | b(ItemList)
    rule a => b((item))
endmodule

Steps to Reproduce

$ kompile a.k
[Warning] Compiler: Non exhaustive match detected:
`#reverse(_,_)_A_ItemList_ItemList_ItemList`(_,_)
        Source(/mnt/data/pi-squared/rust-demo-semantics/tmp/a.k)
        Location(6,25,6,72)
        6 |                           | #reverse(ItemList, ItemList)  [function, total]
          .                             ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Note that if the parentheses around item in rule a => b((item)) are removed, the warning dissapears.

Expected Results

No "Non-exhausive match" warning.