@@ -731,20 +731,24 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
731731 IsInstantiationOfInputSig< TypeMentionTypeTree >
732732 {
733733 pragma [ nomagic]
734- private predicate typeCondition ( Type type , TypeAbstraction abs , TypeMentionTypeTree lhs ) {
735- conditionSatisfiesConstraint ( abs , lhs , _) and type = resolveTypeMentionRoot ( lhs )
734+ private predicate typeCondition (
735+ Type type , TypeAbstraction abs , TypeMentionTypeTree condition
736+ ) {
737+ conditionSatisfiesConstraint ( abs , condition , _) and
738+ type = resolveTypeMentionRoot ( condition )
736739 }
737740
738741 pragma [ nomagic]
739- private predicate typeConstraint ( Type type , TypeMentionTypeTree rhs ) {
740- conditionSatisfiesConstraint ( _, _, rhs ) and type = resolveTypeMentionRoot ( rhs )
742+ private predicate typeConstraint ( Type type , TypeMentionTypeTree constraint ) {
743+ conditionSatisfiesConstraint ( _, _, constraint ) and
744+ type = resolveTypeMentionRoot ( constraint )
741745 }
742746
743747 predicate potentialInstantiationOf (
744- TypeMentionTypeTree condition , TypeAbstraction abs , TypeMention constraint
748+ TypeMentionTypeTree constraint , TypeAbstraction abs , TypeMention condition
745749 ) {
746750 exists ( Type type |
747- typeConstraint ( type , condition ) and typeCondition ( type , abs , constraint )
751+ typeConstraint ( type , constraint ) and typeCondition ( type , abs , condition )
748752 )
749753 }
750754 }
@@ -761,20 +765,20 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
761765 constraint .resolveTypeAt ( path ) = t
762766 or
763767 // recursive case
764- exists ( TypeAbstraction midAbs , TypeMention midSup , TypeMention midSub |
765- conditionSatisfiesConstraint ( abs , condition , midSup ) and
766- // NOTE: `midAbs` describe the free type variables in `midSub `, hence
768+ exists ( TypeAbstraction midAbs , TypeMention midConstraint , TypeMention midCondition |
769+ conditionSatisfiesConstraint ( abs , condition , midConstraint ) and
770+ // NOTE: `midAbs` describe the free type variables in `midCondition `, hence
767771 // we use that for instantiation check.
768- IsInstantiationOf< TypeMentionTypeTree , IsInstantiationOfInput > :: isInstantiationOf ( midSup ,
769- midAbs , midSub )
772+ IsInstantiationOf< TypeMentionTypeTree , IsInstantiationOfInput > :: isInstantiationOf ( midConstraint ,
773+ midAbs , midCondition )
770774 |
771- conditionSatisfiesConstraintTypeAt ( midAbs , midSub , constraint , path , t ) and
775+ conditionSatisfiesConstraintTypeAt ( midAbs , midCondition , constraint , path , t ) and
772776 not t = midAbs .getATypeParameter ( )
773777 or
774778 exists ( TypePath prefix , TypePath suffix , TypeParameter tp |
775779 tp = midAbs .getATypeParameter ( ) and
776- conditionSatisfiesConstraintTypeAt ( midAbs , midSub , constraint , prefix , tp ) and
777- instantiatesWith ( midSup , midSub , tp , suffix , t ) and
780+ conditionSatisfiesConstraintTypeAt ( midAbs , midCondition , constraint , prefix , tp ) and
781+ instantiatesWith ( midConstraint , midCondition , tp , suffix , t ) and
778782 path = prefix .append ( suffix )
779783 )
780784 )
@@ -949,23 +953,24 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
949953 */
950954 pragma [ nomagic]
951955 private predicate hasConstraintMention (
952- HasTypeTree tt , TypeAbstraction abs , TypeMention sub , Type constraint ,
956+ HasTypeTree tt , TypeAbstraction abs , TypeMention condition , Type constraint ,
953957 TypeMention constraintMention
954958 ) {
955959 exists ( Type type | hasTypeConstraint ( tt , type , constraint ) |
956960 not exists ( countConstraintImplementations ( type , constraint ) ) and
957- conditionSatisfiesConstraintTypeAt ( abs , sub , constraintMention , _, _) and
958- resolveTypeMentionRoot ( sub ) = abs .getATypeParameter ( ) and
961+ conditionSatisfiesConstraintTypeAt ( abs , condition , constraintMention , _, _) and
962+ resolveTypeMentionRoot ( condition ) = abs .getATypeParameter ( ) and
959963 constraint = resolveTypeMentionRoot ( constraintMention )
960964 or
961965 countConstraintImplementations ( type , constraint ) > 0 and
962- rootTypesSatisfaction ( type , constraint , abs , sub , constraintMention ) and
966+ rootTypesSatisfaction ( type , constraint , abs , condition , constraintMention ) and
963967 // When there are multiple ways the type could implement the
964968 // constraint we need to find the right implementation, which is the
965969 // one where the type instantiates the precondition.
966970 if multipleConstraintImplementations ( type , constraint )
967971 then
968- IsInstantiationOf< HasTypeTree , IsInstantiationOfInput > :: isInstantiationOf ( tt , abs , sub )
972+ IsInstantiationOf< HasTypeTree , IsInstantiationOfInput > :: isInstantiationOf ( tt , abs ,
973+ condition )
969974 else any ( )
970975 )
971976 }
0 commit comments