Printed names of meta-context variables for a hole do not match with their defined names

[Ailrun]

As a demonstration, when I have these holes,

%coverage

LF ty : type =
  | base : ty
  | arr : ty -> ty -> ty
;
%name ty T.

LF tm : ty -> type =
  | abs : (tm A -> tm B) -> tm (arr A B)
  | app : tm (arr A B) -> tm A -> tm B
;
%name tm M.

schema cxt = tm A;

% One-step reduction
LF step : tm A -> tm A -> type =
  | s-beta : step (app (abs M) N) (M N)
  | s-abs : ({x : tm A} step (M x) (M' x)) -> step (abs M) (abs M')
  | s-app-l : step M M' -> step (app M N) (app M' N)
  | s-app-r : step N N' -> step (app M N) (app M N')
;

% Accessibility definition of strong normalization
inductive Sn : (g : cxt) {M : [g |- tm A[]]} ctype =
  | Sn-acc : {M : [g |- tm A[]]}
             ({M' : [g |- tm A[]]} {S : [g |- step M M']} Sn [g |- M'])
             -> Sn [g |- M]
;

inductive Sne : (g : cxt) {M : [g |- tm A[]]} ctype =
  | Sne-var : {#p : [g |- tm A[]]} Sne [g |- #p]
  | Sne-app : Sne [g |- R]
              → Sne [g |- app R N]
;

% Lemma 3.11: Closure Properties of Neutral Terms
rec Sn-Sne : (g : cxt)
             {R : [g |- tm (arr A[] B[])]}
             {N : [g |- tm A[]]}
             Sne [g |- R]
             -> Sn [g |- R]
             -> Sn [g |- N]
             -> Sn [g |- app R N] =
/ total {sn0 sn1} (Sn-Sne g a b r n sne sn0 sn1) /
mlam R, N => fn sne, sn0, sn1 => Sn-acc [_ |- app R N] 
                                   (mlam _L', S => case [_ |- S] of
                                      | [_ |- s-beta] => ?
                                      | [_ |- s-app-l S'] =>
                                            ?
                                      | [_ |- s-app-r S'] =>
                                            ?)
;

bin/beluga <this file> prints these contexts/types

<Position of Hole 0>:
Hole number 0, <anonymous>
  Meta-context:
    z : cxt
    Z : ( |- ty)
    A1 : ( |- ty)
    M : (z, y3 : tm Z[] |- tm A1[])
    N1 : (z |- tm Z[])
  Computation context:
    sne : Sne [_] [ |- arr Z A1] [_ |- abs Z[] A1[] (\x1. M)]
    sn0 : Sn [_] [ |- arr Z A1] [_ |- abs Z[] A1[] (\x1. M)]*
    sn1 : Sn [_] [ |- Z] [_ |- N1]*
  Goal: Sn [_] [ |- A1] [_ |- M[.., N1]]
<Position of Hole 1>:
Hole number 1, <anonymous>
  Meta-context:
    x : cxt
    Y : ( |- ty)
    A1 : ( |- ty)
    M : (x |- tm (arr Y[] A1[]))
    N1 : (x |- tm Y[])
    M'1 : (x |- tm (arr Y[] A1[]))
    S' : (x |- step (arr Y[] A1[]) M M'1)
  Computation context:
    sne : Sne [_] [ |- arr Y A1] [_ |- M]
    sn0 : Sn [_] [ |- arr Y A1] [_ |- M]*
    sn1 : Sn [_] [ |- Y] [_ |- N1]*
  Goal: Sn [_] [ |- A1] [_ |- app Y[] A1[] M'1 N1]
<Position of Hole 2>:
Hole number 2, <anonymous>
  Meta-context:
    y : cxt
    X : ( |- ty)
    A1 : ( |- ty)
    M : (y |- tm (arr X[] A1[]))
    N1 : (y |- tm X[])
    N' : (y |- tm X[])
    S' : (y |- step X[] N1 N')
  Computation context:
    sne : Sne [_] [ |- arr X A1] [_ |- M]
    sn0 : Sn [_] [ |- arr X A1] [_ |- M]*
    sn1 : Sn [_] [ |- X] [_ |- N1]*
  Goal: Sn [_] [ |- A1] [_ |- app X[] A1[] M N']

For me, it looks strange because I defined Sn-Sne with mlam R, N =>, so I think the Meta-context should use R and N instead of M and N1 in this case. Though I'm not sure whether this behavior is intended or not....

[tsani]

I haven't looked closely at this yet, but my suspicion is that the refinement substitution generated by splitting is messing up the names of the variables that were there on the outside.

I'll look into this this afternoon, hopefully.

[tsani]

It turns out that this is a lot more complicated than I first anticipated. The name changes are actually intentional. Beluga can't figure out what the indices of variables appearing in a branch are during indexing, because the refinement substitution isn't computed until type reconstruction. So during type reconstruction these variables get properly indexed using the fmvApxExp function in elBranch. The problem is that this indexing is based on names, and duplicate names get generated by abstraction if we remove the contextual name generation code that I added, and that is at fault for generating N1 in your example. If we remove this renumbering logic, the variables in the branch end up referring to the wrong things in the meta-context and cause strange type mismatches saying that the expected type is the same as the actual type! That's because their printed representations are identical, but the underlying indices differ, and unification cares about indices not strings.

Properly fixing this will probably require thinking really hard about how to eliminate apxnorm to avoid this reindexing at a later time.