Type inference fails

[gusty]

Type inference fails in this relatively simple scenario:

Repro steps

Write this:

type T = T with     
    static member        (+.) (T, x) = x : int    
    static member        (+.) (T, x) = x : string
    static member inline Add source = T +. source
    static member        (+.) (T, x) = x

Expected behavior

To compile, or at least type check

Actual behavior

~vs8323.fsx(4,41): error FS0001: This expression was expected to have type
    '_arg3    
but here has type
'b    

Known workarounds

Move the overload up

[dsyme]

@gmpl I think this is by design. Is there a specific reason you think this should compile?

Variations that pass include

type T = T with     
    static member        (+.) (mthd : T, x) : int = x 
    static member        (+.) (mthd : T, x) : string = x 
    static member inline Add source = T +. source
    static member        (+.) (mthd : T, x) : T = x

[gusty]

@dsyme It should compile because the code is correct. If this error is by design what's the specific reason of this error?

Note that the code you posted is not equivalent, the type of the last overload shouldn't be T it should be 'a I mean, a generic type. Why did you move the type annotations to the left side? That shouldn't have any effect, right?

I think this not urgent, but it should be filed as a bug and eventually should be addressed. It's good to have a list of all existing bugs for me or someone else who is reviewing the type inference code.

Let's remove the binding for the first parameter, they are not relevant for this repro.

[smoothdeveloper]

From my superficial understanding, I'd expect stating the type on the function signature:

type T = T with     
    static member        (+.) (T, x) : int = x 

us the same as stating the expression type

type T = T with     
    static member        (+.) (T, x) = (x : int)

[dsyme]

Why did you move the type annotations to the left side? That shouldn't have any effect, right?

Yes, it can have an effect. The type information on the left of all recursive bindings is analyzed prior to the r.h.s. of the first binding. That's always the case for all recursive bindings, regardless of how big the r.h.s. expression is.

For this particular case the error is raised when solving the witness for the constraint during code generation. That does seem like a bug - we should never report errors so late.

Regardless, the best thing to do is really to add full type annotations to signatures in this situation:

type T = 
    | T 
    static member        (+.) (mthd : T, x: int) : int = x 
    static member        (+.) (mthd : T, x: string) : string = x 
    static member        (+.) (mthd : T, x: 'a) : 'a = x
    static member inline Add (source:'a) = T +. source

[gusty]

@dsyme Even full type annotations won't help here, your code works because you moved the last overload up, but otherwise it would keep failing:

type T = 
    | T 
    static member        (+.) (mthd : T, x: int) : int = x 
    static member        (+.) (mthd : T, x: string) : string = x 
    static member inline Add (source:'a) = T +. source
    static member        (+.) (mthd : T, x: 'a) : 'a = x


~vs8323.fsx(6,56): error FS0001: This expression was expected to have type
    'a    
but here has type
>     'a0    

[dsyme]

@gmpl Yes, you're correct. Adding generic parameters to the full type annotation works (it gives an unrelated warning which you can use by using the mangled name op_PlusDot explicitly, there's an issue tracking that somewhere I think)

type T = 
    | T 
    static member        (+.) (mthd : T, x: int) : int = x 
    static member        (+.) (mthd : T, x: string) : string = x 
    static member inline Add (source:'a)  = T +. source
    static member        (+.)<'a> (mthd : T, x: 'a) : 'a = x

[gusty]

@dsyme Very interesting workaround !

[gusty]

@dsyme I didn't realize that this issue seems to be solved in F# 4.1 , at least this repro compiles fine.

Looks like it was solved by the changes I did in type inference in #1530

Funny that I reported a bug without knowing that I had fixed it already.

[dsyme]

@gmpl That's interesting.... thanks for updating. Perhaps add these as new test cases in a PR?