@@ -626,6 +626,37 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
626626 )
627627 }
628628
629+ pragma [ nomagic]
630+ private predicate hasTypeParameterAt (
631+ App app , TypeAbstraction abs , Constraint constraint , TypePath path , TypeParameter tp
632+ ) {
633+ tp = getTypeAt ( app , abs , constraint , path ) and
634+ tp = abs .getATypeParameter ( )
635+ }
636+
637+ pragma [ nomagic]
638+ private predicate hasTypeParameterAt2 (
639+ App app , TypeAbstraction abs , Constraint constraint , TypePath path1 , TypePath path2
640+ ) {
641+ exists ( TypeParameter tp |
642+ hasTypeParameterAt ( app , abs , constraint , path1 , tp ) and
643+ hasTypeParameterAt ( app , abs , constraint , path2 , tp ) and
644+ path1 != path2
645+ )
646+ }
647+
648+ private Type getNonPseudoTypeAt ( App app , TypePath path ) {
649+ result = app .getTypeAt ( path ) and not isPseudoType ( result )
650+ }
651+
652+ pragma [ nomagic]
653+ private Type getNonPseudoTypeAt2 (
654+ App app , TypeAbstraction abs , Constraint constraint , TypeParameter tp , TypePath path
655+ ) {
656+ hasTypeParameterAt ( app , abs , constraint , path , tp ) and
657+ result = getNonPseudoTypeAt ( app , path )
658+ }
659+
629660 /**
630661 * Holds if `app` is _not_ a possible instantiation of `constraint`, because `app`
631662 * and `constraint` differ on concrete types at `path`.
@@ -649,22 +680,16 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
649680 exists ( Type t , Type t2 |
650681 t = getTypeAt ( app , abs , constraint , path ) and
651682 not t = abs .getATypeParameter ( ) and
652- app .getTypeAt ( path ) = t2 and
653- not isPseudoType ( t2 ) and
683+ t2 = getNonPseudoTypeAt ( app , path ) and
654684 t2 != t
655685 )
656686 or
657687 // satisfiesConcreteTypes(app, abs, constraint) and
658688 exists ( TypeParameter tp , TypePath path2 , Type t , Type t2 |
659- tp = getTypeAt ( app , abs , constraint , path ) and
660- tp = getTypeAt ( app , abs , constraint , path2 ) and
661- tp = abs .getATypeParameter ( ) and
662- path != path2 and
663- app .getTypeAt ( path ) = t and
664- app .getTypeAt ( path2 ) = t2 and
665- not isPseudoType ( t ) and
666- not isPseudoType ( t2 ) and
667- t != t2
689+ t = getNonPseudoTypeAt2 ( app , abs , constraint , tp , path ) and
690+ t2 = getNonPseudoTypeAt2 ( app , abs , constraint , tp , path2 ) and
691+ t != t2 and
692+ path != path2
668693 )
669694 }
670695 }
@@ -1030,10 +1055,9 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
10301055 ambiguous = true
10311056 or
10321057 forall ( TypePath prefix , TypeAbstraction other |
1033- typeAbstractionHasAmbiguousConstraintAt ( abs , constraintRoot , other , prefix )
1058+ typeAbstractionHasAmbiguousConstraintAt ( abs , constraintRoot , other , prefix ) and
1059+ prefix .isPrefixOf ( path )
10341060 |
1035- not prefix .isPrefixOf ( path )
1036- or
10371061 TermIsInstantiationOfCondition:: isNotInstantiationOf ( term , other , _, _)
10381062 ) and
10391063 ambiguous = false
0 commit comments