@@ -796,6 +796,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
796796)
797797}
798798
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+
799807/**
800808 * Holds if `baseMention` is a (transitive) base type mention of `sub`,
801809 * and `t` is mentioned (implicitly) at `path` inside `baseMention`. For
@@ -902,14 +910,20 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
902910{
903911private import Input
904912
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+
905920private module IsInstantiationOfInputimplements IsInstantiationOfInputSig< HasTypeTree > {
906921predicate potentialInstantiationOf ( HasTypeTree tt , TypeAbstraction abs , TypeMention cond ) {
907922exists ( Type constraint , Type type |
908- type = tt .getTypeAt ( TypePath:: nil ( ) ) and
909- relevantConstraint ( tt , constraint ) and
923+ hasTypeConstraint ( tt , type , constraint ) and
910924rootTypesSatisfaction ( type , constraint , abs , cond , _) and
911925// We only need to check instantiations where there are multiple candidates.
912- countConstraintImplementations ( type , constraint ) > 1
926+ multipleConstraintImplementations ( type , constraint )
913927)
914928}
915929
@@ -918,13 +932,6 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
918932}
919933}
920934
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-
928935/**
929936 * Holds if `tt` satisfies `constraint` through `abs`, `sub`, and `constraintMention`.
930937 */
@@ -944,7 +951,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
944951// When there are multiple ways the type could implement the
945952// constraint we need to find the right implementation, which is the
946953// one where the type instantiates the precondition.
947- if countConstraintImplementations ( type , constraint ) > 1
954+ if multipleConstraintImplementations ( type , constraint )
948955then
949956 IsInstantiationOf< HasTypeTree , IsInstantiationOfInput > :: isInstantiationOf ( tt , abs , sub )
950957else any ( )