@@ -287,11 +287,11 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
287
287
* - `T3` is mentioned at `T2.T1` for immediate base type mention `Base<C<T3>>`
288
288
* of `Mid`,
289
289
* - ``C`1`` is mentioned at `T3` for immediate base type mention `Mid<C<T4>>`
290
- * of `Sub`, and
290
+ * of `Sub`,
291
291
* - `T4` is mentioned at `T3.T1` for immediate base type mention `Mid<C<T4>>`
292
- * of `Sub`, and
292
+ * of `Sub`,
293
293
* - ``C`1`` is mentioned at `T2` and implicitly at `T2.T1` for transitive base type
294
- * mention `Base<C<T3>>` of `Sub`.
294
+ * mention `Base<C<T3>>` of `Sub`, and
295
295
* - `T4` is mentioned implicitly at `T2.T1.T1` for transitive base type mention
296
296
* `Base<C<T3>>` of `Sub`.
297
297
*/
@@ -307,8 +307,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
307
307
or
308
308
// transitive base class
309
309
exists ( Type immediateBase | immediateBase = resolveTypeMentionRoot ( immediateBaseMention ) |
310
- not t = immediateBase .getATypeParameter ( ) and
311
- baseTypeMentionHasTypeAt ( immediateBase , baseMention , path , t )
310
+ baseTypeMentionHasNonTypeParameterAt ( immediateBase , baseMention , path , t )
312
311
or
313
312
exists ( TypePath path0 , TypePath prefix , TypePath suffix , TypeParameter tp |
314
313
/*
@@ -336,15 +335,29 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
336
335
* ```
337
336
*/
338
337
339
- baseTypeMentionHasTypeAt ( immediateBase , baseMention , prefix , tp ) and
340
- tp = immediateBase .getATypeParameter ( ) and
338
+ baseTypeMentionHasTypeParameterAt ( immediateBase , baseMention , prefix , tp ) and
341
339
t = immediateBaseMention .resolveTypeAt ( path0 ) and
342
340
path0 .isCons ( tp , suffix ) and
343
341
path = prefix .append ( suffix )
344
342
)
345
343
)
346
344
)
347
345
}
346
+
347
+ /** Similar to `baseTypeMentionHasTypeAt` but FIXME: */
348
+ pragma [ inline]
349
+ predicate baseTypeMentionHasNonTypeParameterAt (
350
+ Type sub , TypeMention baseMention , TypePath path , Type t
351
+ ) {
352
+ not t = sub .getATypeParameter ( ) and baseTypeMentionHasTypeAt ( sub , baseMention , path , t )
353
+ }
354
+
355
+ pragma [ inline]
356
+ predicate baseTypeMentionHasTypeParameterAt (
357
+ Type sub , TypeMention baseMention , TypePath path , TypeParameter tp
358
+ ) {
359
+ tp = sub .getATypeParameter ( ) and baseTypeMentionHasTypeAt ( sub , baseMention , path , tp )
360
+ }
348
361
}
349
362
350
363
private import BaseTypes
@@ -514,7 +527,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
514
527
private module AccessBaseType {
515
528
/**
516
529
* Holds if inferring types at `a` might depend on the type at `path` of
517
- * `apos` having `baseMention ` as a transitive base type mention.
530
+ * `apos` having `base ` as a transitive base type mention.
518
531
*/
519
532
private predicate relevantAccess ( Access a , AccessPosition apos , TypePath path , Type base ) {
520
533
exists ( Declaration target , DeclarationPosition dpos |
@@ -557,8 +570,9 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
557
570
* // ^^^^^^^^^^^^^^^^^^^^^^^^^ `a`
558
571
* ```
559
572
*
560
- * where the method call is an access and `new Sub<int>()` is at an
561
- * access position, which is the receiver of a method call, we have:
573
+ * where the method call is an access, `new Sub<int>()` is at the access
574
+ * position which is the receiver of a method call, and `pathToSub` is
575
+ * `""` we have:
562
576
*
563
577
* `baseMention` | `path` | `t`
564
578
* ------------- | ------------ | ---
@@ -575,12 +589,10 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
575
589
) {
576
590
relevantAccess ( a , apos , pathToSub , resolveTypeMentionRoot ( baseMention ) ) and
577
591
exists ( Type sub | sub = a .getInferredType ( apos , pathToSub ) |
578
- not t = sub .getATypeParameter ( ) and
579
- baseTypeMentionHasTypeAt ( sub , baseMention , path , t )
592
+ baseTypeMentionHasNonTypeParameterAt ( sub , baseMention , path , t )
580
593
or
581
594
exists ( TypePath prefix , TypePath suffix , TypeParameter tp |
582
- tp = sub .getATypeParameter ( ) and
583
- baseTypeMentionHasTypeAt ( sub , baseMention , prefix , tp ) and
595
+ baseTypeMentionHasTypeParameterAt ( sub , baseMention , prefix , tp ) and
584
596
t = inferTypeAt ( a , apos , pathToSub , tp , suffix ) and
585
597
path = prefix .append ( suffix )
586
598
)
@@ -681,15 +693,15 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
681
693
* For this example
682
694
* ```csharp
683
695
* interface IFoo<A> { }
684
- * void M<T1, T2>(T2 item) where T2 : IFoo<T1> { }
696
+ * T1 M<T1, T2>(T2 item) where T2 : IFoo<T1> { }
685
697
* ```
686
698
* with the method declaration being the target and the for the first
687
699
* parameter position, we have the following
688
700
* - `path1 = ""`,
689
701
* - `tp1 = T2`,
690
702
* - `constraint = IFoo`,
691
- * - `path2 = "A"`,
692
- * - `tp2 = T1`
703
+ * - `path2 = "A"`, and
704
+ * - `tp2 = T1`.
693
705
*/
694
706
pragma [ nomagic]
695
707
private predicate typeParameterConstraintHasTypeParameter (
0 commit comments