Typechecking of ENFORCE statement is incorrect

[hanjoosten]

I have been experimenting with the ENFORCE statement. However, in doing so, I got a fatal (while building a docker image):

#9 0.685 !             Ampersand-v4.6.2 [51c3de2e65c540ef026925fe8547c991765a5588:refs/tags/v4.6.2]
#9 0.685 Cannot unite (with operator "\/") expression l of type [Persoon*Tekst]
#9 0.685    ECpl (EDcD naam[Persoon*Tekst])
#9 0.686    with expression r of type [AanmeldingVluchteling*Persoon]
#9 0.686    EDcD betreft[AanmeldingVluchteling*Persoon]
#9 0.687 CallStack (from HasCallStack):
#9 0.687   fatal, called at src/Ampersand/Core/AbstractSyntaxTree.hs:1098:10 in ampersand-4.6.2-2iu3WivvGYHDzfozf1CZcu:Ampersand.Core.AbstractSyntaxTree
#9 0.689 2022-03-14 12:41:30.964209: [error] ExitFailure 2

The script I was editing has a clear type error, but the daemon didn't complain about it. Hence, I expect the root cause is that there is no proper type checking of the ENFORCE statement.

[stefjoosten]

@hanjoosten can you give an example in Ampersand source code?

[stefjoosten]

@hanjoosten can you make this reproducible for @sjcjoosten?

[hanjoosten]

Sure, The following example shows this behavior, because the types of the sources should match and the types of the targets should match as well:

CONTEXT Issue1281

r :: A*B
s :: C*D

ENFORCE r := s

ENDCONTEXT

This script passes the type checker, which it shouldn't. It then leads to the following runtime error in the compiler:

#0 12.37 !             Ampersand-v4.6.3 [6b132da7a8c1a3db946ed430f091aa2767e6111d:refs/heads/main]
#0 12.38 Cannot unite (with operator "\/") expression l of type [A*B]
#0 12.38    ECpl (EDcD r[A*B])
#0 12.38    with expression r of type [C*D]
#0 12.38    EDcD s[C*D]
#0 12.38 CallStack (from HasCallStack):
#0 12.38   fatal, called at src/Ampersand/Core/AbstractSyntaxTree.hs:1098:10 in ampersand-4.6.3-H9O277NO7RLHXAppxFGo3B:Ampersand.Core.AbstractSyntaxTree
#0 12.38 2022-06-12 06:28:19.793829: [error] ExitFailure 2

(details added by @stefjoosten)

[hanjoosten]

@sjcjoosten I have tried to fix this issue myself. I started the branch https://github.com/AmpersandTarski/Ampersand/tree/feature/typecheck-ENFORCE for this. I tried to get my head around this, and spend the whole aftenoon trying to find out how to do this. Very frustrating. I thought it would be easy, like the typecheck of the PEqu. But I underestimated. Could you please have a look at this?

[stefjoosten]

Here is another example, which I ran into in practice:

CONTEXT Issue1281

   CLASSIFY Vrijwilliger ISA Person

   RELATION personalia[AanmeldingVrijwilliger*Vrijwilliger]
   RELATION nationaliteit[Person*Tekst]
   RELATION nationaliteit[AanmeldingVrijwilliger*Tekst]
   ENFORCE nationaliteit[Person*Tekst] >: personalia~;nationaliteit
   
ENDCONTEXT

This script passes the type checker, as expected, and leads to the following runtime error in the compiler:

#0 12.21 !             Ampersand-v4.6.3 [6b132da7a8c1a3db946ed430f091aa2767e6111d:refs/heads/main]
#0 12.21 Cannot unite (with operator "\/") expression l of type [Vrijwilliger*Tekst]
#0 12.21    ECpl (ECps (EFlp (EDcD personalia[AanmeldingVrijwilliger*Vrijwilliger]),EDcD nationaliteit[AanmeldingVrijwilliger*Tekst]))
#0 12.21    with expression r of type [Person*Tekst]
#0 12.21    EDcD nationaliteit[Person*Tekst]
#0 12.21 CallStack (from HasCallStack):
#0 12.21   fatal, called at src/Ampersand/Core/AbstractSyntaxTree.hs:1098:10 in ampersand-4.6.3-H9O277NO7RLHXAppxFGo3B:Ampersand.Core.AbstractSyntaxTree
#0 12.22 2022-06-12 06:21:34.191626: [error] ExitFailure 2

[stefjoosten]

Workaround

There is an obvious workaround: Make sure the ENFORCE rule is type-safe without relying on ISA's. So the script I just gave can be compiled without problems if reformulated thus:

CONTEXT Issue1281

   CLASSIFY Vrijwilliger ISA Person

   RELATION personalia[AanmeldingVrijwilliger*Vrijwilliger]
   RELATION nationaliteit[Person*Tekst]
   RELATION nationaliteit[AanmeldingVrijwilliger*Tekst]
   ENFORCE nationaliteit[Person*Tekst] >: I[Person];personalia~;nationaliteit
   
ENDCONTEXT

[stefjoosten]

Alas, this issue has not been resolved completely. The example I gave does not compile. It still produces:

sjo00577@BA92-VYF9TXMD9G shouldSucceed % ampersand proto Issue1281.adl
Generating frontend...
!             Ampersand-v4.7.0 [Issue:b82c28936*]
Cannot unite (with operator "\/") expression l of type [Vrijwilliger*Tekst]
   ECpl (ECps (EFlp (EDcD personalia[AanmeldingVrijwilliger*Vrijwilliger]),EDcD nationaliteit[AanmeldingVrijwilliger*Tekst]))
   with expression r of type [Person*Tekst]
   EDcD nationaliteit[Person*Tekst]
CallStack (from HasCallStack):
  fatal, called at src/Ampersand/Core/AbstractSyntaxTree.hs:1098:10 in ampersand-4.7.0-HeXiIIWzFZvBuJb2jILIqi:Ampersand.Core.AbstractSyntaxTree
ExitFailure 2
sjo00577@BA92-VYF9TXMD9G shouldSucceed % 

Apparently you didn't test it, so I have now introduced this example into the regression test.

[hanjoosten]

@sjcjoosten, I found the root cause of this problem. It is where we extract the rules from the enforce statement. It can be found in this commit: 6c011ae .
However, I am not sure how to solve it. It might be a good idea to generate the rules in the type-checking stage because it has all type information available. How would you approach this?