@@ -463,24 +463,34 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
463463 * Gets the path to the `i`th occurrence of `tp` within `tm` per some
464464 * arbitrary order, if any.
465465 */
466+ pragma [ nomagic]
466467 private TypePath getNthTypeParameterPath ( TypeMention tm , TypeParameter tp , int i ) {
467468 result =
468469 rank [ i + 1 ] ( TypePath path | tp = tm .resolveTypeAt ( path ) and relevantTypeMention ( tm ) | path )
469470 }
470471
472+ pragma [ nomagic]
473+ private predicate typeParametersEqualFromIndexBase (
474+ App app , TypeAbstraction abs , TypeMention tm , TypeParameter tp , TypePath path
475+ ) {
476+ path = getNthTypeParameterPath ( tm , tp , 0 ) and
477+ satisfiesConcreteTypes ( app , abs , tm ) and
478+ // no need to compute this predicate if there is only one path
479+ exists ( getNthTypeParameterPath ( tm , tp , 1 ) )
480+ }
481+
471482 pragma [ nomagic]
472483 private predicate typeParametersEqualFromIndex (
473484 App app , TypeAbstraction abs , TypeMention tm , TypeParameter tp , Type t , int i
474485 ) {
475- satisfiesConcreteTypes ( app , abs , tm ) and
476486 exists ( TypePath path |
477- path = getNthTypeParameterPath ( tm , tp , i ) and
478487 t = app .getTypeAt ( path ) and
479488 if i = 0
480- then
481- // no need to compute this predicate if there is only one path
482- exists ( getNthTypeParameterPath ( tm , tp , 1 ) )
483- else typeParametersEqualFromIndex ( app , abs , tm , tp , t , i - 1 )
489+ then typeParametersEqualFromIndexBase ( app , abs , tm , tp , path )
490+ else (
491+ typeParametersEqualFromIndex ( app , abs , tm , tp , t , i - 1 ) and
492+ path = getNthTypeParameterPath ( tm , tp , i )
493+ )
484494 )
485495 }
486496
0 commit comments