Regression in overload resolution

[gusty]

After updating to F#9 I'm observing many regressions in overload resolution.
Here I managed to capture one of them, this one keeps failing even using the langversion flag.

Repro steps

Try this in fsi

type ToSeq =
    static member inline Invoke (source: 'FldT) : seq<'T>  =
        let inline call (mthd: ^M, input1: ^I) = ((^M or ^I) : (static member ToSeq : _*_ -> _) input1, mthd)
        call (Unchecked.defaultof<ToSeq>, source)

    static member inline ToSeq (x: 'Foldable                      , _: ToSeq) = (^Foldable: (static member ToSeq : _ -> _) x)
    static member inline ToSeq (_: 'T when 'T: null and 'T: struct, _: ToSeq) = ()

type Append =    
    static member inline Append (x: 'AltT        , y: 'AltT           , _: obj   ) = (^AltT : (static member Append : _*_ -> _) x, y) : 'AltT
    static member inline Append (_: ^t when ^t: null and ^t: struct, _, _: obj   ) = ()
    static member inline Append (x: Result<_,_>  , y                  , _: Append) = match x, y with Ok _, _ -> x | Error x, Error y -> Error (x + y) | _, _ -> y

    static member inline Invoke (x: 'AltT) (y: 'AltT) : 'AltT =
        let inline call (mthd: ^M, input1: ^I, input2: ^I) = ((^M or ^I) : (static member Append : _*_*_ -> _) input1, input2, mthd)
        call (Unchecked.defaultof<Append>, x, y)

    static member inline Append (x: 'R -> 'AltT  , y                  , _: Append) = fun r -> Append.Invoke (x r) (y r)

type Choice =
    static member inline Choice (x: ref<'RAltT>, _: obj) =
        let t = ToSeq.Invoke x.Value
        use e = t.GetEnumerator ()
        e.MoveNext() |> ignore
        let mutable res = e.Current
        while e.MoveNext() do res <- Append.Invoke res e.Current
        res

    static member inline Choice (x: ref<'FAltT> , _: Choice) = (^FAltT : (static member Choice : _ -> _) x.Value) : 'AltT
    static member inline Choice (_: ref< ^t> when ^t: null and ^t: struct, _: Choice) = ()

    static member inline Invoke (x: 'FAltT) : 'AltT =
        let inline call (mthd: ^M, input1: ^I) = ((^M or ^I) : (static member Choice : _*_ -> _) (ref input1, mthd))
        call (Unchecked.defaultof<Choice>, x)

type WrappedSeqE<'s> = WrappedSeqE of 's seq with static member ToSeq (WrappedSeqE x) = x

let v1 = [Ok 1; Error "a" ]
let v2 = Choice.Invoke (WrappedSeqE v1)

Expected behavior

val v2: Result<int,string> = Ok 1

Actual behavior

error FS0465: Type inference problem too complicated (maximum iteration depth reached). Consider adding further type annotations.

Stopped due to error

Known workarounds

Make the last two lines a single one: let v = Choice.Invoke (WrappedSeqE [Ok 1; Error "a" ])

Related information

Provide any related information (optional):

• Operating system: Windows
• .NET Runtime kind (.NET Core, .NET Framework, Mono): net9 / F#9
• Editing Tools (e.g. Visual Studio Version, Visual Studio): VIsual Studio: Microsoft (R) F# Interactive version 12.9.101.0 for F# 9.0* Operating system

[T-Gro]

The current depth limit is 300 calls within type inference (ConstraintSolver), I will check how it behaved before net9 and how much more would be needed to make this code compile in net9. There have been changes in the code for ConstraintSolver which can in turn lead to more recursive invocations of type solving.

[T-Gro]

@gusty:

I found out there was an infinite loop in type inference (= limit increase would not help) when the following was encountered:
static member inline ToSeq (_: 'T when 'T: null and 'T: struct, _: ToSeq) = ()

Is there a reason for this annotation I am not seeing?
I have made a fix that avoids the infinity recursion, but I would not want to also raise a new error when these two constraints are defined together.

Or is this somewhat intentional when writing SRTP members like this, to define a member which can be never satisfied by any type?

[gusty]

@T-Gro thanks for having a look at this

Or is this somewhat intentional when writing SRTP members like this, to define a member which can be never satisfied by any type?

Yes, in many cases we need to generate ambiguity in order to avoid overload resolution to resolve earlier. For those cases we have what I call "the impossible overload", which generates the ambiguity needed and at the same time provides no danger of resolving to it.

I found out there was an infinite loop in type inference (= limit increase would not help) when the following was encountered:

I suspected about an infinite loop, but of course, this worked since F# 2.0