Typechecker mistakenly reports type error for well-typed program with generic ADT

[sungshik]

Describe the bug

The following test mistakenly fails (i.e., the typechecker reports a type error, but the program is well-typed):

test bool falsePositive() = checkModuleOK("
    module FalsePositive /**/
        data D[&T] = d(&T n);
        int f() {
            n1 = d(5).n;
            n2 = n1;
            n3 = n2;
            return n3 + 5;
        }
    ");

// Typechecker reports type error: "Addition not defined on `&T` and `int`"

The " /**/" is needed to force Typepal to schedule calcs/reqs in a particular order. Without it, the test succeeds.

To Reproduce

Run the test. See also: #2869.

Expected behavior

The test should succeed.

[sungshik]

Preliminary analysis

Depending on the order in which calcs/reqs are scheduled by Typepal's solver, the type of the field access in the statement n1 = d(5).n will either be set to int (if &T has already been instantiated) or to &T (if it hasn't; in this case, it will be instantiated later).

• Case 1: In the former case, int is propagated downstream, from n to d(5).n, n1, n2, and n3. As a result, no type error is reported for the addition.
• Case 2: In the latter case, first, &T is propagated downstream. Next, &T is instantiated to int, and the type of n is updated accordingly. However, this update isn't propagated downstream. As a result, a type error is reported for the addition.

Intuitively, a solution direction could be to register additional dependencies for the calc of the field access to make sure that &T has already been instantiated. This would eliminate case 2. There are several complications, though:

• In general, it doesn't seem to be possible to determine for a field access in isolation (without considering the context in which it takes place) whether or not &T is an admissible type. For instance, in the falsePositive test, it is inadmissible. However, for the following function, it is admissible:

  data D[&T] = d(&T n);
  &T f(D[&T] d) = d.n;

• Typepal's solver automatically propagates types of definitions to their uses. For instance, when the solver determines the type of field n in the ADT is &T (definition location), that type is automatically propagated to the field access (use location), which is later overwritten when the separate calc for the field access is evaluated.