Help required with getting typechecker correct again

[hanjoosten]

I am stuck with the branch called feature/namespaces-part1. This feature is mainly about creating a new type for Name. That type didn't exist, all names were of type Text. The new Name type now only takes texts that have exactly one word. Quoted names are not allowed any longer. Anyways, I have fixed all but one regressions tests. There is one that I don't know how to fix. It is related to the typechecker. See this log: https://github.com/AmpersandTarski/Ampersand/actions/runs/3689642307/jobs/6245815393

Reproduction:

• Check out the branch called feature/namespaces-part1.
• Compile it, and run the command ampersand check testing/Travis/testcases/Check/EnforceTest1.adl. It will give the following fatal:

!             Ampersand-v4.7.1 [feature/namespaces-part1:5ab818b06]
Cannot unite (with operator "\/") term l of type [Person*FirstName]:
    ECpl (EDcD personFirstName[Person*FirstName])
  with term r of type [NPReg*Voornaam]:
    ECps (EDcI NPReg,ECps (EEps NPReg [NPReg*NatuurlijkPersoon],EDcD npRoepnaam[NatuurlijkPersoon*Voornaam])).
CallStack (from HasCallStack):
  fatal, called at src/Ampersand/Core/AbstractSyntaxTree.hs:1104:10 in ampersand-4.7.1-FYNXYLnQnOhI95WuRjdoZE:Ampersand.Core.AbstractSyntaxTree
2022-12-26 14:40:43.770552: [error] ExitFailure 2
vscode@bf78d399085e:/workspaces/Ampersand$ 

@stefjoosten and/or @sjcjoosten , could you help in any way?

[stefjoosten]

Analysis

We made an error when we implemented the three ENFORCE statements:

ENFORCE r := p;q
ENFORCE r :< p;q
ENFORCE r >: p;q

The type checker requires that the type of r is greater than or equal to the type of the right-hand side expression. The code behind the type checker generated code in which r is equal to the type of the right-hand side expression. So, the problem was i-epsilon expressions were missing in the generated code.

Diagnosis

The type checker has been fixed by adding i-epsilon expressions to r, so the code behind the type checker matches the allowed expression

[stefjoosten]

Reflection

This error was known already half a year ago in Issue #1281. However, somebody closed that issue, so the error was never fixed.

[hanjoosten]

Strange indeed. I thought that test had been in the regression test set all the time. That was why I assumed I had broken something in doing the namespaces stuff. I am happy that this bug seems solved now. I can now continue with the namespace feature.

[hanjoosten]

For the record: This bug is solved now in the namespace branche. If for whatever reason that branch wouldn't make it to main eventually, then we need to cherrypick the fix @sjcjoosten made and get it into main. I assume that this is theoretically only.

[hanjoosten]

It still is strange. The bug isn't there in the current main branch. Proof is here. That said, the code that @sjcjoosten has changed isn't present in the main branch. Proof is here.

[sjcjoosten]

The bug surfaced because the conjuncts are calculated in the namespace branch, which causes the enforce rule to be translated into a complement with a disjunction. I don't have an explanation as to why there is a difference in which conjuncts are used and/or calculated for enforce rules between the main branch and the namespaces branch, it could be something as trivial as simply testing if there are any conjuncts through a pattern match, but the main branch does have the same bug. The way to expose it is to run:

ampersand proofs testing/Travis/testcases/Check/EnforceTest1.adl

Output is:

Generating Proof for EnforceTest1 into ./proofs_of_EnforceTest1.html...
!             Ampersand-v4.7.1 [main:0ebc600c5]
Cannot unite (with operator "\/") term l of type [NPReg*Voornaam]
   ECpl (ECps (EDcI NPReg,ECps (EEps NPReg [NPReg*NatuurlijkPersoon],EDcD npRoepnaam[NatuurlijkPersoon*Voornaam])))
   with term r of type [Person*FirstName]
   EDcD personFirstName[Person*FirstName]
CallStack (from HasCallStack):
  fatal, called at src/Ampersand/Core/AbstractSyntaxTree.hs:1096:10 in ampersand-4.7.1-Evu2DMMq1n0JnK2WkVlrg5:Ampersand.Core.AbstractSyntaxTree

[sjcjoosten]

I was thinking about how to get bugs of this category to surface. The category I have in mind is that of fatals (or errors, infinite loops, etc) in the fspec structure: I'm under the assumption that there shouldn't be any.

One reason this bug was hidden from view, is that Haskell calculates the fspec lazily. To avoid bugs of this category, asking whether the fspec is equal to itself should force evaluation of the entire fspec structure. That may have the downside that equality needs to be defined on structures for which we never want to calculate equality. There are also some classes in Haskell that help evaluate values into normal form, which might be an alternative way to achieve this goal.

[hanjoosten]

I think the explanation you gave makes sense. I have been working on making quite some data structures strict, using bang patterns (See this blog post. For the FSpec, that doesn't work, because it reveals an infinite loop in the normalizer, which isn't used. The bang pattern would be best to make strict. Your other option, to check for equality, isn't possible either because the FSpec contains functions, so equality is hard /impossible? to specify.

[sjcjoosten]

For the FSpec, that doesn't work, because it reveals an infinite loop in the normalizer, which isn't used currently.

Smells to me, food for a separate issue though (fixing the FSpec to get rid of this so we can fully evaluate FSpec).