Additional comments and testing related to SRTP resolution (#3967)

* Fix Oddities in statically resolved method constraints and method overloading

* no return type needed before proceeding to overload resolution

* fix tests

* unwind changes

* revert to be cleanup only

* revert to be cleanup only

* revert to be cleanup only

* revert to be cleanup only

* adjsut test

* test doesn't pass peverify

* test doesn't pass peverify

* apply code review

src/fsharp/ConstraintSolver.fs

@@ -1004,10 +1004,22 @@ and SolveDimensionlessNumericType (csenv:ConstraintSolverEnv) ndeep m2 trace ty
     | None ->
         CompleteD
 
-/// We do a bunch of fakery to pretend that primitive types have certain members. 
-/// We pretend int and other types support a number of operators.  In the actual IL for mscorlib they 
-/// don't, however the type-directed static optimization rules in the library code that makes use of this 
-/// will deal with the problem. 
+/// Attempt to solve a statically resolved member constraint.
+///
+/// 1. We do a bunch of fakery to pretend that primitive types have certain members. 
+///    We pretend int and other types support a number of operators.  In the actual IL for mscorlib they 
+///    don't. The type-directed static optimization rules in the library code that makes use of this 
+///    will deal with the problem. 
+///
+/// 2. Some additional solutions are forced prior to generalization (permitWeakResolution=true).  These are, roughly speaking, rules
+///    for binary-operand constraints arising from constructs such as "1.0 + x" where "x" is an unknown type. THe constraint here
+///    involves two type parameters - one for the left, and one for the right.  The left is already known to be Double.
+///    In this situation (and in the absence of other evidence prior to generalization), constraint solving forces an assumption that 
+///    the right is also Double - this is "weak" because there is only weak evidence for it.
+///
+///    permitWeakResolution also applies to resolutions of multi-type-variable constraints via method overloads.  Method overloading gets applied even if
+///    only one of the two type variables is known
+///    
 and SolveMemberConstraint (csenv:ConstraintSolverEnv) ignoreUnresolvedOverload permitWeakResolution ndeep m2 trace (TTrait(tys, nm, memFlags, argtys, rty, sln)): OperationResult<bool> = trackErrors {
     // Do not re-solve if already solved
     if sln.Value.IsSome then return true else
@@ -1065,7 +1077,7 @@ and SolveMemberConstraint (csenv:ConstraintSolverEnv) ignoreUnresolvedOverload p
                // The rule is triggered by these sorts of inputs when permitWeakResolution=true
                //    float * 'a 
                //    'a * float 
-               //    decimal<'u> * 'a <---
+               //    decimal<'u> * 'a
                   (let checkRuleAppliesInPreferenceToMethods argty1 argty2 = 
                      // Check that at least one of the argument types is numeric
                      (IsNumericOrIntegralEnumType g argty1) && 
@@ -1314,7 +1326,7 @@ and SolveMemberConstraint (csenv:ConstraintSolverEnv) ignoreUnresolvedOverload p
 
           // Now check if there are no feasible solutions at all
           match minfos, recdPropSearch, anonRecdPropSearch with 
-          | [], None, None when not (tys |> List.exists (isAnyParTy g)) ->
+          | [], None, None when MemberConstraintIsReadyForStrongResolution csenv traitInfo ->
               if tys |> List.exists (isFunTy g) then 
                   return! ErrorD (ConstraintSolverError(FSComp.SR.csExpectTypeWithOperatorButGivenFunction(DecompileOpName nm), m, m2)) 
               elif tys |> List.exists (isAnyTupleTy g) then 
@@ -1387,14 +1399,21 @@ and SolveMemberConstraint (csenv:ConstraintSolverEnv) ignoreUnresolvedOverload p
               | _ -> 
                   let support = GetSupportOfMemberConstraint csenv traitInfo
                   let frees = GetFreeTyparsOfMemberConstraint csenv traitInfo
-                  // If there's nothing left to learn then raise the errors 
-                  if (permitWeakResolution && isNil support) || isNil frees then do! errors
+
+                  // If there's nothing left to learn then raise the errors.
+                  // Note: we should likely call MemberConstraintIsReadyForResolution here when permitWeakResolution=false but for stability
+                  // reasons we use the more restrictive isNil frees.
+                  if (permitWeakResolution && MemberConstraintIsReadyForWeakResolution csenv traitInfo) || isNil frees then 
+                      do! errors  
                   // Otherwise re-record the trait waiting for canonicalization 
-                  else do! AddMemberConstraint csenv ndeep m2 trace traitInfo support frees
-                  return!
-                       match errors with
-                       | ErrorResult (_, UnresolvedOverloading _) when not ignoreUnresolvedOverload && (not (nm = "op_Explicit" || nm = "op_Implicit")) -> ErrorD LocallyAbortOperationThatFailsToResolveOverload
-                       | _ -> ResultD TTraitUnsolved
+                  else
+                      do! AddMemberConstraint csenv ndeep m2 trace traitInfo support frees
+
+                  match errors with
+                  | ErrorResult (_, UnresolvedOverloading _) when not ignoreUnresolvedOverload && (not (nm = "op_Explicit" || nm = "op_Implicit")) ->
+                      return! ErrorD LocallyAbortOperationThatFailsToResolveOverload
+                  | _ -> 
+                      return TTraitUnsolved
      }
     return! RecordMemberConstraintSolution csenv.SolverState m trace traitInfo res
   }
@@ -1475,7 +1494,7 @@ and TransactMemberConstraintSolution traitInfo (trace:OptionalTrace) sln  =
 /// That is, don't perform resolution if more nominal information may influence the set of available overloads 
 and GetRelevantMethodsForTrait (csenv:ConstraintSolverEnv) permitWeakResolution nm (TTrait(tys, _, memFlags, argtys, rty, soln) as traitInfo): MethInfo list =
     let results = 
-        if permitWeakResolution || isNil (GetSupportOfMemberConstraint csenv traitInfo) then
+        if permitWeakResolution || MemberConstraintSupportIsReadyForDeterminingOverloads csenv traitInfo then
             let m = csenv.m
             let minfos = 
                 match memFlags.MemberKind with
@@ -1483,13 +1502,9 @@ and GetRelevantMethodsForTrait (csenv:ConstraintSolverEnv) permitWeakResolution
                     tys |> List.map (GetIntrinsicConstructorInfosOfType csenv.SolverState.InfoReader m)
                 | _ ->
                     tys |> List.map (GetIntrinsicMethInfosOfType csenv.SolverState.InfoReader (Some nm, AccessibleFromSomeFSharpCode, AllowMultiIntfInstantiations.Yes) IgnoreOverrides m) 
-            /// Merge the sets so we don't get the same minfo from each side 
-            /// We merge based on whether minfos use identical metadata or not. 
 
-            /// REVIEW: Consider the pathological cases where this may cause a loss of distinction 
-            /// between potential overloads because a generic instantiation derived from the left hand type differs 
-            /// to a generic instantiation for an operator based on the right hand type. 
-            
+            // Merge the sets so we don't get the same minfo from each side 
+            // We merge based on whether minfos use identical metadata or not. 
             let minfos = List.reduce (ListSet.unionFavourLeft MethInfo.MethInfosUseIdenticalDefinitions) minfos
             
             /// Check that the available members aren't hiding a member from the parent (depth 1 only)
@@ -1503,7 +1518,7 @@ and GetRelevantMethodsForTrait (csenv:ConstraintSolverEnv) permitWeakResolution
             []
     // The trait name "op_Explicit" also covers "op_Implicit", so look for that one too.
     if nm = "op_Explicit" then 
-        results @ GetRelevantMethodsForTrait (csenv:ConstraintSolverEnv) permitWeakResolution "op_Implicit" (TTrait(tys, "op_Implicit", memFlags, argtys, rty, soln))
+        results @ GetRelevantMethodsForTrait csenv permitWeakResolution "op_Implicit" (TTrait(tys, "op_Implicit", memFlags, argtys, rty, soln))
     else
         results
 
@@ -1512,10 +1527,28 @@ and GetRelevantMethodsForTrait (csenv:ConstraintSolverEnv) permitWeakResolution
 and GetSupportOfMemberConstraint (csenv:ConstraintSolverEnv) (TTrait(tys, _, _, _, _, _)) =
     tys |> List.choose (tryAnyParTyOption csenv.g)
     
-/// All the typars relevant to the member constraint *)
+/// Check if the support is fully solved.  
+and SupportOfMemberConstraintIsFullySolved (csenv:ConstraintSolverEnv) (TTrait(tys, _, _, _, _, _)) =
+    tys |> List.forall (isAnyParTy csenv.g >> not)
+
+// This may be relevant to future bug fixes, see https://github.com/Microsoft/visualfsharp/issues/3814
+// /// Check if some part of the support is solved.  
+// and SupportOfMemberConstraintIsPartiallySolved (csenv:ConstraintSolverEnv) (TTrait(tys, _, _, _, _, _)) =
+//     tys |> List.exists (isAnyParTy csenv.g >> not)
+    
+/// Get all the unsolved typars (statically resolved or not) relevant to the member constraint
 and GetFreeTyparsOfMemberConstraint (csenv:ConstraintSolverEnv) (TTrait(tys, _, _, argtys, rty, _)) =
     freeInTypesLeftToRightSkippingConstraints csenv.g (tys@argtys@ Option.toList rty)
 
+and MemberConstraintIsReadyForWeakResolution csenv traitInfo =
+   SupportOfMemberConstraintIsFullySolved csenv traitInfo
+
+and MemberConstraintIsReadyForStrongResolution csenv traitInfo =
+   SupportOfMemberConstraintIsFullySolved csenv traitInfo
+
+and MemberConstraintSupportIsReadyForDeterminingOverloads csenv traitInfo =
+   SupportOfMemberConstraintIsFullySolved csenv traitInfo
+
 /// Re-solve the global constraints involving any of the given type variables. 
 /// Trait constraints can't always be solved using the pessimistic rules. We only canonicalize 
 /// them forcefully (permitWeakResolution=true) prior to generalization. 

tests/fsharp/core/members/basics-hw-mutrec/test.fs

@@ -5549,7 +5549,7 @@ module Devdiv2_Bug_5385 =
                     g "1" |> ignore; // note, use of non-generic 'g' within a generic, generalized memoized function
                     2
 
-        and g : string -> int = memoize f // note, computed function value using generic f at an instance
+        and g : string -> int = memoize f // note, computed function value using generic �f� at an instance
         g "1"                                        
 
     let res = test3e()

tests/fsharp/core/members/ops-mutrec/test.fs

@@ -217,16 +217,15 @@ module BasicOverloadTests =
     // This gets type DateTime -> DateTime -> TimeSpan, through non-conservative resolution.
     let f6 x1 (x2:System.DateTime) = x1 - x2
 
-    // This gets type TimeSpan -> TimeSpan -> TimeSpan, through non-conservative resolution.
+    // This gets type TimeSpan -> TimeSpan -> TimeSpan, through default type propagation
     let f7 x1 (x2:System.TimeSpan) = x1 - x2
 
-    // This gets type TimeSpan -> TimeSpan -> TimeSpan, through non-conservative resolution.
+    // This gets type TimeSpan -> TimeSpan -> TimeSpan, through default type propagation
     let f8 x1 (x2:System.TimeSpan) = x2 - x1
 
-    // This gets type TimeSpan -> TimeSpan -> TimeSpan, through non-conservative resolution.
+    // This gets type TimeSpan -> TimeSpan -> TimeSpan, through default type propagation
     let f9 (x1:System.TimeSpan) x2 = x1 - x2
 
-
     // This gets type TimeSpan -> TimeSpan -> TimeSpan
     let f10 x1 (x2:System.TimeSpan) = x1 + x2
 

tests/fsharp/core/members/ops/test.fsx

@@ -219,16 +219,16 @@ module BasicOverloadTests =
     // This gets type int -> int
     let f5 x = 1 - x
 
-    // This gets type DateTime -> DateTime -> TimeSpan, through non-conservative resolution.
-    let f6 x1 (x2:System.DateTime) = x1 - x2
+    // // This gets type DateTime -> DateTime -> TimeSpan, through non-conservative resolution.
+    // let f6 x1 (x2:System.DateTime) = x1 - x2
 
-    // This gets type TimeSpan -> TimeSpan -> TimeSpan, through non-conservative resolution.
+    // This gets type TimeSpan -> TimeSpan -> TimeSpan, through default type propagation
     let f7 x1 (x2:System.TimeSpan) = x1 - x2
 
-    // This gets type TimeSpan -> TimeSpan -> TimeSpan, through non-conservative resolution.
+    // This gets type TimeSpan -> TimeSpan -> TimeSpan, through default type propagation
     let f8 x1 (x2:System.TimeSpan) = x2 - x1
 
-    // This gets type TimeSpan -> TimeSpan -> TimeSpan, through non-conservative resolution.
+    // This gets type TimeSpan -> TimeSpan -> TimeSpan, through default type propagation
     let f9 (x1:System.TimeSpan) x2 = x1 - x2
 
 

tests/fsharp/core/subtype/test.fsx

@@ -232,8 +232,31 @@ module SomeRandomOperatorConstraints = begin
 
     let f2 x : float = x * x 
     let f3 x (y:float) = x * y
+
     //let neg4 x (y:System.DateTime) = x + y
+
+    // This example resolves the type of "y" to "TimeSpam". It checks that a single "+" overload between 
+    // two different types DateTime and TimeSpan get resolved via 
+    // via weak SRTP resolution using a DateTime constraint alone.
     let f5 (x:DateTime) y = x + y
+
+    // This example checks a use of TimeSpan/DateTime overloads
+    let f5b (x:DateTime) (y:DateTime) = (x - y) 
+
+
+    // This example checks a use of TimeSpan/DateTime overloads
+    let f5b2 (x:DateTime) (y:TimeSpan) = (x - y) 
+
+    // This example coincidentally checks that the return type is not taken into account before the list of method overloads
+    // is prepared in SRTP resolution.  That is the type of (a - b) is immediately known (and we can use it for
+    // dot-notation name resolution of .TotalSeconds) _immediately_ that the types of a and b are
+    // known and _prior_ to generalization.
+    let f5c (x: DateTime) (y:DateTime) = 
+        (x  - y).TotalSeconds |> int
+
+    let f5c2 (x: DateTime) (y:TimeSpan) = 
+        (x  - y).Second |> int
+
     let f6 (x:int64) y = x + y
     let f7 x y : int64 = x + y
     let f8 x = Seq.reduce (+) x
@@ -1744,6 +1767,51 @@ module GenericPropertyConstraintSolvedByRecord =
 
     let v = print_foo_memb { foo=1 } 
 
+
+/// In this case, the presence of the Method(obj) overload meant overload resolution was being applied and resolving to that
+/// overload, even before the full signature of the trait constraint was known.
+module MethodOverloadingForTraitConstraintsIsNotDeterminedUntilSignatureIsKnnown =
+    type X =
+        static member Method (a: obj) = 1
+        static member Method (a: int) = 2
+        static member Method (a: int64) = 3
+
+
+    let inline Test< ^t, ^a when ^t: (static member Method: ^a -> int)> (value: ^a) =
+        ( ^t: (static member Method: ^a -> int)(value))
+
+    let inline Test2< ^t> a = Test<X, ^t> a
+
+    // NOTE, this is seen to be a bug, see https://github.com/Microsoft/visualfsharp/issues/3814
+    // The result should be 2.  
+    // This test has been added to pin down current behaviour pending a future bug fix.
+    check "slvde0vver90u1" (Test2<int> 0) 1
+    check "slvde0vver90u2" (Test2<int64> 0L) 1
+
+/// In this case, the presence of the "Equals" method on System.Object was causing method overloading to be resolved too
+/// early, when ^t was not yet known.  The underlying problem was that we were proceeding with weak resolution
+/// even for a single-support-type trait constraint.
+module MethodOverloadingForTraitConstraintsWhereSomeMethodsComeFromObjectTypeIsNotDeterminedTooEarly =
+    type Test() =
+         member __.Equals (_: Test) = true
+
+    //let inline Equals(a: obj) (b: ^t) =
+    //    match a with
+    //    | :? ^t as x -> (^t: (member Equals: ^t -> bool) (b, x))
+    //    | _-> false
+
+    let a  = Test()
+    let b  = Test()
+
+    // NOTE, this is seen to be a bug, see https://github.com/Microsoft/visualfsharp/issues/3814
+    //
+    // The result should be true.  
+    //
+    // This test should be added to pin down current behaviour pending a future bug fix.
+    //
+    // However the code generated fails peverify.exe so even the pin-down test has been removed for now.
+    //check "cewjewcwec09ew" (Equals a b) false
+
 module SRTPFix = 
 
     open System

tests/fsharp/typecheck/sigs/neg99.bsl

@@ -3,4 +3,4 @@ neg99.fs(19,16,19,64): typecheck error FS0077: Member constraints with the name
 
 neg99.fs(22,18,22,64): typecheck error FS0077: Member constraints with the name 'op_Explicit' are given special status by the F# compiler as certain .NET types are implicitly augmented with this member. This may result in runtime failures if you attempt to invoke the member constraint from your own code.
 
-neg99.fs(25,39,25,43): typecheck error FS0043: The type 'CrashFSC.OhOh.MyByte' does not support a conversion to the type 'CrashFSC.OhOh.MyByte'
+neg99.fs(25,39,25,43): typecheck error FS0043: The type 'CrashFSC.OhOh.MyByte' does not support a conversion to the type 'CrashFSC.OhOh.MyByte'
\ No newline at end of file