Wrong error message on recursive call using unbound meta-level identifier

[MartyO256]

Load the following signature:

LF nat : type =
  | z : nat
  | s : nat → nat
;

LF leq : nat → nat → type =
  | leq_z : leq z N
  | leq_s : leq N1 N2 → leq (s N1) (s N2)
;

proof trans : [⊢ leq N1 N2] → [⊢ leq N2 N3] → [⊢ leq N1 N3] =
/ total 1 /
intros
{ N : ( |- nat), N1 : ( |- nat), N2 : ( |- nat)
| x : [ |- leq N N1], x1 : [ |- leq N1 N2]
; split x as
  case leq_s:
  { X : ( |- nat), X1 : ( |- nat), N2 : ( |- nat), X2 : ( |- leq X X1)
  | x : [ |- leq (s X) (s X1)], x1 : [ |- leq (s X1) N2]
  ; split x1 as
    case leq_s:
    { X : ( |- nat),
      X1 : ( |- nat),
      X4 : ( |- nat),
      X2 : ( |- leq X X1),
      X5 : ( |- leq X1 X4)
    | x : [ |- leq (s X) (s X1)], x1 : [ |- leq (s X1) (s X4)]
    ; ?
    }
  }
  case leq_z:
  { N1 : ( |- nat), N2 : ( |- nat)
  | x : [ |- leq z N1], x1 : [ |- leq N1 N2]
  ; solve [ |- leq_z ]
  }
}
;

There is no meta-variable Q in the the remaining subgoal's context. Using by trans [ |- Q] [ |- X5] as L unboxed results in a "Recursive call not structurally smaller" error as opposed to an "Unbound meta-level identifier: Q" error.

[tsani]

The way Beluga deals with with out-of-scope metavariables is kind of weird. It doesn't immediately produce an error, because there's one situation where free metavariables are actually important, and that's in type signatures where they are automatically abstracted. So internally, what one has to do is explicitly to forbid free variables by scanning the term to see if there are any.

So the reason you get a recursive call not structurally smaller error is that internally [|- Q] is a free variable and you're using it in the first argument of a recursive call, which must be unifiable with one of the generated valid recursive calls. The free variable won't unify with anything, so Beluga just thinks you tried a bogus recursive call.

I think that to resolve this, one needs to explicitly forbid free metavariables in any box embedded in a Beluga expression.

[MartyO256]

Closed by #266. The free meta-variable Q is disallowed.

Theorem: trans
intros <- split x (case leq_s) <- split x1 (case leq_s)
Meta-context:
  X : ( |- nat)
  X1 : ( |- nat)
  X4 : ( |- nat)
  X2 : ( |- leq X X1)
  X5 : ( |- leq X1 X4)
Computational context:
  x : [ |- leq (s X) (s X1)]
  x1 : [ |- leq (s X1) (s X4)]
--------------------------------------------------------------------------------
[ |- leq (s X) (s X4)]
> by trans [ |- Q] [ |- X5] as L unboxed
File "<prompt>", line 1, column 15
Error: This free meta-variable is illegal.