Arrays extracted two-ways, but end up in the same C++

First.v

(** Arrays in coq*)
Set Implicit Arguments.

Module Array.

(** arrays as a monad. Coq typechecker does not allow `get` to be `array T -> nat -> T` as it should
 and requires the wrong type `array T -> nat -> array T` to always terminate in `array T`. *)
  Inductive array: Type -> Type :=
    | get: forall T, array T -> nat -> array T
    | put: forall T, array T -> nat -> T -> array T
    | empty: forall T,  nat -> T -> array T
    (** Monad implementation *)
    | ret: forall T, T -> array T
    | bind: forall T T', array T -> (T -> array T') -> array T'.
    
  (** arrays axiomatically *)
  Class NativeArray A Array :=
  {
    hget:    nat -> Array -> A;
    hput:    nat -> A -> Array -> Array;
    hempty:  nat -> A -> Array;
  }.

  Parameter Array: Type -> Type.
  Instance nativeArray {T}: NativeArray T (Array T). Admitted.                                   

  (** Define some arrays *)
  Definition m := let zero := empty 4 0 in put zero 2 1.
  Definition h := let zero := hempty 4 0 in hput 2 1 zero.

  (** Two arrays, one a monad and the other a `let` chain *)
  Compute m.
  Compute h.

  (** They look the same in proofs *)
  Theorem equalityBySameness: h = h.
    Proof.
      unfold h.
      assert(m = m). unfold m.
      reflexivity. reflexivity.
    Qed.
End Array.

(** Let's see what we extract to *)
Require Extraction.
Extraction Language JSON.
Separate Extraction Array.m Array.h.

Second.cpp

// $ machcoq Arrays.json
array<nat> m() {
  auto zero = coq_empty((nat)4, (nat)0);
  return coq_put(zero, (nat)2, (nat)1);
}

coq_Array<nat> h() {
  auto zero = hempty((nat)4, (nat)0);
  return hput((nat)2, (nat)1, zero);
}
 /*
    The monadic and axiomatic definitions extract to the same code. 
    
    Given that fact, I think h() and `hget` are better than the monadic `m` and `get` which is the wrong type signature, 
    as get does not return an array<T> but an element of type T. 
`*/