[K-Bug] `#let`, `#as`, and `#fun` break type safety

Start by running kompile on the three reproductions: test-let.k, test-as.k, and test-fun.k. Trace the front-end type checking for #let, #as, and #fun, using the shown outputs as the expected behavior. Done means each invalid use reports a type error instead of compiling with only a warning or no diagnostic.

What component is the issue in?

Front-End

Which command

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

What K Version?

v6.0.137

Operating System

Linux

K Definitions (If Possible)

test-let.k

module TEST-LET
syntax Void
syntax Foo ::= foo()
syntax Top ::= start()
             | Evil(Void)

rule start() => #let X = foo() #in Evil(X)
endmodule

test-as.k

module TEST-AS
syntax Void
syntax Top ::= start()
             | Evil(Void)

rule start() #as X => Evil(X)
endmodule

test-fun.k

module TEST-FUN                                                                                                                                                                                             
syntax Void
syntax Foo ::= foo()
syntax Top ::= start()
             | Evil(Void)                                                                                                                                                                                   

rule start() => #fun(X => Evil(X))(foo())
endmodule

Steps to Reproduce

• kompile test-let.k --main-module TEST-LET --syntax-module TEST-LET
  • Output: [Warning] Compiler: Non exhaustive match detected: `#lambda__`(_)
• kompile test-as.k --main-module TEST-AS --syntax-module TEST-AS
  • Output:
• kompile test-fun.k --main-module TEST-FUN --syntax-module TEST-FUN
  • Output: [Warning] Compiler: Non exhaustive match detected: `#lambda__`(_)

Expected Results

We should report a type error in all cases.

test-let.k

[Error] Inner Parser: Unexpected sort Foo for variable X. Expected: Void
	Source(test-let.k)
	Location(7,41,7,42)
	7 |	rule start() => #let X = foo() #in Evil(X)
	  .	                                        ^
[Error] Compiler: Had 1 parsing errors.

test-as.k

[Error] Inner Parser: Unexpected sort Top for variable X. Expected: Void
	Source(test-as.k)
	Location(6,28,6,29)
	6 |	rule start() #as X => Evil(X)
	  .	                           ^
[Error] Compiler: Had 1 parsing errors.

test-fun.k

[Error] Inner Parser: Unexpected sort Foo for term parsed as production syntax 
Foo ::= "foo" "(" ")" [klabel(foo)]. Expected: Void
	Source(test-let.k)
	Location(7,36,7,41)
	7 |	rule start() => #fun(X => Evil(X))(foo())
	  .	                                   ^~~~~
[Error] Compiler: Had 1 parsing errors.