Type reconstruction fails in Harpoon in the variable case for context schemas of alternating assumptions

[MartyO256]

Load the following signature using Harpoon:

LF kind : type =;
LF con : type =;
LF etp : type =;
LF eterm : type =;
LF map : con -> eterm -> type =;

schema can-map-ctx =
  % evar
  block (ex : eterm) +
  % can-map-bind
  some [m : eterm]
  block (a : con, at : map a m);

LF can-map/e : con -> type = can-map/i : { M : eterm } map C M -> can-map/e C;

proof can-map :
  (g : can-map-ctx)
  { C : [g |- con] }
  [g |- can-map/e C] =
/ total 1 /
?
;

Then, input the following commands:

msplit C
session serialize

Upon type reconstruction, the following error is thrown:

Uncaught exception.
Please report this as a bug.
Internal error. (State may be undefined.)
File "src/core/reconstruct.ml", line 2248, characters 11-16: Pattern matching failed

The same error is thrown if the theorem is solved with solve [_ |- can-map/i _ #p.at] before serializing.

Harpoon fails to reconstruct the serialized variable case.
This seems to only happen when dealing with schemas comprised of alternating assumptions, because that error does not arise using the same commands in the following signature.

In other proofs where this error occurs, it is possible to comment out the variable case in order to pass type reconstruction, without using the / trust / totality declaration.
Type reconstruction should still fail without the variable case because of non-exhaustive pattern matching.

LF kind : type =;
LF con : type =;
LF etp : type =;
LF eterm : type =;
LF map : con -> eterm -> type =;

schema can-map-ctx =
  % can-map-bind
  some [m : eterm]
  block (a : con, at : map a m);

LF can-map/e : con -> type = can-map/i : { M : eterm } map C M -> can-map/e C;

proof can-map :
  (g : can-map-ctx)
  { C : [g |- con] }
  [g |- can-map/e C] =
/ total 1 /
?
;

Executing the first scenario in debug mode yields the following backtrace for the error:

Raised at file "src/core/reconstruct.ml", line 2248, characters 11-512
Called from file "list.ml", line 92, characters 20-23
Called from file "src/core/reconstruct.ml", line 2528, characters 25-65
Called from file "src/core/reconstruct.ml", line 2111, characters 17-46
Called from file "src/core/reconstruct.ml", line 2072, characters 6-32
Called from file "src/core/reconstruct.ml", line 2545, characters 7-90
Called from file "src/core/reconstruct.ml", line 2111, characters 17-46
Called from file "src/core/reconstruct.ml", line 2656, characters 21-71
Called from file "src/core/recsgn.ml", line 991, characters 11-181
Called from file "list.ml", line 92, characters 20-23
Called from file "src/core/recsgn.ml", line 1095, characters 9-63
Called from file "src/core/recsgn.ml", line 224, characters 19-34
Called from file "src/core/recsgn.ml", line 225, characters 19-36
Called from file "src/core/recsgn.ml", line 225, characters 19-36
Called from file "src/core/recsgn.ml", line 225, characters 19-36
Called from file "src/core/recsgn.ml", line 225, characters 19-36
Called from file "src/core/recsgn.ml", line 225, characters 19-36
Called from file "src/core/recsgn.ml", line 225, characters 19-36
Called from file "src/core/recsgn.ml", line 225, characters 19-36
Called from file "src/core/recsgn.ml", line 1184, characters 15-33
Called from file "src/core/load.ml", line 94, characters 27-49
Called from file "src/core/load.ml", line 142, characters 4-22