Checking if `DependentMemberType` conformance requirement is satisfied by SubstitutionMap

Development Compiler
1

Hi compiler experts,

I'm wondering how to check (in a SIL transform) whether a conformance requirement with a DependentMemberType lhs type is satisfied either in a given SubstitutionMap or in a given module.

Context is the following program. 1 shows the array of Requirements and 2 shows the substitution map. The "given module" is the current module.

// In stdlib:
// protocol Differentiable {
//   associatedtype TangentVector: Differentiable & AdditiveArithmetic
//       where ...
// }

protocol MyProtocol {
  associatedtype Scalar
}
extension MyProtocol where Scalar : FloatingPoint {
  // 1. `@differentiable` attribute declares an array of `Requirement`s in
  //    a trailing where clause.
  //
  //    Relevant to the question: the `Self.TangentVector : MyProtocol`
  //    requirement is a conformance requirement, where the lhs
  //    `Self.TangentVector` is a `DependentMemberType` type:
  //
  // (dependent_member_type assoc_type=Swift.(file).Differentiable.TangentVector
  //   (base=generic_type_param_type depth=0 index=0 decl=main.(file).MyProtocol extension.Self))
  @differentiable(
    where Self : Differentiable, Scalar : Differentiable,
          Self.TangentVector : MyProtocol
  )
  static func +(lhs: Self, rhs: Self) -> Self { ... }
}

struct Dummy<Scalar> : MyProtocol {}
extension Dummy : Differentiable where Scalar : Differentiable {
  typealias TangentVector = Dummy
}

let fn = { (x: Dummy<Float>) -> Dummy<Float> in
  // 2. Here, I need to check that the requirements declared in the
  //    `@differentiable` attribute above are met.
  //
  //   I have access to the substitution map of the `apply` instruction
  //   corresponding to the `+` application:
  //
  // (substitution_map generic_signature=<τ_0_0 where τ_0_0 : MyProtocol, τ_0_0.Scalar : FloatingPoint>
  //   (substitution τ_0_0 -> Dummy<Float>)
  //     (conformance type=τ_0_0
  //       (specialized_conformance type=Dummy<Float> protocol=MyProtocol
  //         (substitution_map generic_signature=<τ_0_0>
  //           (substitution τ_0_0 -> Float))
  //         (conditional requirements unable to be computed)
  //         (normal_conformance type=Dummy<Scalar> protocol=MyProtocol
  //           (assoc_type req=Scalar type=Scalar))))
  //     (conformance type=τ_0_0.Scalar
  //       (normal_conformance type=Float protocol=FloatingPoint lazy)))
  return x + x
}

Reposting the key information: how can I check whether the Self.TangentVector : MyProtocol conformance requirement, whose LHS is a DependentMemberType:

(dependent_member_type assoc_type=Swift.(file).Differentiable.TangentVector
  (base=generic_type_param_type depth=0 index=0 decl=main.(file).MyProtocol extension.Self))

Is satisfied given the current module and the following substitution map?

(substitution_map generic_signature=<τ_0_0 where τ_0_0 : MyProtocol, τ_0_0.Scalar : FloatingPoint>
  (substitution τ_0_0 -> Dummy<Float>)
  (conformance type=τ_0_0
    (specialized_conformance type=Dummy<Float> protocol=MyProtocol
      (substitution_map generic_signature=<τ_0_0>
        (substitution τ_0_0 -> Float))
      (conditional requirements unable to be computed)
      (normal_conformance type=Dummy<Scalar> protocol=MyProtocol
        (assoc_type req=Scalar type=Scalar))))
  (conformance type=τ_0_0.Scalar
    (normal_conformance type=Float protocol=FloatingPoint lazy)))

Intuitively, the requirement is satisfied: Dummy<Float> conforms to Differentiable and Dummy<Float>.TangentVector is equal to Dummy<Float> and also conforms to Differentiable.

However, the conformance of Dummy<Float> to Differentiable is missing from the substitution map, and it's not clear how to remap τ_0_0 from the substitution map to Self in the conformance requirement in a robust way.

Here's the current hacky logic for checking this requirement: it calls DependentMemberType:: substBaseType on the first replacement type in the substitution map, if the substitution map has only one replacement type (acting as Self). It's not robust, and the entire checkRequirementsSatisfied function can likely be improved.

Any advice would be greatly appreciated!

2

cc team: @rxwei @bartchr808
cc @Slava_Pestov

3

Why can't you just call SubstitutionMap::lookupConformance()?

4

Actually, I think what you want here is to do module->lookupConformance(subMap.subst(myType), myProto). This should work with any Type, not just DependentMemberType.

5

I don't believe the conformance of τ_0_0 to Differentiable actually exists in the substitution map.

Thanks! Let me give this a try.

Edit: actually, I believe module->lookupConformance(subMap.subst(myType), myProto) is already attempted, but it doesn't work for some reason:

      if (auto origFirstType = firstType.subst(substMap)) {
        if (!origFirstType->hasError() &&
            swiftModule->lookupConformance(origFirstType, protocol)) {
          continue; // continue loop before diagnosing unmet requirement
        }
      }

Let me see why it doesn't work.

6

Oh I see. That's weird and it suggests that the substitution map was built from the wrong generic signature. If the original generic signature had a requirement τ_0_0 : Differentiable, it would work.

However, if that is not an option I think then you need something like:

auto substType = type.subst(QuerySubstitutionMap(subMap), LookUpConformanceInModule(swiftModule))

Then we will find the conformance in the module in order to resolve the correct type witness for τ_0_0.TangentVector (since it can't be found in the substitution map).

1 Like
7

FWIW, subst() will return the null type Type() on failure, not a type containing error types, so your code above will segfault in this case. If you want to return the original type with failed substitutions replaced by ErrorTypes, call subst() with SubstitutionFlags::UseErrorTypes.

1 Like
8

This seems promising, thanks! Let me try it and report back.

9

Thanks, your suggestion worked!

Reference PR: [AutoDiff] Fix logic for checking differentiation generic requirements. by dan-zheng · Pull Request #25176 · apple/swift · GitHub

1 Like