[kazinator]

Even if environments are immutable, the problem has to be solved somehow that the environments are hierarchical. Newly instantiated versions of a sub-environment share the same super-environment. For instance, a local tail call occurring in the scope of some stable outer bindings, capturing different versions of the tail call inner variables.

[catnaroek]

I fail to understand why hierarchical environments pose a problem for HOAS. Environments map variables to their values, and they're used to give meaning to non-closed terms (containing variables that aren't bound within the term itself).

The whole point to HOAS is making unbound variables irrepresentable in the first place (which is the source of the accidental variable capture problem), eliminating the need for environments as separate data structures. For example, this is the HOAS representation of closed terms of the untyped lambda calculus:

    datatype term = Lam of term -> term
                  | App of term * term

Note there is no need for a separate constructor for free variables.