@@ -365,10 +365,24 @@ 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 ) {
385+ private Type getTypeMentionNonPseudoRoot ( TypeMention tm ) {
372386 result = tm .getTypeAt ( TypePath:: nil ( ) ) and
373387 not result instanceof PseudoType
374388 }
@@ -647,13 +661,13 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
647661 pragma [ nomagic]
648662 private predicate typeCondition ( Type type , TypeAbstraction abs , TypeMention condition ) {
649663 conditionSatisfiesConstraint ( abs , condition , _, _) and
650- type = getTypeMentionRoot ( condition )
664+ type = getTypeMentionNonPseudoRoot ( condition )
651665 }
652666
653667 pragma [ nomagic]
654668 private predicate typeConstraint ( Type type , TypeMention constraint ) {
655669 conditionSatisfiesConstraint ( _, _, constraint , _) and
656- type = getTypeMentionRoot ( constraint )
670+ type = getTypeMentionNonPseudoRoot ( constraint )
657671 }
658672
659673 predicate potentialInstantiationOf (
@@ -708,8 +722,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
708722 TypeMention constraint
709723 ) {
710724 conditionSatisfiesConstraintTypeAt ( abs , condition , constraint , _, _) and
711- conditionRoot = getTypeMentionRoot ( condition ) and
712- constraintRoot = getTypeMentionRoot ( constraint )
725+ conditionRoot = getTypeMentionNonPseudoRoot ( condition ) and
726+ constraintRoot = getTypeMentionNonPseudoRoot ( constraint )
713727 }
714728
715729 /**
@@ -814,8 +828,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
814828 //
815829 // not exists(countConstraintImplementations(type, constraint)) and
816830 // conditionSatisfiesConstraintTypeAt(abs, condition, constraintMention, _, _) and
817- // getTypeMentionRoot (condition) = abs.getATypeParameter() and
818- // constraint = getTypeMentionRoot (constraintMention)
831+ // getTypeMentionNonPseudoRoot (condition) = abs.getATypeParameter() and
832+ // constraint = getTypeMentionNonPseudoRoot (constraintMention)
819833 // or
820834 countConstraintImplementations ( type , constraintRoot ) > 0 and
821835 rootTypesSatisfaction ( type , constraintRoot , abs , condition , constraintMention ) and
@@ -854,9 +868,9 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
854868 // or
855869 // forall(TypeAbstraction abs, TypeMention condition, TypeMention constraintMention |
856870 // conditionSatisfiesConstraintTypeAt(abs, condition, constraintMention, _, _) and
857- // getTypeMentionRoot (condition) = abs.getATypeParameter()
871+ // getTypeMentionNonPseudoRoot (condition) = abs.getATypeParameter()
858872 // |
859- // not constraint = getTypeMentionRoot (constraintMention)
873+ // not constraint = getTypeMentionNonPseudoRoot (constraintMention)
860874 // )
861875 // ) and
862876 (
0 commit comments