Context variable naming conflict when destructuring block

[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
invert single-omnibus [_, b : block (a : con, da : cn-of a _) |- Dsing1[.., b.a]] [_, b |- Dwf1[.., _, b.da]]

This last inversion (functionally equivalent to using the split tactic) on the appeal to the induction hypothesis yields these two metavariables:

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

As in issue #230, there is a naming conflict in the contextual variables in X and X1, where there are two variables a : con.
Manually renaming the con in the block when performing the appeal to the induction hypothesis bypasses this issue.

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

The difference between #230 and this issue is that the renaming needs to occur when destructuring the b : block (a : con, da : cn-of a _) in the inversion.

[MartyO256]

A similar issue arises with the following signature.

LF kind : type = sigma : kind -> (con -> kind) -> kind
and con : type = pi1 : con -> con | pi2 : con -> con; --name con C. --name kind K.

schema conblock = block (a : con);

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 Dsingle single.

LF tidy : kind -> type =
| tidy/sigma :
  tidy K1 ->
  tidy K2 ->
    tidy (sigma K1 (\l. K2)); --name tidy Dtidy tidy.

proof single-tidy :
  (g : conblock)
  [g |- single K (\a. Ks)] ->
    [g, a : con |- tidy Ks[.., a]] =
/ total 1 /
?
;

Using these tactics

split x
by single-tidy [_, a : con |- Dsingle1] as Dtidy2 unboxed

yields this metavariable

Dtidy2 : (g, a : con, a : con |- tidy K4)

which has two a : con as assumptions.
Harpoon seems to internally recognize that these terms are distinct since the theorem may be completed and reconstructed using these tactics.

split x
by single-tidy [_ |- Dsingle] as Dtidy1 unboxed
by single-tidy [_, a : con |- Dsingle1] as Dtidy2 unboxed
solve [g, a : con |- tidy/sigma (Dtidy1[.., pi1 a]) (Dtidy2[.., pi1 a, pi2 a])]

However, doing some case analysis after introducing the metavariable Dtidy2 will result in Dtidy2 : (g, a : con, a : con |- tidy K4) being serialized, which somehow passes type reconstruction afterwards.
This issue has low priority.