Wrong contextual type for meta-variable (M)

[fferreira]

In the example below Beluga provides the type of M is
{M : [g, x : tm, x : tm |- tm]}

Instead of the expected M with only one variable in the context.

tm : type.
lam : (tm -> tm) -> tm.
app : tm -> tm -> tm.

schema ctx = tm;

rec copy : (g : ctx)  [g |- tm] -> [g |- tm] =
fn t => case t of
| [g |- lam M] => ?
;

[ajcave]

The problem is in lfrecon where eta expansion is performed (etaExpandFMV); it doesn't properly weaken the identity substitution