Internal error

[mb64]

I'm trying to go through the NbE example, and got an internal error. I've simplified it to this:

$ cat bug.bel
LF tm : type =
  | abs : (tm → tm) → tm;

rec thing : [⊢ tm] → [⊢ tm] = fn t ⇒ case t of
  | [ ⊢ abs (λx. E)] ⇒ ?hole;
$ beluga bug.bel
## Type Reconstruction begin: bug.bel ##
Internal error (please report as a bug):
[elTerm'] Proj (FMVar _, _)

I've since figured out that the syntax has changed to only allow \ instead of λ, but I'm reporting the bug anyway as requested.

[MartyO256]

This error occurs because λx is parsed as a free meta-variable with name λx, which cannot occur in a projection with the . operator. Like you wrote, \ is expected instead of λ, and error reporting needs improvement. The error is raised from the elTerm' function in the LF reconstruction module: https://github.com/Beluga-lang/Beluga/blob/6f1acde3a32f9228dbd912ca6895207b1afed7b0/src/core/lfrecon.ml#L1948-L1949