@@ -796,6 +796,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
796
796
)
797
797
}
798
798
799
+ /**
800
+ * Holds if there is multiple ways in which a type with `conditionRoot` at
801
+ * the root can satisfy a constraint with `constraintRoot` at the root.
802
+ */
803
+ predicate multipleConstraintImplementations ( Type conditionRoot , Type constraintRoot ) {
804
+ countConstraintImplementations ( conditionRoot , constraintRoot ) > 1
805
+ }
806
+
799
807
/**
800
808
* Holds if `baseMention` is a (transitive) base type mention of `sub`,
801
809
* and `t` is mentioned (implicitly) at `path` inside `baseMention`. For
@@ -902,14 +910,20 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
902
910
{
903
911
private import Input
904
912
913
+ /** Holds if the type tree has the type `type` and should satisfy `constraint`. */
914
+ pragma [ nomagic]
915
+ private predicate hasTypeConstraint ( HasTypeTree term , Type type , Type constraint ) {
916
+ type = term .getTypeAt ( TypePath:: nil ( ) ) and
917
+ relevantConstraint ( term , constraint )
918
+ }
919
+
905
920
private module IsInstantiationOfInput implements IsInstantiationOfInputSig< HasTypeTree > {
906
921
predicate potentialInstantiationOf ( HasTypeTree tt , TypeAbstraction abs , TypeMention cond ) {
907
922
exists ( Type constraint , Type type |
908
- type = tt .getTypeAt ( TypePath:: nil ( ) ) and
909
- relevantConstraint ( tt , constraint ) and
923
+ hasTypeConstraint ( tt , type , constraint ) and
910
924
rootTypesSatisfaction ( type , constraint , abs , cond , _) and
911
925
// We only need to check instantiations where there are multiple candidates.
912
- countConstraintImplementations ( type , constraint ) > 1
926
+ multipleConstraintImplementations ( type , constraint )
913
927
)
914
928
}
915
929
@@ -918,13 +932,6 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
918
932
}
919
933
}
920
934
921
- /** Holds if the type tree has the type `type` and should satisfy `constraint`. */
922
- pragma [ nomagic]
923
- private predicate hasTypeConstraint ( HasTypeTree term , Type type , Type constraint ) {
924
- type = term .getTypeAt ( TypePath:: nil ( ) ) and
925
- relevantConstraint ( term , constraint )
926
- }
927
-
928
935
/**
929
936
* Holds if `tt` satisfies `constraint` through `abs`, `sub`, and `constraintMention`.
930
937
*/
@@ -944,7 +951,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
944
951
// When there are multiple ways the type could implement the
945
952
// constraint we need to find the right implementation, which is the
946
953
// one where the type instantiates the precondition.
947
- if countConstraintImplementations ( type , constraint ) > 1
954
+ if multipleConstraintImplementations ( type , constraint )
948
955
then
949
956
IsInstantiationOf< HasTypeTree , IsInstantiationOfInput > :: isInstantiationOf ( tt , abs , sub )
950
957
else any ( )
0 commit comments