@@ -365,10 +365,27 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
365365 module Make2< HasTypeTreeSig TypeMention, InputSig2< TypeMention > Input2> {
366366 private import Input2
367367
368- /** Gets the type at the empty path of `tm`. */
368+ /**
369+ * Gets the non-pseudo root type mentioned at `tm`.
370+ *
371+ * Type mentions are allowed to resolve to `UnknownType` (which this predicate
372+ * will filter away), for example in
373+ *
374+ * ```rust
375+ * let x: Vec<Unresolved> = Vec::new();
376+ * x.push(foo());
377+ * ```
378+ *
379+ * by resolving `Unresolved` to `UnknownType` (that is, treating it as if it was
380+ * `_`), we allow for the element type to be inferred from the return type of
381+ * `foo`.
382+ */
369383 bindingset [ tm]
370384 pragma [ inline_late]
371- private Type getTypeMentionRoot ( TypeMention tm ) { result = tm .getTypeAt ( TypePath:: nil ( ) ) }
385+ private Type getTypeMentionNonPseudoRoot ( TypeMention tm ) {
386+ result = tm .getTypeAt ( TypePath:: nil ( ) ) and
387+ not result instanceof PseudoType
388+ }
372389
373390 /** Provides the input to `IsInstantiationOf`. */
374391 signature module IsInstantiationOfInputSig< HasTypeTreeSig App, HasTypeTreeSig Constraint> {
@@ -644,21 +661,22 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
644661 pragma [ nomagic]
645662 private predicate typeCondition ( Type type , TypeAbstraction abs , TypeMention condition ) {
646663 conditionSatisfiesConstraint ( abs , condition , _, _) and
647- type = getTypeMentionRoot ( condition )
664+ type = getTypeMentionNonPseudoRoot ( condition )
648665 }
649666
650667 pragma [ nomagic]
651668 private predicate typeConstraint ( Type type , TypeMention constraint ) {
652669 conditionSatisfiesConstraint ( _, _, constraint , _) and
653- type = getTypeMentionRoot ( constraint )
670+ type = getTypeMentionNonPseudoRoot ( constraint )
654671 }
655672
656673 predicate potentialInstantiationOf (
657674 TypeMention constraint , TypeAbstraction abs , TypeMention condition
658675 ) {
659676 exists ( Type type |
660677 typeConstraint ( type , constraint ) and typeCondition ( type , abs , condition )
661- )
678+ ) and
679+ conditionSatisfiesConstraint ( _, _, constraint , true )
662680 }
663681 }
664682
@@ -704,8 +722,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
704722 TypeMention constraint
705723 ) {
706724 conditionSatisfiesConstraintTypeAt ( abs , condition , constraint , _, _) and
707- conditionRoot = getTypeMentionRoot ( condition ) and
708- constraintRoot = getTypeMentionRoot ( constraint )
725+ conditionRoot = getTypeMentionNonPseudoRoot ( condition ) and
726+ constraintRoot = getTypeMentionNonPseudoRoot ( constraint )
709727 }
710728
711729 /**
@@ -810,8 +828,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
810828 //
811829 // not exists(countConstraintImplementations(type, constraint)) and
812830 // conditionSatisfiesConstraintTypeAt(abs, condition, constraintMention, _, _) and
813- // getTypeMentionRoot (condition) = abs.getATypeParameter() and
814- // constraint = getTypeMentionRoot (constraintMention)
831+ // getTypeMentionNonPseudoRoot (condition) = abs.getATypeParameter() and
832+ // constraint = getTypeMentionNonPseudoRoot (constraintMention)
815833 // or
816834 countConstraintImplementations ( type , constraintRoot ) > 0 and
817835 rootTypesSatisfaction ( type , constraintRoot , abs , condition , constraintMention ) and
@@ -850,9 +868,9 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
850868 // or
851869 // forall(TypeAbstraction abs, TypeMention condition, TypeMention constraintMention |
852870 // conditionSatisfiesConstraintTypeAt(abs, condition, constraintMention, _, _) and
853- // getTypeMentionRoot (condition) = abs.getATypeParameter()
871+ // getTypeMentionNonPseudoRoot (condition) = abs.getATypeParameter()
854872 // |
855- // not constraint = getTypeMentionRoot (constraintMention)
873+ // not constraint = getTypeMentionNonPseudoRoot (constraintMention)
856874 // )
857875 // ) and
858876 (
0 commit comments