@@ -35,6 +35,12 @@ private predicate implSiblingCandidate(
3535 rootType = selfTy .resolveType ( )
3636}
3737
38+ pragma [ nomagic]
39+ private predicate blanketImplSiblingCandidate ( ImplItemNode impl , Trait trait ) {
40+ impl .isBlanketImplementation ( ) and
41+ trait = impl .resolveTraitTy ( )
42+ }
43+
3844/**
3945 * Holds if `impl1` and `impl2` are a sibling implementations of `trait`. We
4046 * consider implementations to be siblings if they implement the same trait for
@@ -44,40 +50,31 @@ private predicate implSiblingCandidate(
4450 */
4551pragma [ inline]
4652private predicate implSiblings ( TraitItemNode trait , Impl impl1 , Impl impl2 ) {
47- exists ( Type rootType , TypeMention selfTy1 , TypeMention selfTy2 |
48- impl1 != impl2 and
49- implSiblingCandidate ( impl1 , trait , rootType , selfTy1 ) and
50- implSiblingCandidate ( impl2 , trait , rootType , selfTy2 ) and
51- // In principle the second conjunct below should be superflous, but we still
52- // have ill-formed type mentions for types that we don't understand. For
53- // those checking both directions restricts further. Note also that we check
54- // syntactic equality, whereas equality up to renaming would be more
55- // correct.
56- typeMentionEqual ( selfTy1 , selfTy2 ) and
57- typeMentionEqual ( selfTy2 , selfTy1 )
53+ impl1 != impl2 and
54+ (
55+ exists ( Type rootType , TypeMention selfTy1 , TypeMention selfTy2 |
56+ implSiblingCandidate ( impl1 , trait , rootType , selfTy1 ) and
57+ implSiblingCandidate ( impl2 , trait , rootType , selfTy2 ) and
58+ // In principle the second conjunct below should be superflous, but we still
59+ // have ill-formed type mentions for types that we don't understand. For
60+ // those checking both directions restricts further. Note also that we check
61+ // syntactic equality, whereas equality up to renaming would be more
62+ // correct.
63+ typeMentionEqual ( selfTy1 , selfTy2 ) and
64+ typeMentionEqual ( selfTy2 , selfTy1 )
65+ )
66+ or
67+ blanketImplSiblingCandidate ( impl1 , trait ) and
68+ blanketImplSiblingCandidate ( impl2 , trait )
5869 )
5970}
6071
61- pragma [ nomagic]
62- private predicate isBlanketImpl ( ImplItemNode impl , Trait trait ) {
63- impl .isBlanketImplementation ( ) and
64- trait = impl .resolveTraitTy ( )
65- }
66-
6772/**
6873 * Holds if `impl` is an implementation of `trait` and if another implementation
6974 * exists for the same type.
7075 */
7176pragma [ nomagic]
72- private predicate implHasSibling ( ImplItemNode impl , Trait trait ) {
73- implSiblings ( trait , impl , _)
74- or
75- exists ( ImplItemNode other |
76- isBlanketImpl ( impl , trait ) and
77- isBlanketImpl ( other , trait ) and
78- impl != other
79- )
80- }
77+ private predicate implHasSibling ( ImplItemNode impl , Trait trait ) { implSiblings ( trait , impl , _) }
8178
8279/**
8380 * Holds if type parameter `tp` of `trait` occurs in the function `f` with the name
0 commit comments