Internal error: Undefined or unsolved type variable with SRTP chains

[realvictorprm]

While digging into #4924 I found an example with SRTP chains which produces an internal error.

Repro steps

Try compiling this in FSI:

type Bar =
    static member inline bar (f: ^c -> ^b, (a, b) : ^c) : ^b = f (a, b)
    static member inline bar (f: ^c -> ^b, (a, b, c) : ^c) : ^b = f (a, b, c)

let inline bar_(f:^a -> ^b) (x: ^c) : ^d when (^bar or ^d) : (static member bar : (^a -> ^b) * ^c -> ^d) = 
    ((^bar or ^d) : (static member bar : (^a -> ^b) * ^c -> ^d)(f, x))

type Foo =
    static member inline foo (f : ^a -> ^b, (a, b)) : ^c = bar_ f (a,b)
    static member inline foo (f : ^a -> ^b, (a, b, c)) : ^c = bar_ f (a,b,c)

let inline foo< ^foo, ^a, ^b, ^c, ^d when (^foo or ^a) : (static member foo : (^a -> ^b) * ^c -> ^d)> (f: ^a -> ^b) (x: ^c) : ^d =
        ((^foo or ^a) : (static member foo : (^a -> ^b) * ^c -> ^d)(f, x))

let inline callFoo (f: ^a -> ^b) (x: ^c) : ^d when (Foo or ^d) : (static member foo: (^a -> ^b) * ^c -> ^d)=
    foo<Foo, ^a, ^b, ^c, ^d> f x

let test = (fun (a : int, b : int) -> (a, b))

let appliedFoo : int * int -> int * int =
    callFoo test

Will produce an error like: FS0073: Internal Error: Undefined or unsolved type variable: ^_?35727 for the last function appliedFoo.

Expected behavior

No internal error.

Actual behavior

An internal error is thrown.

Known workarounds

None

Related information

F# 4.5

[cartermp]

Labeling as a bug due to the internal error - whether or not this should actually compile is a separate question, but from a usability standpoint the internal error needs to be done away with so your entire editor won't go red.

[dsyme]

From compiler office hours:

@dsyme says:

1. A stack trace would be the first thing, to find which phase.
2. Minimizing the sample more if it can be done

@realvictorprm says

1. The compiler noticed that something went super wrong at the last stage, code generation (edited) I already tried 2. it was complex enough to get it down to what I wrote

@dsyme says

OK, then use the debugger to determine which construct still contains an unsolved type variable. There are several possibilities.

[realvictorprm]

I debugged the compiler and found out:

1. This should could not compile, ^bar should have been inferred to be of type obj
2. I discovered that the compiler does not infer obj as default type in inline exprs if full annotations are given in partial function application.

[dsyme]

I discovered that the compiler does not infer obj as default type in inline exprs if full annotations are given in partial function application.

Is this in the body of the inline expression, or the copy of the inline expression (after it's been inlined into a callsite)?

[realvictorprm]

Part of the call stack is:

[realvictorprm]

I think I've got a different reproduction for this issue which is based on the code from #4924.

type Either<'l,'r> = Left of 'l | Right of 'r
type Maybe<'a> = Either<unit,'a>

let inline addfst x y = (x, y)

module Either =

    let rmap f : Either<'l,'a> -> Either<'l,'b> =
        function Right x -> Right (f x) | Left e -> Left e

type Multifunctor() =
    static member inline mapB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^a * ^b0 = (a, f b)
    // If you comment the line below you'll get an internal error undefined or unsolved type variable
    // Otherwise it compiles but you won't get compile errors although the type signature ofwhatInTheWorld is wrong
    // static member inline mapB (f : ^b -> ^b0, x : Either< ^a,^b>) : Either< ^a,^b0> = Either.rmap f x
    static member inline mapB (f : ^b -> ^b0, (a : ^a, b : ^b, c : ^c)) : ^a * ^b0 * ^c = (a, f b, c)

let inline mapB_< ^mf, ^f, ^a, ^b when (^mf or ^a) : (static member mapB : ^f * ^a -> ^b)> (f : ^f, x : ^a) : ^b =
    ((^mf or ^a) : (static member mapB : ^f * ^a -> ^b) (f, x))

type Multitraverse() =
    static member inline traverseBB (f : ^b1 -> ^b2, x : ^a1 * ^c2 * ^d3) = fun a -> printfn "hi"; a
    static member inline traverseBB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^b1
        when (Multifunctor or ^b0) : (static member mapB : _ * ^b0 -> ^b1) =
            mapB_<Multifunctor,_,_,_> (addfst a, (f b))

let inline traverseBB_< ^mf, ^a, ^b, ^c, ^d when (^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d)> (f : ^a -> ^b, x : ^c) : ^d =
    ((^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) (f, x))

let inline traverseBB (f : ^a -> ^b) (x : ^c) : ^d
    when (Multitraverse or ^c) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) =
        // The intent of requiring monad is just trying to be lawful
        traverseBB_<Multitraverse,^a,^b,^c,^d> (f, x)

let private maybeZero : int -> Maybe<int> =
    function
    | 0 -> Right 0
    | _ -> Left ()

// This type clearly does not match the implementation, and yet it type checks
// full signature is: int -> Maybe<int> -> list<string> * int -> Either<string,list<string>>
// This selects the function traverseBB : (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^b1
//                                        (f : int -> Maybe<int>, (a : list<string>, b : int)) : Either<string, list<string>>
// Inner selected function is: mapB : _ * ^b0 -> ^b1
//                                  : (^x -> (list<string> * ^x)) * Maybe<int> -> Either<string, list<string>>
// Which would be:             mapB (f : ^b/int -> ^b0/list<string> * int, x : Either< ^a/unit, ^b/int>) : Either< ^a/unit,^b0/list<string> * int>
let private whatInTheWorld : list<string>*int -> Either<unit,list<string> * float> =
    traverseBB maybeZero

[dsyme]

I referenced this in #6805 to make sure we pin down known status for this in that branch