What typing logic compels me to have the same return-types for GADT function alternatives?

Question

In this question, it was explained to me how to correctly pattern-match GADT types to get alternative return types using universally quantified type variables and locally abstract types. Notwithstanding the misconceptions in my original example, the explanation did not express: (1) how the type matching is done given that the type system seem to require, when using universally quantified type variables, that alternative branches have the same return type and (2) show an elegant way to mix universally quantified variables and locally abstract type for desired GADT return type outcome.

The type from the original question cited above is:

type
  liLabel_t = string        (* Instruction name (label) *)
and
  context_t = string
and
  'a context_list_t = 'a list
and
  'a liChooser_t = 'a -> int    (* get index of i-th list entry *)
and
  ('a, 'b) liInstr_t =
    LiExec: 'a -> ('a, 'b) liInstr_t        (* executable operation *)
  | LiExecTRY: ('a, _) liInstr_t        (* Ignore: Experiment on GADT *)
  | LiLab: liLabel_t -> ('a, 'b) liInstr_t  (* instruction label *)
  | LiLabTRY: (liLabel_t, _) liInstr_t      (* Ignore: Experiment on GADT *)
  | LiSeq: 'a liChooser_t * 'b list -> ('a, 'b) liInstr_t   (* sequence *)
  | LiAlt: 'a liChooser_t * 'b list -> ('a, 'b) liInstr_t   (* choice *)
  | LiLoop: 'a liChooser_t * 'b list -> ('a, 'b) liInstr_t  (* loop *)
  | LiName: 'a liChooser_t * liLabel_t * 'b context_list_t ->
    ('a, 'b) liInstr_t              (* change context *)
  | Err_LiInstr: ('a, 'b) liInstr_t     (* error handling *)
  | Nil_LiInstr: ('a, 'b) liInstr_t     (* no action *)

In experimenting, when alternatives all have integer return types such as in:

let ft1:   'b 'c. ('b, 'c) liInstr_t -> 'b = function
(* *)  | LiExec n -> 2
(* *)  | LiExecTRY -> 24
(* *)  | LiLab s -> 4 
(* *)  | LiLabTRY -> 44
(* *)  | LiSeq (f, il) -> 42 
(* *)  | LiAlt (f, il) -> 51
(* *)  | LiLoop (f, il) -> 52
(* *)  | LiName (f, il, ic) -> 53
(* *)  | Err_LiInstr -> 54
(* *)  | Nil_LiInstr -> 55
      *               ;;

I receive the error:

Line 2, characters 21-22:
2 | (* *)  | LiExec n -> 2
                         ^
Error: This expression has type int but an expression was expected of type
         liLabel_t = string

and when I comment out these branches that expect string types in their GADT parameters (like so):

(* * )  | LiLab s -> 4 
(* *)  | LiLabTRY -> 44
( * *)

I get the errors:

 ...
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
LiLab _
Lines 1-11, characters 45-26:
...
Error: This definition has type 'c. (int, 'c) liInstr_t -> int
       which is less general than 'b 'c. ('b, 'c) liInstr_t -> 'b

Ignoring the non-exhaustive pattern-matching warning (which is due to variants being commented out), we have a less general type definition of the function. The explanation for this is found in the answers to the original question.

If, however, all the branches have the string type, we sometimes get a similar "less general" error as above but mostly the error:

Line 3, characters 22-26:
3 | (* *)  | LiExecTRY -> "24"
                          ^^^^
Error: This expression has type string but an expression was expected of type
         b

I have not yet figured out why this behaviour, but a suspicion is that the branches:

(* *)  | LiExecTRY -> "24"
(* *)  | LiLab s -> "4" 

if available, somehow compel one to have a string return type for all variants whereas arbitrary types could be returned if they were not used. In that wise, it seems to me that their LiLabel_t (i.e., string) type argument in the GADT is doing this coercion. But how?

If we use local abstract types with all return types being integers, as in:

# let ft1: type b c. (b, c) liInstr_t -> b = function
(* *)  | LiExec n -> 2
(* *)  | LiExecTRY -> 24
...

we get the error

Line 2, characters 21-22:
2 | (* *)  | LiExec n -> 2
                         ^
Error: This expression has type int but an expression was expected of type b

which is as expected as explained in answers to the original question on GADT and local abstract types: the abstract return type b was expected as it was never matched via equational constraints in the GADT to a more concrete type. A similar error arises when I change all the return types (except the first) to string.

My overall questions, effectively raised within the original GADT question are:

1. In my examples, why were all my return types compelled to be int, or to be string (i.e., LiLabel_t) except maybe for the first variant, before being rejected later for being less general than the return type b. What is the reasoning followed within the type checker?
2. Is there an elegant way to combine, in various permutations, universally quantified types and locally abstract types in GADT functions, as there apparently are no syntactically correct ways of doing so. For, if we try to mix universally quantified type variables and locally abstract type variable, we always get an error such as:

Line 1, characters 10-14:
1 | let ft1: (type d) 'b 'c. ('b, 'c) liInstr_t -> d = function
              ^^^^
Error: Syntax error

Answer 1

Question 1: Your example can be reduced to

type ('a,'b) t =
| A of 'a 
| B: (string,_) t

let error (x:('a,'b) t) : 'a= match x with
| A n -> 2
| B -> "hi"

The first branch implies that 'a = int. Then the second branch B has type (string,'c) t, which implies that ('a,'b) t=(string,'c) t and thus 'a = string, which is a contradiction. Indeed, only abstract types can have local equation in pattern matching and 'a and 'b are unification type variables.

(It is hard to guess what went wrong in the other cases, that you only ever hinted at, so I will ignore them.)

Question 2: If you return string in all branches, then your function

let ok (x:('a,'b) t): 'a= match x with
| A n -> n
| B -> "hi"

is well typed by unifying 'a with string, giving the type (string,'b) t -> string to ok. But if you ask the typechecker to check that the type is polymorphic, it will notify you that the type of ok is not polymorphic:

let not_polymorphic: 'a 'b. ('a,'b) t -> 'a= function
| A n -> n
| B -> "hi"

You can notice here that the polymorphism check is done after typechecking the body of the function. Thus the error mentions the inferred type for the function body:

Error: This definition has type 'c. (string, 'c) t -> string
       which is less general than 'a 'b. ('a, 'b) t -> 'a

Question 3. Yes, it is possible, but this is uncommon occurrence

 let f (type d) (x:d) =
  let g : 'a 'b. ('a,'b) t -> d = fun _ -> x
 in g

Most use cases are far better served by the shorthand syntax:

let f: type a b d. d -> (a,b) t -> d = fun d _ -> d

P.S: Would you mind asking one question at a time after trying to reduce your problematic case? It is hard to guess the root issues of the later questions when you layer questions upon questions.