During reasoning, nested patterns are not correctly bound if the variable skips a level

[farost]

Description

There exists a strange combination of factors when inference can cause the reasoner to act just like it ignores a not subquery, leading to incorrect results.

I have a query that can only logically return the max result equal to 1 as I only have 2 entities of a type I fetch and I have a not {$subm2 is $subm1;}; line in my condition. However, a combination of inference, rules, and this specific line creates a strange case when I get 2 as a result.

Environment

1. TypeDB distribution: Core
2. TypeDB version: 2.28.0
3. Environment: Mac
4. Client and version: Studio, Console, Java Driver
5. Other details:

Reproducible Steps

1. Set up
   schema:

define

submission sub entity,
    owns id,
    owns name,
    plays measurement:submission;
    
server sub entity,
    owns id,
    owns name,
    plays measurement:server;
    
metadata sub entity,
    owns name,
    plays measurement:additional;
    
measurement sub relation,
    relates submission,
    relates server,
    relates additional;
    
id sub attribute, value string;
name sub attribute, value string;

rule my-rule: 
    when {
        $m isa metadata;
        $subm isa submission, has name $name;
        (submission: $subm, additional: $m) isa measurement;
    } then {
        $m has $name;
    };

data:

insert
$serv1 isa server, has id "1", has name "server";
$sub1 isa submission, has id "1", has name "first";
$sub2 isa submission, has id "2", has name "second";
$m1 isa metadata;
$m2 isa metadata;

($sub1, $serv1, $m1) isa measurement;
($sub2, $serv1, $m2) isa measurement;

2. Execute a query with inference turned on!

query:

match 
$s isa server;
$subm1 isa submission, has name $name1;
($s, $subm1) isa measurement;
not {
    $subm2 isa submission, has name $name2;
    ($s, $subm2) isa measurement;
    not {$subm2 is $subm1;};
    $name1 > $name2;
};
get
$subm1; count;

3. Unexpected result
   Result> Get Aggregate query successfully calculated:
   2

4. Expected result
   Result> Get Aggregate query successfully calculated:
   1

Additional information

If we turn additional reasoner logs on, we can see:

================================================= Start reasoner plans =================================================
(root-query)::[]

Branch 1:
|	Cost for all []:	94.0
|	[0]	RETRIEVABLE	[]
|		{ $_0 ($s, $subm1); $_0 isa measurement;  $name1 isa name;  $subm1 has $name1; $subm1 isa submission;  $s isa server; }
|	
|	[1]	NEGATION	[$name1, $s]
|	|	Cost for all [$name1, $s]:	56.0
|	|	[0]	RETRIEVABLE	[$name1, $s]
|	|		{ $_1 isa measurement; $_1 ($s, $subm2);  $subm2 has $name2; $subm2 isa submission;  $name1 > $name2;  $name2 isa name; }
|	|	
|	|	[1]	NEGATION	[$subm2]
|	|	|	Cost for all [$subm2]:	8.0
|	|	|	[0]	RETRIEVABLE	[$subm2]
|	|	|		{ $subm2 is $subm1; }
|	|	|	
|	|	
|	


------------------------------------------------------------------------------------------------------------------------
=================================================  End reasoner plans  =================================================

However, everything works good if I comment out this line:

#    not {$subm2 is $subm1;};

Logs for this case:

================================================= Start reasoner plans =================================================
(root-query)::[]

Branch 1:
|	Cost for all []:	72.0
|	[0]	RETRIEVABLE	[]
|		{ $_0 ($s, $subm1); $_0 isa measurement;  $name1 isa name;  $subm1 has $name1; $subm1 isa submission;  $s isa server; }
|	
|	[1]	NEGATION	[$name1, $s]
|	|	Cost for all [$name1, $s]:	24.0
|	|	[0]	RETRIEVABLE	[$name1, $s]
|	|		{ $_1 isa measurement; $_1 ($s, $subm2);  $subm2 has $name2; $subm2 isa submission;  $name1 > $name2;  $name2 isa name; }
|	|	
|	


------------------------------------------------------------------------------------------------------------------------
=================================================  End reasoner plans  =================================================

[krishnangovindraj]

We've isolated the problem to bounds not being passed into nested patterns if they don't occur at every level.
Here, $subm1 is not passed into the negation, leading to a trivially satisfiable $subm1 is $subm2 in the nested negation.

================================================= Start reasoner plans =================================================
(root-query)::[]

Branch 1:
|	Cost for all []:	94.0
|	[0]	RETRIEVABLE	[]
|		{ $_0 ($s, $subm1); $_0 isa measurement;  $name1 isa name;  $subm1 has $name1; $subm1 isa submission;  $s isa server; }
|	
|	[1]	NEGATION	[$name1, $s]
|	|	Cost for all [$name1, $s]:	56.0
|	|	[0]	RETRIEVABLE	[$name1, $s]
|	|		{ $_1 isa measurement; $_1 ($s, $subm2);  $subm2 has $name2; $subm2 isa submission;  $name1 > $name2;  $name2 isa name; }
|	|	
|	|	[1]	NEGATION	[$subm2]
|	|	|	Cost for all [$subm2]:	8.0
|	|	|	[0]	RETRIEVABLE	[$subm2]
|	|	|		{ $subm2 is $subm1; }
|	|	|	
|	|	
|	


------------------------------------------------------------------------------------------------------------------------
=================================================  End reasoner plans  =================================================

An easy workaround is to artificially bind the query in the intermediate level:

match 
$s isa server;
$subm1 isa submission, has name $name1;
($s, $subm1) isa measurement;
not {
    $subm1 is $dummy-to-bind-subm1; # Dummy to force the bounds in.
    $subm2 isa submission, has name $name2;
    ($s, $subm2) isa measurement;
    not {$subm2 is $subm1;};
    $name1 > $name2;
};
get
$subm1; count;