Figuring out why these types differ when using a catch all in the pattern matching

I’d like some help with understanding how type inference affects the following code, which comes from a previous question (which after some thoughts I’ve simplified to the following):

type 'a result =
  | Succ of 'a
  | Fail

let first f = function
  | Succ c -> let res = f c in Succ res
  | fail   -> fail

let second f = function
  | Succ c -> let res = f c in Succ res
  | Fail   -> Fail

My question is: why does f in first have type ('a -> 'a) but f in second have type ('a -> 'b)?

You can see it here.

>Solution :

• The two occurrences of Fail in Fail -> Fail in second are treated as two distinct values, and thus are allowed to have different types 'a result and 'b result, but
• The two occurrences of fail in fail -> fail in first are treated as the same value, and thus cannot change types.

Or at least the type inference system doesn’t allow it to change types. I’m not sure whether that’s a specification or a quirk of this particular interpreter.

As food for thought, a third version:

let third f r = match r with
  | Succ c -> Succ (f c)
  | _ -> r

You and I know that if we reach the _ case of the pattern-match, it means that r is Fail and could be of any 'b result type, but what the compiler sees is that r is of type 'a result since it’s the input, and so 'a == 'b.