SRTP resolution uses wrong witness, allows unreachable code reached

[gusty]

Using the CompilerMessage attribute is a technique I use a lot and normally it works, in order to give customized compile error messages. Unfortunately there are some isolated cases where the code is reached, despite the attribute.

Repro steps

type Default2 = class end
type Default1 = class inherit Default2 end

type T =
    inherit Default1

    [<CompilerMessage("Message", 01234, IsError = true)>]
    static member        M (_:           unit -> '``Monad<'T>``       , _: Default2) = invalidOp "this code is unreachable"

    static member inline M (x: unit -> 'R                             , _: Default1) = (^R : (static member M : _->_) x) : 'R
    static member inline M (_: unit -> ^t when ^t: null and ^t: struct, _: Default1) = id
    static member        M (_: unit -> list<_>                        , _: T       ) = []

    static member inline Invoke (source: unit ->'R) : 'R =
        let inline call (mthd: 'M, input: unit -> 'I, _output: 'R) = ((^M or ^I) : (static member M : _*_ -> _) input, mthd)
        call (Unchecked.defaultof<T>, source, Unchecked.defaultof<'R>)

let f () = T.Invoke (fun () -> [1])

Expected behavior

The above code should not compile.

Actual behavior

It compiles. Then when calling f () you get the exception at runtime which in theory should be unreachable.

Known workarounds

None that I know.

Related information

Tested in F# 6.0

[T-Gro]

@gusty : Can we please ask you to test on F# 7 ? A few things did change around SRTPs