Type mismatch error in result type

Question

I was playing around with writing a result type and assorted functions, and came across a type mismatch error I cannot explain. Here is a minimum 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 (f x)
    | Failure _, Success _ -> fr
    | Success _, Failure _ -> xr
    | Failure a, Failure b -> Failure (List.concat [a; b])

Compiling this code produces 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 according to the below, it compiles correctly:

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

Why does using the matched over value (here fr or xr) not work but constructing a new Failure value does?

Answer 1

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

Thus, using fr and xr as return values constrains their types to be identical to apply's return type.

But there's also the line that takes a parameter of Success f to a return value of Success (f x)! If these two are to have the same type, the type of f x must be the type of f! That's a function that returns a function of its own type, no matter how many times you apply it; such an infinite type isn't allowed and causes the compiler error.

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

Answer 2

Here is the error.

In this line:

Success f, Success x -> Success (f x)

you define 'a to be a function type and as a result your return 'a is also a function.

but when you do

| Failure _, Success _ -> fr

this fr has the same function type, but here is unapplied.

In contrast, creating the new object gives it a new type which can use the fact that the success type is now the result of the function in the second case