@@ -1392,7 +1392,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
13921392 }
13931393
13941394 /** A position whose inferred type should satisfy a declared type or type constraint. */
1395- abstract private class MatchingPosition extends TMatchingPosition {
1395+ abstract class MatchingPosition extends TMatchingPosition {
13961396 abstract Declaration getTarget ( ) ;
13971397
13981398 abstract Type getTypeAt ( TypePath path ) ;
@@ -1406,6 +1406,18 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
14061406
14071407 abstract predicate typeParameterAt ( TypePath path , TypeParameter tp ) ;
14081408
1409+ /** Holds if `prefix` leads from `apos` to the inferred type being constrained. */
1410+ abstract predicate accessPath ( AccessPosition apos , TypePath prefix ) ;
1411+
1412+ /** Gets a concrete type that can be propagated from this constraint to the access. */
1413+ Type getConcreteTypeAt ( TypePath path ) { none ( ) }
1414+
1415+ /** Holds if the type parameter at `path` can supply contextual types for `a`. */
1416+ predicate contextualTypeParameterAt ( Access a , TypePath path , TypeParameter tp ) {
1417+ this .getTarget ( ) = a .getTarget ( _) and
1418+ this .typeParameterAt ( path , tp )
1419+ }
1420+
14091421 abstract string toString ( ) ;
14101422
14111423 Location getLocation ( ) { result = this .getTarget ( ) .getLocation ( ) }
@@ -1442,6 +1454,16 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
14421454 argRootTypeSatisfiesTargetTypeCand ( _, target , apos , tp , path )
14431455 }
14441456
1457+ override predicate accessPath ( AccessPosition accessPos , TypePath prefix ) {
1458+ accessPos = apos and
1459+ prefix = TypePath:: nil ( )
1460+ }
1461+
1462+ override predicate contextualTypeParameterAt ( Access a , TypePath path , TypeParameter tp ) {
1463+ super .contextualTypeParameterAt ( a , path , tp ) and
1464+ hasNotTypeArgument ( a , target , tp )
1465+ }
1466+
14451467 override string toString ( ) { result = target .toString ( ) + ", " + apos .toString ( ) }
14461468 }
14471469
@@ -1467,6 +1489,18 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
14671489 typeParameterConstraintHasTypeParameter ( target , constrainedTp , constraint , path , tp )
14681490 }
14691491
1492+ override predicate accessPath ( AccessPosition apos , TypePath prefix ) {
1493+ exists ( DeclarationPosition dpos |
1494+ accessDeclarationPositionMatch ( apos , dpos ) and
1495+ constrainedTp = target .getDeclaredType ( dpos , prefix )
1496+ )
1497+ }
1498+
1499+ override Type getConcreteTypeAt ( TypePath path ) {
1500+ result = this .getTypeAt ( path ) and
1501+ not result instanceof TypeParameter
1502+ }
1503+
14701504 override string toString ( ) {
14711505 result = constrainedTp .toString ( ) + ": " + constraint .toString ( )
14721506 }
@@ -1571,95 +1605,20 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
15711605 )
15721606 }
15731607
1574- predicate baseTypeMatchAtTypeParameter (
1575- Access a , AccessEnvironment e , AccessPosition apos , Declaration target , TypeParameter tp ,
1576- TypePath prefix , TypePath requiredPrefix
1577- ) {
1578- exists (
1579- TypePath pathToTypeParamInConstraint , TypePath pathToTp , TypePath pathToTypeParamInSub
1580- |
1581- argRootTypeSatisfiesTargetTypeCand ( _, target , pragma [ only_bind_into ] ( apos ) , tp , pathToTp ) and
1582- SatisfiesParameterConstraint:: satisfiesConstraintAtTypeParameter ( MkRelevantAccess ( a ,
1583- MkArgumentPosition ( target , pragma [ only_bind_into ] ( apos ) ) , e ) ,
1584- MkArgumentPosition ( target , pragma [ only_bind_into ] ( apos ) ) , pathToTypeParamInConstraint ,
1585- pathToTypeParamInSub ) and
1586- hasNotTypeArgument ( a , target , tp )
1587- |
1588- /*
1589- * Example:
1590- *
1591- * ```swift
1592- * class Base<B> {
1593- * init(_ value: B) {}
1594- * }
1595- *
1596- * class Derived<D>: Base<[D]> {
1597- * init(_ value: D) { super.init([value]) }
1598- * }
1599- *
1600- * func foo<T>(_ value: T, _ base: Base<T>) { }
1601- *
1602- * foo([2], Derived(<unknown>))
1603- * ```
1604- *
1605- * - tp = T (bound by `foo`)
1606- * - prefix = pathToTypeParamInSub = "D"
1607- * - requiredPrefix = "Element"
1608- * - pathToTypeParamInConstraint = "B.Element"
1609- * - pathToTp = "B"
1610- */
1611-
1612- pathToTypeParamInConstraint = pathToTp .appendInverse ( requiredPrefix ) and
1613- prefix = pathToTypeParamInSub
1614- or
1615- /*
1616- * Example:
1617- *
1618- * ```swift
1619- * class Base<B> {
1620- * init(_ value: B) {}
1621- * }
1622- *
1623- * class Derived<D>: Base<D> {
1624- * override init(_ value: D) { super.init(value) }
1625- * }
1626- *
1627- * func foo<T>(_ value: T, _ base: Base<T?>) {}
1628- *
1629- * foo(2, Derived(Optional.none))
1630- * ```
1631- *
1632- * - tp = T (bound by `foo`)
1633- * - prefix = "D.Wrapped"
1634- * - pathToTypeParamInSub = "D"
1635- * - requiredPrefix = ""
1636- * - pathToTypeParamInConstraint = "B"
1637- * - pathToTp = "B.Wrapped"
1638- */
1639-
1640- exists ( TypePath path0 |
1641- pathToTp = pathToTypeParamInConstraint .appendInverse ( path0 ) and
1642- prefix = pathToTypeParamInSub .append ( path0 ) and
1643- requiredPrefix = TypePath:: nil ( )
1644- )
1645- )
1646- }
1647-
1608+ /**
1609+ * Holds if a constraint on an argument or type argument reaches a type
1610+ * parameter in the inferred type at `pathToTypeParamInSub`. `prefix` is
1611+ * the path from `apos` to the inferred type being constrained.
1612+ */
16481613 pragma [ nomagic]
16491614 predicate argSatisfiesConstraintAtTypeParameter (
1650- Access a , AccessEnvironment e , Declaration target , AccessPosition apos , TypePath prefix ,
1651- TypeMention constraint , TypePath pathToTypeParamInConstraint ,
1615+ Access a , AccessEnvironment e , AccessPosition apos , TypePath prefix ,
1616+ MatchingPosition constraint , TypePath pathToTypeParamInConstraint ,
16521617 TypePath pathToTypeParamInSub
16531618 ) {
1654- exists ( TypeParameter constrainedTp , MatchingPosition pos |
1655- pos = MkTypeArgumentPosition ( target , constrainedTp , constraint ) and
1656- SatisfiesParameterConstraint:: satisfiesConstraintAtTypeParameter ( MkRelevantAccess ( a ,
1657- pos , e ) , pos , pathToTypeParamInConstraint , pathToTypeParamInSub ) and
1658- exists ( DeclarationPosition dpos |
1659- accessDeclarationPositionMatch ( apos , dpos ) and
1660- constrainedTp = target .getDeclaredType ( dpos , prefix )
1661- )
1662- )
1619+ constraint .accessPath ( apos , prefix ) and
1620+ SatisfiesParameterConstraint:: satisfiesConstraintAtTypeParameter ( MkRelevantAccess ( a ,
1621+ constraint , e ) , constraint , pathToTypeParamInConstraint , pathToTypeParamInSub )
16631622 }
16641623 }
16651624
@@ -1798,21 +1757,11 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
17981757 )
17991758 or
18001759 exists (
1801- Declaration target , TypePath prefix , TypePath requiredPrefix , TypePath suffix ,
1802- TypeParameter tp
1803- |
1804- ConstraintMatching:: baseTypeMatchAtTypeParameter ( a , e , apos , target , tp , prefix ,
1805- requiredPrefix ) and
1806- typeMatch ( a , e , target , requiredPrefix .appendInverse ( suffix ) , result , tp ) and
1807- path = prefix .append ( suffix )
1808- )
1809- or
1810- exists (
1811- Declaration target , TypePath prefix , TypeMention constraint ,
1760+ TypePath prefix , ConstraintMatching:: MatchingPosition constraint ,
18121761 TypePath pathToTypeParamInConstraint , TypePath pathToTypeParamInSub
18131762 |
1814- ConstraintMatching:: argSatisfiesConstraintAtTypeParameter ( a , e , target , apos , prefix ,
1815- constraint , pathToTypeParamInConstraint , pathToTypeParamInSub )
1763+ ConstraintMatching:: argSatisfiesConstraintAtTypeParameter ( a , e , apos , prefix , constraint ,
1764+ pathToTypeParamInConstraint , pathToTypeParamInSub )
18161765 |
18171766 exists ( TypePath suffix |
18181767 /*
@@ -1841,18 +1790,12 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
18411790 * That is, it allows us to infer that the type of `x` is `MyThing<i32>`.
18421791 */
18431792
1844- result = constraint .getTypeAt ( pathToTypeParamInConstraint .appendInverse ( suffix ) ) and
1845- not result instanceof TypeParameter and
1793+ result = constraint .getConcreteTypeAt ( pathToTypeParamInConstraint .appendInverse ( suffix ) ) and
18461794 path = prefix .append ( pathToTypeParamInSub .append ( suffix ) )
18471795 )
18481796 or
18491797 exists ( TypeParameter tp , TypePath suffix , TypePath mid , TypePath pathToTp |
1850- exists ( TypeParameter constrainedTp , DeclarationPosition dpos |
1851- typeParameterConstraintHasTypeParameter ( target , constrainedTp , constraint , pathToTp ,
1852- tp ) and
1853- accessDeclarationPositionMatch ( apos , dpos ) and
1854- constrainedTp = target .getDeclaredType ( dpos , _)
1855- )
1798+ constraint .contextualTypeParameterAt ( a , pathToTp , tp )
18561799 |
18571800 /*
18581801 * Example:
@@ -1887,7 +1830,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
18871830 * That is, it allows us to infer that the type of `y` is `MyThing<S<i32>>`.
18881831 */
18891832
1890- typeMatch ( a , e , target , suffix , result , tp ) and
1833+ typeMatch ( a , e , constraint . getTarget ( ) , suffix , result , tp ) and
18911834 pathToTp = pathToTypeParamInConstraint .appendInverse ( mid ) and
18921835 path = prefix .append ( pathToTypeParamInSub .append ( mid ) .append ( suffix ) )
18931836 or
@@ -1925,7 +1868,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
19251868 */
19261869
19271870 pathToTypeParamInConstraint = pathToTp .appendInverse ( mid ) and
1928- typeMatch ( a , e , target , mid .appendInverse ( suffix ) , result , tp ) and
1871+ typeMatch ( a , e , constraint . getTarget ( ) , mid .appendInverse ( suffix ) , result , tp ) and
19291872 path = prefix .append ( pathToTypeParamInSub .append ( suffix ) )
19301873 )
19311874 )
0 commit comments