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

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.

Start with the minimal example in owise.k and run kompile --syntax-module OWISE-SYNTAX owise.k to reproduce the totality-checker warning. Trace how the foo rules are analyzed, then confirm that the sufficiently complete functional definition no longer emits the warning without the owise rule.