eval: unification rule doesn't hold (X & X != X)

[loisch]

I think the underlying cause for the bad performance in #3654 is a correctness issue with the evaluator. #3672 shows a problem with evalv3 but this issue shows an independent correctness problem with the current evaluator.

What version of CUE are you using (cue version)?

$ cue version
cue version v0.11.1

go version go1.23.4
      -buildmode exe
       -compiler gc
       -trimpath true
  DefaultGODEBUG asynctimerchan=1,gotypesalias=0,httpservecontentkeepheaders=1,tls3des=1,tlskyber=0,x509keypairleaf=0,x509negativeserial=1
     CGO_ENABLED 1
          GOARCH arm64
            GOOS darwin
         GOARM64 v8.0
cue.lang.version v0.11.1

Does this issue reproduce with the latest stable release?

Yes.

What did you do?

The following testscript shows that for term X = (*null | #FinDefSetOfConfigText) and some term Z the expression X & X & Z doesn't have the same value than just X & Z which violates rule 1 according to the definition for Unification in the CUE language specification (The unification of a with itself is always a.)

Both values (works2 and fails1) should be equal but they are not:

works2: (*null | #FinDefSetOfConfigText) & { Only: [{ UseSectionName: true }] } 
fails1: (*null | #FinDefSetOfConfigText) & (*null | #FinDefSetOfConfigText) & { Only: [{ UseSectionName: true }] }

I know that changing the program to

--- ../correctness.txtar	2025-01-13 17:02:22.106978377 +0100
+++ ../correctness2.txtar	2025-01-13 17:13:08.510166130 +0100
@@ -35,7 +35,7 @@
 		if (IN & string) != _|_ {
 			IN
 		},
-		if IN.UseSectionName != _|_ {
+		if (IN & {UseSectionName:_}) != _|_ {
 			"UseSectionName"
 		}
 	][0]

solves the issue. I don't know why because the surrounding definition #orgForConfigText is only used with newly constructed values (in the list comprehension) so the accidental unification of IN / source with {UseSectionName:_} shouldn't change anything.

But the important issue is that X & X & Z != X & Z.

exec cue export out.cue -e works1
exec cue export out.cue -e works2
exec cue export out.cue -e works3
! exec cue export out.cue -e fails1
! exec cue export out.cue -e fails2

-- out.cue --
import "strings"

#ConfigText: string | {UseSectionName: true}

#ConfigTextRule: #ConfigText | {Append: #ConfigText}

#FinDefSetDefinition: {
	#Alternatives: {
		only: {
			Only: [...#ConfigTextRule]
			let xs = [for x in Only {(#orgForConfigText & {source: x}).orgSyntax}]
			let str = strings.Join(xs, "\",\"")
			orgSyntax: "Only [\(str)]"
		}
	}
}

#mkFinDefSet: {
	#Definition!: #FinDefSetDefinition
	#Type: or([for _, v in #Definition.#Alternatives {v}])
}

#FinDefSetOfConfigText: #mkFinDefSet.#Type

#orgForConfigText: {
	IN=source: #ConfigText
	orgSyntax: [
		if (IN & string) != _|_ {
			IN
		},
		if IN.UseSectionName != _|_ {
			"UseSectionName"
		}
	][0]
}

works1: #FinDefSetOfConfigText & { Only: [{ UseSectionName: true }] } 
works2: (*null | #FinDefSetOfConfigText) & { Only: [{ UseSectionName: true }] } 
works3: (*null | #FinDefSetOfConfigText) & #FinDefSetOfConfigText & { Only: [{ UseSectionName: true }] } 
fails1: (*null | #FinDefSetOfConfigText) & (*null | #FinDefSetOfConfigText) & { Only: [{ UseSectionName: true }] }
fails2: #FinDefSetOfConfigText & (*null | #FinDefSetOfConfigText) & { Only: [{ UseSectionName: true }] }

What did you expect to see?

Failing testscript where all checks either fail or succeed.

What did you see instead?

Passing testscript showing that evaluation order matters and/or unifying a term with itself changes the meaning.

[myitcv]

Passing testscript showing that evaluation order matters and/or unifying a term with itself changes the meaning.

Thanks again for the hugely detailed repro, @loisch. I observed something similar en route to debugging #3672, but opted to reduce further to what is possibly/likely the core issue. That said, there might still be an issue of the sort you describe.

There are a number of issues swirling in this space of evalv3 right not, including #3672. Subject to @mpvl or @mvdan agreeing/disagreeing, I suggest we let that swirl settle and then revisit the bug raised in this issue.