@@ -368,7 +368,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
368368 predicate potentialInstantiationOf ( TypeAbstraction abs , App app , TypeMention term ) ;
369369 }
370370
371- module GenIsInstantiationOf < TypeTreeSig App, IsInstantiationOfSig< App > Input> {
371+ module IsInstantiationOf < TypeTreeSig App, IsInstantiationOfSig< App > Input> {
372372 private import Input
373373
374374 /** Gets the `i`th path in `term` per some arbitrary order. */
@@ -520,6 +520,28 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
520520 )
521521 }
522522
523+ /**
524+ * Holds if the type `type` can satisfy the constraint `constraint`
525+ * through `abs`, `sub`, and `constraintMention`.
526+ */
527+ predicate typeToTypeMention (
528+ Type type , Type constraint , TypeAbstraction abs , TypeMention sub ,
529+ TypeMention constraintMention
530+ ) {
531+ typeSatisfiesConstraintTrans ( abs , sub , constraintMention , _, _) and
532+ type = resolveTypeMentionRoot ( sub ) and
533+ constraint = resolveTypeMentionRoot ( constraintMention )
534+ }
535+
536+ int countConstraintImplementations ( Type type , Type constraint ) {
537+ result =
538+ strictcount ( TypeAbstraction abs , TypeMention tm , TypeMention constraintMention |
539+ typeToTypeMention ( type , constraint , abs , tm , constraintMention )
540+ |
541+ constraintMention
542+ )
543+ }
544+
523545 /**
524546 * Holds if `baseMention` is a (transitive) base type mention of `sub`,
525547 * and `t` is mentioned (implicitly) at `path` inside `baseMention`. For
@@ -847,23 +869,23 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
847869
848870 private module AccessConstraint {
849871 /**
850- * Holds if inferring types at `a` might depend on the type at `path` of
851- * `apos` having `base` as a transitive base type .
872+ * If the access `a` for `apos` and `path` has the root type `type` and
873+ * type inference requires it to satisfy the constraint `constraint` .
852874 */
853- private predicate relevantAccess ( Access a , AccessPosition apos , TypePath path , Type base ) {
875+ private predicate relevantAccess (
876+ Access a , AccessPosition apos , TypePath path , Type type , Type constraint
877+ ) {
854878 exists ( Declaration target , DeclarationPosition dpos |
855- adjustedAccessType ( a , apos , target , _, _) and
856- accessDeclarationPositionMatch ( apos , dpos )
857- |
858- path .isEmpty ( ) and declarationBaseType ( target , dpos , base , _, _)
859- or
860- typeParameterConstraintHasTypeParameter ( target , dpos , path , _, base , _, _)
879+ target = a .getTarget ( ) and
880+ type = a .getInferredType ( apos , path ) and
881+ accessDeclarationPositionMatch ( apos , dpos ) and
882+ typeParameterConstraintHasTypeParameter ( target , dpos , path , _, constraint , _, _)
861883 )
862884 }
863885
864886 newtype TTRelevantAccess =
865887 TRelevantAccess ( Access a , AccessPosition apos , TypePath path ) {
866- relevantAccess ( a , apos , path , _)
888+ relevantAccess ( a , apos , path , _, _ )
867889 }
868890
869891 class RelevantAccess extends TTRelevantAccess {
@@ -878,37 +900,69 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
878900 }
879901
880902 string toString ( ) {
881- result = a .toString ( ) + "," + apos .toString ( ) + "," + pathToSub .toString ( )
903+ result = a .toString ( ) + ", " + apos .toString ( ) + ", " + pathToSub .toString ( )
882904 }
883905
884906 Location getLocation ( ) { result = a .getLocation ( ) }
885907 }
886908
887909 module IsInstantiationOfInput implements IsInstantiationOfSig< RelevantAccess > {
888910 predicate potentialInstantiationOf ( TypeAbstraction abs , RelevantAccess at , TypeMention sub ) {
889- exists ( TypeMention sup , Access a , AccessPosition apos , TypePath pathToSub |
911+ // We only need to check instantiations where there are multiple candidates.
912+ exists (
913+ TypeMention constraintMention , Access a , AccessPosition apos , TypePath pathToSub ,
914+ Type type
915+ |
916+ type = resolveTypeMentionRoot ( sub ) and
890917 at = TRelevantAccess ( a , apos , pathToSub ) and
891- relevantAccess ( a , apos , pathToSub , resolveTypeMentionRoot ( sup ) ) and
892- typeSatisfiesConstraintTrans ( abs , sub , sup , _, _)
918+ relevantAccess ( a , apos , pathToSub , type , resolveTypeMentionRoot ( constraintMention ) ) and
919+ typeSatisfiesConstraintTrans ( abs , sub , constraintMention , _, _) and
920+ countConstraintImplementations ( type , resolveTypeMentionRoot ( constraintMention ) ) > 1
893921 )
894922 }
895923 }
896924
897- module IsInstantiationOf = GenIsInstantiationOf< RelevantAccess , IsInstantiationOfInput > ;
925+ /**
926+ * The type at `a`, `apos`, `pathToSub` satisfies `constraint` through
927+ * `abs`, `sub`, and `constraintMention`.
928+ */
929+ predicate hasConstraintMention (
930+ Access a , AccessPosition apos , TypePath pathToSub , Type constraint , TypeAbstraction abs ,
931+ TypeMention sub , TypeMention constraintMention
932+ ) {
933+ exists ( Type type | relevantAccess ( a , apos , pathToSub , type , constraint ) |
934+ not exists ( countConstraintImplementations ( type , constraint ) ) and
935+ typeSatisfiesConstraintTrans ( abs , sub , constraintMention , _, _) and
936+ resolveTypeMentionRoot ( sub ) = abs .getATypeParameter ( ) and
937+ constraint = resolveTypeMentionRoot ( constraintMention )
938+ or
939+ countConstraintImplementations ( type , constraint ) > 0 and
940+ typeToTypeMention ( type , constraint , abs , sub , constraintMention ) and
941+ // When there are multiple ways the type could implement the
942+ // constraint we need to find the right implementation, which is the
943+ // one where the type instantiates the precondition.
944+ if countConstraintImplementations ( type , constraint ) > 1
945+ then
946+ IsInstantiationOf< RelevantAccess , IsInstantiationOfInput > :: isInstantiationOf ( TRelevantAccess ( a ,
947+ apos , pathToSub ) , abs , sub )
948+ else any ( )
949+ )
950+ }
898951
899952 /**
900953 * Holds if the constraint is satisfied.
901954 */
902955 pragma [ nomagic]
903956 predicate satisfiesConstraintTypeMention (
904- Access a , AccessPosition apos , TypePath pathToSub , TypeMention sup , TypePath path , Type t
957+ Access a , AccessPosition apos , TypePath pathToSub , Type constraint , TypePath path , Type t
905958 ) {
906- relevantAccess ( a , apos , pathToSub , resolveTypeMentionRoot ( sup ) ) and
907- exists ( TypeAbstraction abs , TypeMention sub , TypePath prefix , Type t0 , RelevantAccess at |
959+ exists (
960+ RelevantAccess at , TypeAbstraction abs , TypeMention sub , Type t0 , TypePath prefix ,
961+ TypeMention constraintMention
962+ |
908963 at = TRelevantAccess ( a , apos , pathToSub ) and
909- // The found sub type is more general than the inferred access type
910- typeSatisfiesConstraintTrans ( abs , sub , sup , prefix , t0 ) and
911- IsInstantiationOf:: isInstantiationOf ( at , abs , sub ) and
964+ hasConstraintMention ( a , apos , pathToSub , constraint , abs , sub , constraintMention ) and
965+ typeSatisfiesConstraintTrans ( abs , sub , constraintMention , prefix , t0 ) and
912966 (
913967 not t0 = abs .getATypeParameter ( ) and t = t0 and path = prefix
914968 or
@@ -1049,13 +1103,13 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
10491103 not exists ( getTypeArgument ( a , target , tp , _) ) and
10501104 target = a .getTarget ( ) and
10511105 exists (
1052- TypeMention base , AccessPosition apos , DeclarationPosition dpos , TypePath pathToTp ,
1106+ Type constraint , AccessPosition apos , DeclarationPosition dpos , TypePath pathToTp ,
10531107 TypePath pathToTp2
10541108 |
10551109 accessDeclarationPositionMatch ( apos , dpos ) and
1056- typeParameterConstraintHasTypeParameter ( target , dpos , pathToTp2 , _,
1057- resolveTypeMentionRoot ( base ) , pathToTp , tp ) and
1058- AccessConstraint:: satisfiesConstraintTypeMention ( a , apos , pathToTp2 , base ,
1110+ typeParameterConstraintHasTypeParameter ( target , dpos , pathToTp2 , _, constraint , pathToTp ,
1111+ tp ) and
1112+ AccessConstraint:: satisfiesConstraintTypeMention ( a , apos , pathToTp2 , constraint ,
10591113 pathToTp .append ( path ) , t )
10601114 )
10611115 }
0 commit comments