Type erasure issue in translated program from Harpoon proof

[MartyO256]

Load the following signature:

LF kind : type = sigma : kind -> (con -> kind) -> kind
and con : type =;
LF kind-eq : kind -> kind -> type = kind-eq/i : kind-eq K K;
LF sg : type = sg/sigma : sg -> (con -> sg) -> sg; --name sg S.
LF sg-fst : sg -> kind -> type =
  sg-fst/sigma :
  sg-fst S1 K1 ->
  ({ a : con } sg-fst (S2 a) (K2 a)) ->
    sg-fst (sg/sigma S1 S2) (sigma K1 K2);

schema conblock = block (a : con);

proof sg-fst-fun :
  (g : conblock)
  [g |- sg-fst S K] ->
  [g |- sg-fst S K'] ->
    [g |- kind-eq K K'] =
/ total 1 /
intros
{ g : conblock, S : (g |- sg), K : (g |- kind), K' : (g |- kind)
| x : [g |- sg-fst S K], fst : [g |- sg-fst S K']
; split x as
  case sg-fst/sigma:
  { g : conblock,
    S1 : (g |- sg),
    S2 : (g, a : con |- sg),
    K1 : (g |- kind),
    K2 : (g, a : con |- kind),
    K' : (g |- kind),
    Dfst : (g |- sg-fst S1 K1),
    Dfst1 : (g, a : con |- sg-fst S2 K2)
  | x : [g |- sg-fst (sg/sigma S1 (\x2. S2)) (sigma K1 (\z. K2))],
    fst : [g |- sg-fst (sg/sigma S1 (\x2. S2)) K']
  ; split fst as
    case sg-fst/sigma:
    { g : conblock,
      S1 : (g |- sg),
      S2 : (g, a : con |- sg),
      K1 : (g |- kind),
      K2 : (g, a : con |- kind),
      K3 : (g |- kind),
      K4 : (g, a : con |- kind),
      Dfst : (g |- sg-fst S1 K1),
      Dfst1 : (g, a : con |- sg-fst S2 K2),
      Dfst2 : (g |- sg-fst S1 K3),
      Dfst3 : (g, a : con |- sg-fst S2 K4)
    | x : [g |- sg-fst (sg/sigma S1 (\x2. S2)) (sigma K1 (\z. K2))],
      fst : [g |- sg-fst (sg/sigma S1 (\x2. S2)) (sigma K3 (\z. K4))]
    ; split sg-fst-fun [_ |- Dfst] [_ |- Dfst2] as
      case kind-eq/i:
      { g : conblock,
        S1 : (g |- sg),
        S2 : (g, a : con |- sg),
        K3 : (g |- kind),
        K2 : (g, a : con |- kind),
        K4 : (g, a : con |- kind),
        Dfst : (g |- sg-fst S1 K3),
        Dfst1 : (g, a : con |- sg-fst S2 K2),
        Dfst2 : (g |- sg-fst S1 K3),
        Dfst3 : (g, a : con |- sg-fst S2 K4)
      | x : [g |- sg-fst (sg/sigma S1 (\x2. S2)) (sigma K3 (\z. K2))],
        fst : [g |- sg-fst (sg/sigma S1 (\x2. S2)) (sigma K3 (\z. K4))]
      ; split sg-fst-fun [_, a : con |- Dfst1] [_, a : con |- Dfst3] as
        case kind-eq/i:
        { g : conblock,
          S1 : (g |- sg),
          S2 : (g, a : con |- sg),
          K3 : (g |- kind),
          K4 : (g, a : con |- kind),
          Dfst : (g |- sg-fst S1 K3),
          Dfst1 : (g, a : con |- sg-fst S2 K4),
          Dfst2 : (g |- sg-fst S1 K3),
          Dfst3 : (g, a : con |- sg-fst S2 K4)
        | x : [g |- sg-fst (sg/sigma S1 (\x2. S2)) (sigma K3 (\z. K4))],
          fst : [g |- sg-fst (sg/sigma S1 (\x2. S2)) (sigma K3 (\z. K4))]
        ; ?
        }
      }
    }
  }
}
;

Upon completing the proof using solve [_ |- kind-eq/i ], the following translated program is output:

rec sg-fst-fun :
  (g : conblock)
  [g |- sg-fst S K] ->
  [g |- sg-fst S K'] ->
    [g |- kind-eq K K'] =
fn z => fn y1 =>
  let [_ |- sg-fst/sigma Dfst (\a. Dfst1)] = z in
  let [_ |- sg-fst/sigma Dfst2 (\a. Dfst3)] = y1 in
  let [_ |- kind-eq/i ] = sg-fst-fun [_ |- Dfst] [_ |- Dfst2] in
  let [_, x1 |- kind-eq/i ] =
      sg-fst-fun [_, a : con |- Dfst1] [_, a : con |- Dfst3]
  in
  [_ |- kind-eq/i ]
;

This program raises this uncaught exception:

File "src/core/apxnorm.ml", line 512, characters 27-32: Pattern matching failed

This is due to the erasure of the type to x1 : con in let [_, x1 |- kind-eq/i ] = sg-fst-fun [_, a : con |- Dfst1] [_, a : con |- Dfst3].
Adding the type back solves the issue.

[sjjs7]

After encountering this issue, I believe it has to do with the fact that the internal syntax of the case pattern uses as its LF context the dctx_hat, which when printed to the file will only print the names of variables and omit type info (opposed to printing a dctx).