Compilation fails depending on runtime path (???)

[gusty]

I will demonstrate a short piece of code, using SRTPs and overload resolution, where the compilation will either succeed or fail, depending on the runtime execution path.

Repro steps

let compiles = true

type A<'t> = A of 't
type B<'t> = B of 't

type Bind = Bind with
    static member (>>=) (A t, f: 'T -> A<'U> ) = f t
    static member (>>=) (B t, f: 'T -> B<'U> ) = f t
    static member inline Invoke (source: 'MT) (binder: 'T -> 'MU) : 'MU =
        let inline call (_mthd: 'M, input: 'I, _output: 'R, f) = ((^M or ^I or ^R) : (static member (>>=) : _*_ -> _) input, f)
        call (Bind, source, Unchecked.defaultof<'MU>, binder)

type Result = Result with
    static member Return (_: A<'a>) = A
    static member Return (_: B<'a>) = B
    static member inline Invoke (x: 'T) : 'MT =
        let inline call (_mthd: ^M, output: ^R) = ((^M or ^R) : (static member Return : _ -> _) output)
        call (Result, Unchecked.defaultof<'MT>) x

type T<'m>    () = class end
type U<'m,'t> () = class end

let inline createT (_: 'mit) =
    let _  = if compiles then Bind.Invoke (Result.Invoke Unchecked.defaultof<'t> : 'mt) ((fun _ -> Result.Invoke (U<'mt,'t>()))) else Unchecked.defaultof<'mit>
    T() : T<'mt>

type T<'m> with static member inline Return (_) = fun (_:'t) -> U() |> Result.Invoke |> createT

// test
let (u: T<A<unit>>) = Result.Invoke ()  // works !!!  Now try with compiles = false (???)

Expected behavior

Should compile or not (hopefully the former) regardless of the content of compiles.

Actual behavior

It compiles if compiles = true but when compiles = false it fails with error FS0073: internal error: Undefined or unsolved type variable: ^_?21440

Known workarounds

Use compile = true but it will execute unnecessarily some piece of code that is used only to drive type inference to create the desired constraints.

Related information

I've tested it in many environments and different versions of F#. Actually I'm seeing this since long time ago (4 years at least) but it's the first time I manage to create a minimal repro.

[realvictorprm]

This is horrible, thank you very very much @gusty for this reproduction!

[TIHan]

Good find and very interesting.

This is a result of the optimizer. For inline functions, if the optimizer sees a conditional where it knows at compile time will only ever be one branch at the call site, it will only output that one branch.

Meaning, in this case, if compiles = false, it's only outputting Unchecked.defaultof<'mit>, effectively becoming:

    let _  = Unchecked.defaultof<'mit>
    T() : T<'mt>

There is probably a bug in the optimizer that causes IlxGen to throw this error which involves a type parameter.

[gusty]

Ok, I see. So, the problem seems to be that at least some part of the type inference is computed after the optimizer pass, which already suppressed the interesting part.

Also, it's interesting to note, that it only shows when I use the static method extensions, with normal let bindings it compiles fine. It's really this specific combination, which happens to be on my plate more often than what it seems.

[TIHan]

This is after type inference, so that shouldn't be doing anything.

At a high-level, this is like the flow of the compiler: Parsing -> TypeChecking -> PostInferenceChecks -> Optimizer -> IlxGen -> Output Assembly

When it's re-writing the expression it might be forgetting to take something into account. The compiler treats methods and let-bound functions as separate entities; means the optimizer has to handle each separately.

Might take a bit to find the solution, but my guess it's something really simple. It's only about finding it.

[TIHan]

Seems I'm wrong a bit on this. The issue is more complex than I thought. Hard to tell who the real culprit is.

I have another repro that will give the same internal error regardless of optimizations on or off:

let inline call (output: ^R) : ^a = 
    ((^R or ^M) : (static member Return : ^R -> ^a) output)

type T () =
    static member inline Return (x: 'a) : 'b = 
        call Unchecked.defaultof<'b> x

let inline test () : T = 
    T.Return(Unchecked.defaultof<T>)

My head is exploding even looking at this smaller example. I know (^R or ^M) is playing a big factor into this. Going to punt this as I'm not familiar with constraint solver's rules.

[dsyme]

I am recording a link to this bug in https://github.com/dotnet/fsharp/pull/6805 to make sure we capture a definitive status for it as part of that work