Unapplied meta-functions should be eagerly applied

[eelcovisser]

Meta-function is not lifted from map construction in following rule:

  E |- bindVar(x, v) --> {x |--> allocate(v), E}.

[vvergu]

This is a bit trickier to fix. It's not limited to meta-functions, but meta-functions are corner case.

In your example you want an arrow coercion to take place inside a map. The difficulty is that the type mismatch is not local to the term x |--> allocate(v), which is a valid term. The mismatch appears between the term x |--> allocate(v) and E and so you need an arrow coercion Map(String, allocate__meta) --> Map(String, V).

In this particular example the correct outcome is to eagerly reduce all meta-functions which are not explicitly reduced.

I think the editor behavior is correct for the the general case when allocate(v) is not a meta-function.

[eelcovisser]

This is not a case of a coercion. Applications of meta-functions need to be lifted out of term construction in general. This is a different transformation.