Statix messages change constraint evaluation

[JFKakaJFK]

Summary

Sometimes the presence of feedback messages as per Spoofax 2 docs causes drastic changes in the type checking.
For example, if typeOfExp(s, e) == _ works, then typeOfExp(s, e) == _ | error $[Invalid expression] breaks (as in returns an error for the same input).

What you did

I ran into this when defining static semantics for the chocopy language.
I played around with making the basic types such as int etc. part of the class hierarchy and modelled them using scopes as types. This broke my type checking and it turned out that feedback messages were the cause of this.

What you expected to happen

I would expect 1 * 1 to type check given this syntax definition

module start

context-free start-symbols

  Start

context-free sorts

  Start
  Exp

context-free syntax

  Exp.Int = NUM
  Exp.Mul = <<Exp> * <Exp>> {left}
  
  Start.Exp = Exp

lexical sorts ID NUM

lexical syntax

  ID = [a-zA-Z]+
  NUM = [0-9]+

  LAYOUT = [\ \n\v\f\r\t]

lexical restrictions
  ID  -/- [a-zA-Z]
  NUM -/- [0-9]

context-free restrictions

  LAYOUT? -/- [\ \n\v\f\r\t\#]

and this static code

module main

imports
  signatures/start-sig

signature
  sorts
    TYPE

  constructors
    CLASS : scope * ID -> TYPE
    INT : TYPE
  
  relations
    type : ID -> TYPE

rules
  int  : scope -> TYPE
  int(s) = T :- 
    typeOfType(s, "int") == T@CLASS(_, "int").

rules
  typeOfExp : scope * Exp -> TYPE
  typeOfExp(s, e@Int(_)) = I :-
    int(s) == I,
    @e.type := I.
  typeOfExp(s, e@Mul(l, r)) = int(s) :-
    typeOfExp(s, l) == int(s), // adding error feedback here breaks things too
    typeOfExp(s, r) == int(s), // | error $[Expected "int"],
    @e.type := int(s).

  // not having class types works, but defeats the purpose
  /*
  typeOfExp(s, e@Int(_)) = INT() :-
    @e.type := INT().
  typeOfExp(s, e@Mul(l, r)) = INT() :-
    typeOfExp(s, l) == INT() | error $[Expected [INT()]]@l,
    typeOfExp(s, r) == INT() | error $[Expected [INT()]]@r,
    @e.type := INT().
  */

rules
  programOk : Start
  programOk(Exp(e)) :- {s int}
    new s int,
    declareClass(s, "int", int),
    //  no message works
    // typeOfExp(s, e) == _.
    // this fails
    typeOfExp(s, e) == _ | error $[Invalid expression].
    // fails too
    // try { typeOfExp(s, e) == _ } | error $[Invalid expression].

rules
  declareClass : scope * ID * scope
  declareClass(s, id, c) :- {C}
    !type[id, C@CLASS(c, id)] in s,
    resolveType(s, id) == [(_, (_, C))]
      | error $[Duplicate declaration of type [id]],
    @id.type := C.
  
  resolveType : scope * ID -> list((path * (ID * TYPE)))
  resolveType(s, id) = ps :-
    query type
      filter e and {id' :- id' == id}
      min and true
    in s |-> ps.
  
  typeOfType : scope * ID -> TYPE
  typeOfType(s, id) = T :- {id'}
    resolveType(s, id) == [(_, (id', T))]
      | error $[Undefined type [id]],
    @id.type := T, @id.ref := id'.

What actually happened

I got the error

Description	               Resource	       Path	                                Location	  Type
Expected "int"<be>       example.bg	/bug_report/examples	Unknown	  Spoofax dynamic error marker

However, without error feedback, the outcome is as expected.

Context

• Spoofax version: 0.15.2
• Operating system & version: Windows 10 Pro (Version 21H1, OS Build 19043.1288)
• Java version (if applicable): Spoofax 3 embedded JVM
• Eclipse version (if applicable): 2021-09 (4.21.0) (Build id: 20210910-1417)

Additional information

The example Spoofax project can be found here and another version with more cases of hopefully the same bug here.

[AZWN]

Thanks for reporting. Indeed there is an issue that properties cannot be assigned to non-AST terms, such as the "int" in your int() predicate. These are ignored by default, setting a custom message on a parent constraint incorrectly overrides that. See also the announcement on Mattermost.

I created another issue in the NaBL repository.

@Gohla I'd prefer to keep this issue open, because some error message code is duplicated, and perhaps I need to update the Spoofax 3 implementation as well.

[AZWN]

Should be fixed by 4d06d2.

Spoofax 3 correctly reuses these results (either by direct invocation or via the STX_extract_messages primitive), so the issue can be closed once the changes are merged in.