hylo icon indicating copy to clipboard operation
hylo copied to clipboard

Refactor the "specialization" of members during conformance checking

Open kyouko-taiga opened this issue 1 year ago • 1 comments

During conformance checking, the type checker tries to match each requirement of the trait to an implementation of the conforming type. That is done by:

  1. inferring the type a requirement would have it was member of the conforming type;
  2. performing qualified name lookup (QNF) for the requirement's name in the conforming type;
  3. identifying a unique declaration with the type computed at step 1.

The computation of the type is done by calling TypeChecker.specialize with a substitution map associating the generic parameter of the trait (i.e., Self) to the conforming type.

Consider the following example:

trait T {
  type U
  fun f(_ x: U) -> Self
}

type A: T {
  public typelias U = Bool
  public f(_ x: Bool) -> A
}

When checking A : T, we create a substitution table [T.Self => A] and then use it to "specialize" the type of T.f, which is [remote let T.Self](Self.U) -> Self. That will give us [remote let A](Bool) -> A, which is the type of A.f.

Currently, specialization processes associated types with a QNF. It works in the above example because if we substitute T.Self by A, then QNF for U in A will find us Bool. Unfortunately, this trick doesn't work if we're looking for an associated type inherited by refinement. That's because the generic parameter of the refined trait won't match that of the refining trait.

Consider this example:

trait T {
  type U
}
trait S: T {
  fun f() -> U
}

Here, the return type of S.f is an associated type rooted in T. So substituting S.Self by the conforming type won't help us find the implementation of that associated type requirement.

We can workaround this problem by completing the substitution map for the generic parameter of all refined traits before calling TypeChecker.specialize. A better solution, though, would be to leverage the conformances we checked to substitute associated types. We can do that by looking at the trait declaring the associated type and searching for the associated conformance.

kyouko-taiga avatar Oct 21 '23 12:10 kyouko-taiga