Inconsistent behaviour when performing case analysis on appeal to the induction hypothesis in Harpoon

[MartyO256]

Load the following signature:

LF kind : type =
| sigma : kind -> (con -> kind) -> kind
and con : type =
; --name kind K. --name con C.
LF cn-of : con -> kind -> type =;
LF cn-equiv : con -> con -> kind -> type =;
LF kd-sub : kind -> kind -> type =;

LF kd-wf : kind -> type =
| kd-wf/sigma :
  kd-wf K1 ->
  ({ a : con } cn-of a K1 -> kd-wf (K2 a)) ->
    kd-wf (sigma K1 K2)
; --name kd-wf Dwf.

LF single : kind -> (con -> kind) -> type =
| single/sigma :
  single K1 K1s ->
    ({ a : con } single (K2 a) (\b. K2s a b)) ->
    single
      (sigma K1 (\a. K2 a))
      (\b. sigma (K1s (pi1 b))
      (\x. K2s (pi1 b) (pi2 b)))
; --name single Dsing.

schema conbind-reg =
  some [K : kind, wf : kd-wf K]
  block (a : con, da : cn-of a K)
;

LF single-omnibus/e : kind -> (con -> kind) -> type =
| single-omnibus/i :
  ({ a : con } cn-of a K -> kd-sub (Ks a) K) ->
  ({ a : con } cn-of a K ->
   { b : con } cn-of b (Ks a) ->
   cn-equiv a b (Ks a)) ->
    single-omnibus/e K Ks
;

proof single-omnibus :
  (g : conbind-reg)
  [g |- single K (\a. Ks)] ->
  [g |- kd-wf K] ->
    [g |- single-omnibus/e K (\a. Ks)] =
/ trust /
?
;

Then, input the following commands:

split x
invert x1
by single-omnibus [_, b : block (c : con, dc : cn-of c _) |- Dsing1[.., b.c]] [_, b |- Dwf1[.., _, b.dc]] as D unboxed

We get this metavariable:

D :
  (g, b : block (c : con, dc : cn-of c _) |-
      single-omnibus/e (K3[.., b.1]) (\a. K4[.., b.1, a]))

The hole in dc : cn-of c _ should have been instantiated with K1[..] since it can be inferred from the usage of dc in Dwf1.

That notwithstanding, case analysis using either of msplit D, split [_ |- D] and invert [_ |- D] fails with the following exception:

Uncaught exception.
Please report this as a bug.
Internal error. (State may be undefined.)
Failure("Found head that is a Proj?? - nested Proj not allowed")
Raised at file "src/core/error.ml", line 116, characters 4-139
Called from file "src/core/error.ml", line 27, characters 11-16

This error does not appear in the debug log, which reads that [harpoon-split] generated 1 cases, and the correct output metavariables are logged:

X :
  (g, c : con, z2 : cn-of c _, a : con,
    x : cn-of a (K5[.., c]) |-
      kd-sub (K6[.., c, a]) (K5[.., c])),
X1 :
  (g, c : con, y3 : cn-of c _, a : con,
    z : cn-of a (K5[.., c]), b1 : con,
    y : cn-of b1 (K6[.., c, a]) |-
      cn-equiv a b1 (K6[.., c, a]))

This error is especially weird since it is not thrown when we avoid introducing the metavariable D by simply using the invert tactic directly:

invert single-omnibus [_, b : block (c : con, dc : cn-of c _) |- Dsing1[.., b.c]] [_, b |- Dwf1[.., _, b.dc]]

[pientka]

This seems a Harpoon issue which should be fixed; but for now we can work around this issue by providing the explicit Beluga program.