Type-checking error in Harpoon in variable case for schemas with higher-order LF types

[MartyO256]

Load the following signature using Harpoon:

LF kind : type =;
LF con : type =;
LF cn-of : con -> kind -> type =;
LF term : type =;
LF sttp : type =;
LF tm-of : sttp -> term -> con -> type =;
LF sg : type =;
LF kd-wf : kind -> type =;
LF sg-wf : sg -> type =;
LF sg-fst : sg -> kind -> type =;
LF module' : type =;
LF purity : type =;
LF md-of : purity -> sttp -> module' -> sg -> type =;
LF md-fst : module' -> con -> type =;

schema can-md-fst-ctx =
  % termbind-reg
  some [T : con, Dwf : cn-of T t]
  block (x : term, d : { F' : sttp } tm-of F' x T) +
  % modbind-reg
  some [K : kind, S : sg, DwfK : kd-wf K, DwfS : sg-wf S, DfstS : sg-fst S K]
  block (
    a : con, da : cn-of a K,
    m : module', dm : { P' : purity } { F' : sttp } md-of P' F' m S,
    dfst : md-fst m a
  );

LF can-md-fst/e : module' -> type =
| can-md-fst/i : { C : con } md-fst M C -> can-md-fst/e M
;

proof can-md-fst :
  (g : can-md-fst-ctx)
  [g |- md-of pure F M S] ->
    [g |- can-md-fst/e M] =
/ total 1 /
?
;

Then, input the following commands:

split x
session serialize

The following error is thrown:

Uncaught exception.
Please report this as a bug.
Internal error. (State may be undefined.)
Not_found

Using the debug mode, the full backtrace for this error is:

Raised at file "src/core/synint.ml", line 308, characters 11-26
Called from file "src/core/reconstruct.ml", line 2251, characters 14-48
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 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 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

Removing termbind-reg from the schema can-md-fst-ctx as in the following signature, we get a different error message, which reads:

Type-checking error.
Ill-typed expression.
    Expected type:
      [?g[^0] |-
         md-of
           (?pure_109[^0][..])
           (?F_110[^0][..]) (?M_111[^0][..]) (?S_112[^0][..])]
    Inferred type:
      [?g[^0] |-
         {P' : purity}
          {F' : sttp}  md-of P' F' (?#p_118.3[^0][..]) (?X_114[^0][..])]


Raised by primitive operation at file "src/core/id.ml", line 66, characters 34-74

It seems that Harpoon does not properly handle higher-order LF types in schema declarations, at least when reconstructing variable cases involving them.
That particular variable case is expected to be solvable using solve [_ |- can-md-fst/i _ #p.dfst].
The Not_found error may be unrelated to the Type-checking error since the former involves schemas comprised of alternating assumptions which currently raise errors (see #233).

LF kind : type =;
LF con : type =;
LF cn-of : con -> kind -> type =;
LF term : type =;
LF sttp : type =;
LF tm-of : sttp -> term -> con -> type =;
LF sg : type =;
LF kd-wf : kind -> type =;
LF sg-wf : sg -> type =;
LF sg-fst : sg -> kind -> type =;
LF module' : type =;
LF purity : type =;
LF md-of : purity -> sttp -> module' -> sg -> type =;
LF md-fst : module' -> con -> type =;

schema can-md-fst-ctx =
  % modbind-reg
  some [K : kind, S : sg, DwfK : kd-wf K, DwfS : sg-wf S, DfstS : sg-fst S K]
  block (
    a : con, da : cn-of a K,
    m : module', dm : { P' : purity } { F' : sttp } md-of P' F' m S,
    dfst : md-fst m a
  );

LF can-md-fst/e : module' -> type =
| can-md-fst/i : { C : con } md-fst M C -> can-md-fst/e M
;

proof can-md-fst :
  (g : can-md-fst-ctx)
  [g |- md-of pure F M S] ->
    [g |- can-md-fst/e M] =
/ total 1 /
?
;