Insert pattern is not validated if match fails in match-insert

[james-whiteside]

Description

If I run a match-insert query against a database and the match fails, the server gives a normal response, even if the insert pattern is not valid. Example is given below.

Environment

1. OS (where TypeDB server runs): MacOS 12.6.1
2. TypeDB version (and platform): TypeDB Core 2.19.1
3. TypeDB client: Client Python 2.18.2

Reproducible Steps

Steps to create the smallest reproducible scenario:

1. Define schema:

define
person sub entity, owns name;
name sub attribute, value string;
phone sub attribute, value string;

1. Run query:

match
$p isa person, has name "Kevin";
insert
$p has phone "+44 (0)7123 456 789";

Expected Output

Error is thrown as person does not own phone.

Actual Output

TypeDB gives normal response (no inserts performed).

[flyingsilverfin]

This would actually be quite cool if we ran full type inference on 'insert' queries as well - would be a great watch to solve this problem in generality!

[flyingsilverfin]

Note: this may not be doable efficiently

We want to perform the following type check:

1. Make sure there are no permutations of types generatable by the match that are invalid in the insert or delete.

This can be formulated that this query returns no answers:

match
$x-type...
$y-type...
$z-type...
not {
  ... insert typing requirements
}

This can be very expensive since all permutations of types for x/y/z will be checked against the not. It is slightly more efficient if the traversal engine can know when to perform the negation checks, rather than doing it after every completed match permutation.

Relatedly, this is the same issue as faced by efficient rule validation: https://github.com/vaticle/typedb/issues/6387