[K-Bug] “Cannot define constructor: sort has domain values”

[jeanas]

What component is the issue in?

haskell-backend

Which command

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

What K Version?

5.6.90

Operating System

Linux

K Definitions (If Possible)

module BUG-SYNTAX
  import ID-SYNTAX
endmodule

module BUG
  imports BUG-SYNTAX
  syntax Id ::= Foo(Id)
endmodule

Steps to Reproduce

$ kompile --backend haskell bug.k
kore-exec: [39759] Error (ErrorVerify):
    Error:
      module 'BUG':
      symbol 'LblFoo'LParUndsRParUnds'BUG'Unds'Id'Unds'Id' declaration (definition.kore 93:10):
        Cannot define constructor LblFoo'LParUndsRParUnds'BUG'Unds'Id'Unds'Id for sort SortId{}: sort has domain values.
Created bug report: kore-exec.tar.gz
[Error] Critical: Haskell backend reported errors validating compiled
definition.
Examine output to see errors.

Note that this is probably a legitimate error, but the error message seems to be asking me to report a bug.

It might be that the error should have been caught earlier.

This does not occur in the LLVM backend. I don't know if that's expected.

Expected Results

Either no error, or a proper error message instead of an internal error.

[radumereuta]

You are correct. The haskell backend complains that you are extending a token sort with a constructor.
If you write syntax Id ::= Foo(Id) [function], then it's going to kompile just fine.

We need to add a check in the front end. Maybe here:
https://github.com/runtimeverification/k/blob/master/kernel/src/main/java/org/kframework/kompile/Kompile.java#L421

[gtrepta]

Why is this ok on the llvm backend but not the haskell backend? Should token sorts be allowed to have non-function productions?

[Robertorosmaninho]

From @dwightguth: It shouldn't be allowed in llvm-backend as well. It should be blocked by the frontend.

[Robertorosmaninho]

The problem here is that we identify and print the sort that must contain domain values here. But this information isn't available easily in any part of the code.