[Bug] [kompile] - kompile emits a "Non exhaustive match detected" warning for a seemingly sufficiently complete function definition

[malturki]

K Version

$ kompile --version
K version:    5.2.97
Build date:   Sun Mar 06 11:36:17 CST 2022

Description

kompile emits a "Non exhaustive match detected" warning seemingly unnecessarily in some cases (see the minimal example below). The function for which it gives the warning is declared functional and is sufficiently completely specified as far as I can tell.

Note: when uncommenting the owise line in the example below, the warning is not shown. But it shouldn't be needed, I think.

Input Files

The owise.k file below:

module OWISE-SYNTAX
  syntax T ::= "uint"
  syntax TList ::= List{T, ""} [klabel(list)]
endmodule

module OWISE
  imports OWISE-SYNTAX

  syntax MaybeT     ::= T | "NoT"
  syntax MaybeTList ::= List{MaybeT, ""} [klabel(list)]
  syntax MaybeTList ::= TList

  syntax MaybeTList ::= foo(MaybeTList) [function, functional]
  // ---------------------------------------------------------
  rule foo(.MaybeTList)            => .MaybeTList
  rule foo(_:MaybeT TL:MaybeTList) => uint foo(TL)
  //rule foo(TL) => TL [owise] // to suppress a totality checker warning
endmodule

Reproduction Steps

kompile --syntax-module OWISE-SYNTAX owise.k

Expected Behavior

No "Non exhaustive match detected" warning is emitted.

[dwightguth]

This is probably because the exhaustiveness check is not interacting correctly with the overloaded syntax, so it thinks that the rule won't match a TList. This is actually a bug in the llvm backend, but we can look into it.

[malturki]

Thanks for the feedback. Obviously this is not high priority, but I thought I should have it confirmed and documented.

[dwightguth]

http://cambium.inria.fr/~maranget/papers/warn/warn.pdf

[radumereuta]

@Baltoli whenever you have time, this could help you get familiar with the llvm backend.
@dwightguth can provide assistance.

[Baltoli]

Possibly needs replication; will most likely still occur though.

@dwightguth suggests that the trick here is to modify the exhaustiveness algorithm somehow but that the fix might not be obvious.

[virgil-serbanuta]

Here is one more example, extracted from the wasm semantics:

a.k

module A

  syntax A ::= "a" | B
  syntax B ::= "b"
  syntax Bs ::= List{B, ""}
  syntax As ::= List{A, ""}
  syntax As ::= Bs

  syntax K ::= f(As)  [function, total]

  rule f(.As) => .K
  rule f(A AA) => A ~> f(AA)

endmodule

Command line:

$ kompile a.k --backend llvm
[Warning] Compiler: Non exhaustive match detected:
`f(_)_A_K_As`(`.List{"___A_As_A_As"}_As`(.KList))
        Source(/mnt/data/runtime-verification/elrond-wasm-real-elrond/kmxwasm/tmp/a.k)
        Location(9,16,9,40)
        9 |       syntax K ::= f(As)  [function, total]
          .                    ^~~~~~~~~~~~~~~~~~~~~~~~

The same warning shows up if the two list productions have the [klabel(stuff)] attribute (the original rules in the WASM semantics have it) and if one adds rule f(B:Bs) => B to the semantics.