Hi Chris,
despite the claim in a comment in your module, your type invariant is certainly not inductive: you'll need to describe rather precisely the interplay between the stack and the program counter. I believe you want to write something along the following lines (but I haven't checked any of this):
StackEntry ==
[ procedure : {"MergeSort"},
pc : ValidPC,
A0 : [0 .. N-1 -> 0 .. N-1], \* is this local variable really necessary?
mid : Nat, \* 0 .. N-1 ? (similar for the following)
k : Nat,
i : Nat,
j : Nat,
lo : Nat,
hi : Nat ]
MainPC == {"MS", "Done"}
ProcPC == {"l_1", "l_msl", ..., "l_rtn"}
TypeOK ==
/\ ...
/\ stack \in Seq(StackEntry)
/\ \/ stack = <<>> /\ pc \in MainPC
\/ /\ stack # <<>> /\ pc \in ProcPC
/\ Last(stack).pc = "Done" \* return address from main procedure call
/\ \A i \in 1 .. Len(stack)-1 : stack[i].pc \in {"l_msh", "l_sl1"}
\* return addresses from recursive calls
By the way, you may want to consider simplifying your model by removing some of the auxiliary computations, e.g. replace the while loop at l_sl2 by something like
B := [i \in 0 .. mid-lo |-> A[i+lo]]
and similar for l_sh2. It will be pretty obvious in a second step to refine this assignment into your while loop.
Hope this helps to get you on track,
Stephan