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:

Beluga/src/core/lfrecon.ml

Lines 1948 to 1949 in 6f1acde

	| Apx.LF.Root (loc, Apx.LF.Proj (Apx.LF.FMVar _, _), _) ->
	raise (Error.Violation "[elTerm'] Proj (FMVar _, _)")