Assignment from keyword field of type `&T` to variable of type not-`&T` is mistakenly well-typed

[sungshik]

Describe the bug

The following test currently succeeds:

rascal/src/org/rascalmpl/compiler/lang/rascalcore/check/tests/DataDeclarationTCTests.rsc

Lines 487 to 491 in 22b7a02

	test bool ADTWithTypeParameterAndKW3() = checkModuleOK("
	module ADTWithTypeParameterAndKW3
	data D[&T] = d1(&T n, &T kw = n);
	void f() { D[int] x = d1(10); str m = x.kw; }
	");

However, it should fail, because:

• &T is bound to int;
• the type of x.kw is int;
• the type of m is str.

A preliminary investigation suggests that the req that compares the types of m and x.kw is triggered too early by the solver (when it hasn't established yet that &T is bound to int), possibly because of a missing dependency. Need to look into this in more detail.

To Reproduce

Run the test.

Expected behavior

The test should fail.

[sungshik]

Analysis

The following seems to happen:

1. The expected type of m is determined to be str
2. The actual type of x.kw is determined to be &T
3. The requirement that the actual type of x.kw is a subtype of the expected type of m is evaluated to true. This is because "is a subtype of" includes instantiation of type parameters. Relevant line:
   

   rascal/src/org/rascalmpl/compiler/lang/rascalcore/check/ComputeType.rsc

   Line 122 in 22b7a02

   initialTypeU = instantiateRascalTypeParameters(var, initialTypeU, bindings, s);

   
   That is, initialTypeU is &T, so &T is locally (only for the duration of the subtyping check) instantiated to str.
4. &T is globally instantiated to int
5. The test succeeds, because the requirement of step 3 isn't re-evaluated after step 4.

What should happen, is that step 4 precedes step 3. If so, then the requirement evaluates to false, and the test fails. The dependency that ensures that ordering seems to be missing.

Problem

We can distinguish two kinds of dependencies of calculators/requirements:

• Syntactic dependencies are locations for which a type must be available in tm.facts. Syntactic dependencies are declared in the signatures of calculators/requirements as list[loc] fields.
• Semantic dependencies are locations for which the available types in tm.facts are, additionally, "ready to be used". Semantic dependencies are declared in the bodies of calculators/requirements as if (...) throw TypeUnavailable(); statements.

In the case of this issue, all syntactic dependencies are properly declared, but some semantic dependencies aren't. For instance, in the example above:

• In step 1, the type of m becomes available (first syntactic dependency fulfilled)
• In step 2, the type of x.kw becomes available (second syntactic dependency fulfilled)
• In step 3, all syntactic dependencies of the requirement are fulfilled, so it is evaluated. However, this is premature: even though the type of x.kw is available, it is not "ready to be used", as the type parameter still needs to be instantiated. In other words, a semantic dependency is missing.

In general, there are likely to be many places in the Rascal typechecker where semantic dependencies of this kind aren't declared yet.

Solution

After discussion with @PaulKlint, we came up with the following solution for now.

• A: Add a utility function that checks the semantic dependency that all type parameters are instantiated, of this form:

  AType getInstantiated(Tree tree, Solver s) {
      AType t= s.getType(tree);
      if (isInstantiated(t)) {
          return t;
      } else {
          throw TypeUnavailable();
      }
  }

• B: Check all places where s.getType(...) is currently called and determine if the type should already be instantiated to count as "ready to be used". If so, then this semantic dependency must be declared by replacing the s.getType(...) call with a getInstantiated(..., s) call.

It isn't obvious if/that/how Typepal can be extended with additional support for declaring and checking semantic dependencies. For the Rascal typechecker, the bulk of the work is point B anyway, so if later we think of an effective way to incorporate semantic dependency checking in Typepal (or generalize otherwise), then it should be straightforward to adopt it.

[sungshik]

The solution turns out to be too naive. It rests on the assumption it is possible to determine for any location whether or not an uninstantiated &T is an admissible type by only considering the location in isolation (without considering the context in which it takes place). This assumption is false. For instance, &T is an admissible type for the field accesses in the following examples:

test bool Box() = checkModuleOK("
    module Box
        data Box[&T] = box(&T v);
        &T unbox(Box[&T] b) = b.v;
    ");

test bool NumBox() = checkModuleOK("
    module NumBox
        data NumBox[&T \<: num] = box(&T v);

        &T \<: num unboxAndSum(NumBox[&T \<: num] box1, NumBox[&T \<: num] box2) {
            &T v1 = box1.v;
            &T v2 = box2.v;
            return v1 + v2;
        }
    ");