@@ -149,6 +149,10 @@ signature module InputSig1<LocationSig Location> {
149149 Location getLocation ( ) ;
150150 }
151151
152+ /**
153+ * A psuedo type. Pseudo types are skipped when checking for non-instantiations
154+ * in `isNotInstantiationOf`.
155+ */
152156 class PseudoType extends Type ;
153157
154158 /**
@@ -2471,7 +2475,30 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
24712475 TypeMention getReturnType ( ) ;
24722476 }
24732477
2474- /** A special pseudo type representing a particular closure parameter. */
2478+ /**
2479+ * A special pseudo type representing a particular closure parameter.
2480+ *
2481+ * This is needed in cases where the type of a closure parameter must be
2482+ * inferred from the inferred _return type_ of the closure. For example,
2483+ * in
2484+ *
2485+ * ```rust
2486+ * let c = |x| x;
2487+ * let r: i32 = c(42);
2488+ * ```
2489+ *
2490+ * by assigning `x` the pseudo type `T_x`, we can
2491+ *
2492+ * 1. bottom-up infer that `c` has type `Fn(_) -> T_x`,
2493+ * 2. this enables us to detect that contextual inference is needed, so we also
2494+ * assign `c` the type `Fn(_) -> UnknownType`,
2495+ * 3. using bottom-up inference allows us to infer that `c(42)` must have
2496+ * `UnknownType`,
2497+ * 4. using contextual inference allows us to infer that `c` has type `Fn(_) -> i32`, and
2498+ * 5. finally since `c` also has type `Fn(_) -> T_x`, we conclude that `x` has type `i32`.
2499+ *
2500+ * . Then, when we propagate type information downwards from the
2501+ */
24752502 class ClosureParameterPseudoType extends PseudoType ;
24762503
24772504 /** Gets the pseudo type corresponding to closure parameter `p`. */
@@ -2554,6 +2581,15 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
25542581 )
25552582 }
25562583
2584+ private predicate closureStep ( AstNode n1 , TypePath path1 , Closure n2 , TypePath path2 ) {
2585+ exists ( int index , Parameter p |
2586+ n1 = p .getPattern ( ) and
2587+ p = n2 .getParameter ( index ) and
2588+ path1 .isEmpty ( ) and
2589+ path2 = getClosureParameterTypePath ( p )
2590+ )
2591+ }
2592+
25572593 /** Provides logic for inferring certain type information. */
25582594 private module Certain {
25592595 predicate stepCertain ( AstNode n1 , TypePath path1 , AstNode n2 , TypePath path2 ) {
@@ -2572,27 +2608,17 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
25722608 or
25732609 n1 = n2 .( ParenExpr ) .getExpr ( )
25742610 )
2575- or
2576- exists ( Closure c , int index , Parameter p |
2577- path1 .isEmpty ( ) and
2578- p = c .getParameter ( index )
2579- |
2580- n1 = p and
2581- n2 = c and
2582- path2 = getClosureParameterTypePath ( n1 )
2583- or
2584- n1 = p .getPattern ( ) and
2585- n2 = p and
2586- path2 .isEmpty ( )
2587- )
25882611 }
25892612
25902613 pragma [ nomagic]
25912614 private Type inferTypeFromStepCertain ( AstNode n , TypePath path ) {
25922615 exists ( TypePath path1 , AstNode n2 , TypePath path2 , TypePath suffix |
25932616 result = inferTypeCertain ( n2 , path2 .appendInverse ( suffix ) ) and
2594- path = path1 .append ( suffix ) and
2617+ path = path1 .append ( suffix )
2618+ |
25952619 stepCertain ( n2 , path2 , n , path1 )
2620+ or
2621+ closureStep ( n2 , path2 , n , path1 )
25962622 )
25972623 }
25982624
@@ -2716,8 +2742,12 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
27162742 private Type inferTypeFromStep ( AstNode n , TypePath path ) {
27172743 exists ( TypePath path1 , AstNode n2 , TypePath path2 , TypePath suffix |
27182744 result = inferType ( n2 , path2 .appendInverse ( suffix ) ) and
2719- path = path1 .append ( suffix ) and
2745+ path = path1 .append ( suffix )
2746+ |
27202747 step ( n2 , path2 , n , path1 )
2748+ or
2749+ closureStep ( n2 , path2 , n , path1 ) and
2750+ not result = getClosureParameterPseudoType ( n .( Closure ) .getParameter ( _) )
27212751 )
27222752 }
27232753
@@ -2752,8 +2782,11 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
27522782 or
27532783 exists ( TypePath path1 , AstNode n2 , TypePath path2 , TypePath suffix |
27542784 result = inferType ( n2 , path2 .appendInverse ( suffix ) ) and
2755- path = path1 .append ( suffix ) and
2785+ path = path1 .append ( suffix )
2786+ |
27562787 step ( n , path1 , n2 , path2 )
2788+ or
2789+ closureStep ( n , path1 , n2 , path2 )
27572790 )
27582791 }
27592792
@@ -2765,31 +2798,43 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
27652798 prefix = path .getAPrefix ( )
27662799 }
27672800
2768- private Type inferClosureType ( AstNode n , TypePath path ) {
2801+ pragma [ nomagic]
2802+ private predicate hasClosureParameterPseudoType ( AstNode n , Parameter p , TypePath path ) {
2803+ inferType0 ( n , path ) = getClosureParameterPseudoType ( p )
2804+ }
2805+
2806+ /**
2807+ * If the type of a parameter occurs in the inferred return type of the closure,
2808+ * allow for contextual inference based on the inferred return type to propagate
2809+ * type information into the parameter
2810+ */
2811+ private Type inferClosureParameterType ( AstNode n , TypePath path ) {
27692812 exists ( Closure c , Parameter p | p = c .getParameter ( _) |
2770- n = p .getPattern ( ) and
2771- path .isEmpty ( ) and
2772- result = getClosureParameterPseudoType ( p )
2773- or
2774- exists ( TypePath ret | inferType ( c , ret ) = getClosureParameterPseudoType ( p ) |
2813+ not exists ( p .getType ( ) ) and
2814+ (
2815+ n = p .getPattern ( ) and
2816+ path .isEmpty ( ) and
2817+ result = getClosureParameterPseudoType ( p )
2818+ or
27752819 n = c and
2776- path = ret and
2820+ path = getClosureParameterTypePath ( p ) and
27772821 result instanceof UnknownType
27782822 or
2779- inferType ( c , ret .appendInverse ( path ) ) = result and
27802823 n = p .getPattern ( ) and
2824+ result = inferType ( c , getClosureParameterTypePath ( p ) .appendInverse ( path ) ) and
27812825 not result instanceof UnknownType
27822826 )
27832827 or
2828+ hasClosureParameterPseudoType ( c , p , path ) and
2829+ n = c and
2830+ result instanceof UnknownType
2831+ or
27842832 exists ( AstNode n0 , TypePath prefix |
2785- inferType ( n0 , prefix ) = getClosureParameterPseudoType ( p ) and
2786- result = inferTypeCertain ( n0 , prefix .appendInverse ( path ) ) and
2787- n = p .getPattern ( )
2833+ hasClosureParameterPseudoType ( n0 , p , prefix ) and
2834+ result = inferType ( n0 , prefix .appendInverse ( path ) ) and
2835+ n = p .getPattern ( ) and
2836+ not result instanceof UnknownType
27882837 )
2789- // or
2790- // n = p.getPattern() and
2791- // result = inferType(p, path) and
2792- // not result instanceof UnknownType
27932838 )
27942839 }
27952840
@@ -2815,7 +2860,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
28152860 or
28162861 result = inferConstructionReturnType ( n , path )
28172862 or
2818- result = inferClosureType ( n , path )
2863+ result = inferClosureParameterType ( n , path )
28192864 or
28202865 // contextual typing: only propagate type information from surrounding context
28212866 // into a node which has an explicitly unknown type
@@ -2842,7 +2887,12 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
28422887 |
28432888 not Certain:: certainTypeConflict ( n , prefix , path , result )
28442889 or
2845- result instanceof PseudoType and not result instanceof UnknownType // todo
2890+ // propagate closure parameter pseudo types even when there is certain information,
2891+ // but prevent propagation outside of the closure
2892+ exists ( Parameter p |
2893+ result = getClosureParameterPseudoType ( p ) and
2894+ not p = n .( Closure ) .getParameter ( _)
2895+ )
28462896 )
28472897 or
28482898 // If `n` has an explicitly unknown type at `prefix` and at the same time a certain
0 commit comments