@@ -22,17 +22,8 @@ private signature Type resolveTypeMentionAtSig(AstNode tm, TypePath path);
2222 * how to resolve type mentions (`PreTypeMention` vs. `TypeMention`).
2323 */
2424private module MkSiblingImpls< resolveTypeMentionAtSig / 2 resolveTypeMentionAt> {
25- pragma [ nomagic]
26- private Type resolveNonTypeParameterTypeAt ( AstNode tm , TypePath path ) {
27- result = resolveTypeMentionAt ( tm , path ) and
28- not result instanceof TypeParameter
29- }
30-
31- bindingset [ t1, t2]
32- private predicate typeMentionEqual ( AstNode t1 , AstNode t2 ) {
33- forex ( TypePath path , Type type | resolveNonTypeParameterTypeAt ( t1 , path ) = type |
34- resolveNonTypeParameterTypeAt ( t2 , path ) = type
35- )
25+ private class Tm extends AstNode {
26+ Type getTypeAt ( TypePath path ) { result = resolveTypeMentionAt ( this , path ) }
3627 }
3728
3829 pragma [ nomagic]
@@ -50,54 +41,91 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
5041 trait = impl .resolveTraitTy ( )
5142 }
5243
44+ private module ImplIsInstantiationOfSiblingInput implements IsInstantiationOfInputSig< Tm , Tm > {
45+ predicate potentialInstantiationOf ( Tm cond , TypeAbstraction abs , Tm constraint ) {
46+ exists ( TraitItemNode trait , Type rootType |
47+ implSiblingCandidate ( _, trait , rootType , cond ) and
48+ implSiblingCandidate ( abs , trait , rootType , constraint ) and
49+ cond != constraint
50+ )
51+ }
52+ }
53+
54+ private module ImplIsInstantiationOfSibling =
55+ IsInstantiationOf< Tm , Tm , ImplIsInstantiationOfSiblingInput > ;
56+
5357 /**
5458 * Holds if `impl1` and `impl2` are sibling implementations of `trait`. We
55- * consider implementations to be siblings if they implement the same trait for
56- * the same type. In that case `Self` is the same type in both implementations,
57- * and method calls to the implementations cannot be resolved unambiguously
58- * based only on the receiver type.
59+ * consider implementations to be siblings if they implement the same trait and
60+ * the type being implemented by one of the implementations is an instantiation
61+ * of the type being implemented by the other.
62+ *
63+ * For example, in
64+ *
65+ * ```rust
66+ * trait MyTrait<T> { ... }
67+ * impl MyTrait<i64> for i64 { ... } // I1
68+ * impl MyTrait<u64> for i64 { ... } // I2
69+ *
70+ * impl MyTrait<i64> for S<i64> { ... } // I3
71+ * impl MyTrait<u64> for S<u64> { ... } // I4
72+ * impl MyTrait<bool> for S<T> { ... } // I5
73+ * ```
74+ *
75+ * the pairs `(I1, I2)`, `(I3, I5)`, and `(I4, I5)` are siblings, but not `(I3, I4)`.
76+ *
77+ * Whenever an implementation has a sibling, calls to the implementations cannot be
78+ * resolved unambiguously based only on the `Self` type alone.
5979 */
60- pragma [ inline]
61- predicate implSiblings ( TraitItemNode trait , Impl impl1 , Impl impl2 ) {
62- impl1 != impl2 and
63- (
64- exists ( Type rootType , AstNode selfTy1 , AstNode selfTy2 |
65- implSiblingCandidate ( impl1 , trait , rootType , selfTy1 ) and
66- implSiblingCandidate ( impl2 , trait , rootType , selfTy2 ) and
67- // In principle the second conjunct below should be superfluous, but we still
68- // have ill-formed type mentions for types that we don't understand. For
69- // those checking both directions restricts further. Note also that we check
70- // syntactic equality, whereas equality up to renaming would be more
71- // correct.
72- typeMentionEqual ( selfTy1 , selfTy2 ) and
73- typeMentionEqual ( selfTy2 , selfTy1 )
74- )
75- or
76- blanketImplSiblingCandidate ( impl1 , trait ) and
77- blanketImplSiblingCandidate ( impl2 , trait )
80+ pragma [ nomagic]
81+ predicate implSiblings ( TraitItemNode trait , ImplItemNode impl1 , ImplItemNode impl2 ) {
82+ exists ( Type rootType , AstNode selfTy1 , AstNode selfTy2 |
83+ implSiblingCandidate ( impl1 , trait , rootType , selfTy1 ) and
84+ implSiblingCandidate ( impl2 , trait , rootType , selfTy2 )
85+ |
86+ ImplIsInstantiationOfSibling:: isInstantiationOf ( selfTy1 , impl2 , selfTy2 ) or
87+ ImplIsInstantiationOfSibling:: isInstantiationOf ( selfTy2 , impl1 , selfTy1 )
7888 )
89+ or
90+ blanketImplSiblingCandidate ( impl1 , trait ) and
91+ blanketImplSiblingCandidate ( impl2 , trait ) and
92+ impl1 != impl2
7993 }
8094
8195 /**
8296 * Holds if `impl` is an implementation of `trait` and if another implementation
8397 * exists for the same type.
8498 */
85- pragma [ nomagic]
8699 predicate implHasSibling ( ImplItemNode impl , Trait trait ) { implSiblings ( trait , impl , _) }
87100
101+ pragma [ nomagic]
102+ predicate implSiblings ( TraitItemNode trait , ImplItemNode impl1 , Tm traitMention1 , Tm traitMention2 ) {
103+ exists ( ImplItemNode impl2 |
104+ implSiblings ( trait , impl1 , impl2 ) and
105+ traitMention1 = impl1 .getTraitPath ( ) and
106+ traitMention2 = impl2 .getTraitPath ( )
107+ )
108+ }
109+
110+ bindingset [ t1, t2]
111+ pragma [ inline_late]
112+ private predicate differentTypes ( Type t1 , Type t2 ) {
113+ t1 != t2 and
114+ ( not t1 instanceof TypeParameter or not t2 instanceof TypeParameter )
115+ }
116+
88117 pragma [ nomagic]
89118 predicate implHasAmbiguousSiblingAt ( ImplItemNode impl , Trait trait , TypePath path ) {
90- exists ( ImplItemNode impl2 , Type t1 , Type t2 |
91- implSiblings ( trait , impl , impl2 ) and
92- t1 = resolveTypeMentionAt ( impl .getTraitPath ( ) , path ) and
93- t2 = resolveTypeMentionAt ( impl2 .getTraitPath ( ) , path ) and
94- t1 != t2
95- |
96- not t1 instanceof TypeParameter or
97- not t2 instanceof TypeParameter
119+ exists ( Tm traitMention , Tm traitMention2 , Type t1 , Type t2 |
120+ implSiblings ( trait , impl , traitMention , traitMention2 ) and
121+ t1 = traitMention .getTypeAt ( path ) and
122+ t2 = traitMention2 .getTypeAt ( path ) and
123+ differentTypes ( t1 , t2 )
98124 )
99125 or
100- // todo: handle blanket/non-blanket siblings in `implSiblings`
126+ // Since we cannot resolve the `Output` types of certain built-in `Index` trait
127+ // implementations, we need to ensure that the type-specialized versions that we
128+ // ship do not apply unless there is an exact type match
101129 trait =
102130 any ( IndexTrait it |
103131 implSiblingCandidate ( impl , it , _, _) and
@@ -152,19 +180,14 @@ private predicate functionResolutionDependsOnArgumentCand(
152180 * ```rust
153181 * trait MyTrait<T> {
154182 * fn method(&self, value: Foo<T>) -> Self;
155- * // ^^^^^^^^^^^^^ `pos` = 0
183+ * // ^^^^^^^^^^^^^ `pos` = 1
156184 * // ^ `path` = "T"
157185 * }
158186 * impl MyAdd<i64> for i64 {
159187 * fn method(&self, value: Foo<i64>) -> Self { ... }
160188 * // ^^^ `type` = i64
161189 * }
162190 * ```
163- *
164- * Note that we only check the root type symbol at the position. If the type
165- * at that position is a type constructor (for instance `Vec<..>`) then
166- * inspecting the entire type tree could be necessary to disambiguate the
167- * method. In that case we will still resolve several methods.
168191 */
169192
170193 exists ( TraitItemNode trait |
0 commit comments