Type mismatch error in result type

Question

I played with writing the type of the result and various functions and came across a type mismatch error that I cannot explain. Here is a minimal example:

type ('a, 'b) result = | Success of 'a | Failure of 'b list let apply fr xr = match fr, xr with | Success f, Success x -> Success (fx) | Failure _, Success _ -> fr | Success _, Failure _ -> xr | Failure a, Failure b -> Failure (List.concat [a; b]) 

Compiling this code causes the following error:

 init.fsx(8,31): error FS0001: Type mismatch. Expecting a ('a,'b) result but given a (('c -> 'a),'d) result The resulting type would be infinite when unifying ''a' and ''b -> 'a' 

If you change the apply function as follows, it compiles correctly:

 let apply fr xr = match fr, xr with | Success f, Success x -> Success (fx) | Failure a, Success _ -> Failure a | Success _, Failure b -> Failure b | Failure a, Failure b -> Failure (List.concat [a; b]) 

Why using a matching value (here fr or xr) doesn't work, but building a new Failure value does?

Answer 1

The critical thing to understand here is that the type of discriminatory union applies to all its cases. Even if you "only" reuse Failure instances from the function parameter as the return value, all return values, including Success cases, must be of the same type as this parameter.

Thus, using fr and xr , because the return values ​​limit their types to the same as the return type of apply .

But there is also a line that accepts the Success f parameter to return the Success (fx) value! If these two must be of the same type, type fx must be type f ! This is a function that returns a function of its type, regardless of how many times you use it; such an infinite type is invalid and causes a compiler error.

By creating new instances for the return values, you allow the return type of the apply type to differ from the types of its parameters. Then the compiler can provide f and its return value for different types, avoiding the infinite type of function.

Answer 2

Here is the error.

In this line:

 Success f, Success x -> Success (fx) 

you define 'a as a type of function, and as a result, your return 'a also a function.

but when you do

 | Failure _, Success _ -> fr 

this fr has the same type of function, but not applicable here.

On the contrary, creating a new object gives it a new type, which can be used by the fact that the type of success is now the result of a function in the second case