Open hanjoosten opened 2 years ago
@hanjoosten can you give an example in Ampersand source code?
@hanjoosten can you make this reproducible for @sjcjoosten?
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)
@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?
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
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
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.
@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: https://github.com/AmpersandTarski/Ampersand/commit/6c011ae124f9ecfadb108039be5d37ab4e4c5439 . 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?
I have been experimenting with the ENFORCE statement. However, in doing so, I got a fatal (while building a docker image):
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.