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

[Scott-Guest]

What component is the issue in?

Front-End

Which command

• [X] 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.

[Scott-Guest]

The root of the issue here is that the binders in #let, #as, and #fun require more involved sorting rules than what a syntax production can describe.

In particular, treating these like any other production results in the the sort parameter for the binder being widened to the point that anything type checks:

test-let.k

• syntax {S1, S2} S1 ::= "#let" S2 "=" S2 "#in" S1
• #let X = foo() #in Evil(X) constrains sort(X) <: S2, Foo <: S2, Top <: S1
• Evil(X) constrains sort(X) <: Void
• Solved by letting sort(X) = Void, S1 = Top, and S2 = KItem

test-as.k

• syntax {S} S ::= S "#as" S
• start() #as X constrains Top <: S and sort(X) <: S
• Evil(X) constrains sort(X) <: Void
• Solved by letting sort(X) = Void and S = KItem

test-fun.k

• syntax {S} S ::= "#fun" "(" S ")" "(" S ")"
• #fun(X => Evil(X))(foo()) constrains sort(X) <: S, Top <: S, Foo <: S
• Evil(X) constrains sort(X) <: Void
• Solved by letting sort(X) = Void, S = KItem

Instead, we need to treat these forms as special cases during type inference.

[Baltoli]

The warnings about totality here seem to be separate bugs related to #3798; those cases should be fixed on their own merit.

As best I can tell, the problem is when we have a term like:

#let X = ... #in RHS(X)

the usage of X in the term RHS constrains the sort of X, making the underlying lambda non-total. We should identify a reproducing example that doesn't break the type system, then fix the implementation in #3798 to be stricter about what gets marked as total.

So far I'm not able to reproduce the totality warning without also breaking type safety, so let's fix the inference issue here first then look for any totality warnings that sneak back through.

[Baltoli]

Do we want to allow let-polymorphism? Work through an example; probably fine to just monomorphise for now - if we desperately need it then allow, but too complex to do for its own sake.

[Baltoli]

Leaving this for now until we remove the Z3 inferencer - the old version does the wrong thing as well so fixing this in the new version will complexity the equivalence check between versions.

[Scott-Guest]

Blocked on #3848