PLC.eraseTerm is overly constrained to non-debruijn Terms

[bezirg]

The eraseTerm function is very simple (as it ought to be), by removing any ast info that contains types.

Previously this eraseTerm it was broken for DeBruijn terms so we decided to constrain this function to non-debruijn terms, by requiring HasUnique name TermUnique

https://github.com/IntersectMBO/plutus/blob/d99ba339726530873ea126b291983c6f2677986b/plutus-core/plutus-core/src/PlutusCore/Compiler/Erase.hs#L8-L16

Previously, if the input TPLC.term is in debruijn (level or index) format, then the resut Var nodes in the UPLC.Term output would end up having sparse debruijn levels or indices.

E.g.

λχ Λα. χ in our de bruijn is λ. Λ *. 2 , but after erase it would end up:

erase (λ. Λ *. 2) === λ . 2

whereas the result should be instead λ.1

Solutions to unconstrain it:

1) make PlutusCore.DeBruijn functions use two separate universes with two separately counting debruijn levels (this has the extra small benefit of having smaller ints at the uplc ast, and thus flat could potentially compact it even more). 2) make a special erase for DeBruijn which would keep a reader counter and decrement the counter at self-recursion and decreement the Var levels/indices accordingly.

[bezirg]

@michaelpj ' comment on this:

June 22, 2021 at 3:27 PM

There's a more general problem that lots of program transformations are invalid if you're using indices, since you can't move around terms with indices without adjusting them.

I'd be tempted to do something like: add an IsRelocatable name empty class, provide an instance for everything except indices, and require it for transformations that move things around.

[effectfully]

make PlutusCore.DeBruijn functions use two separate universes with two separately counting debruijn levels (this has the extra small benefit of having smaller ints at the uplc ast, and thus flat could potentially compact it even more).

I strongly believe that this is what we should do.

Debruijinifining

/\(a_0 :: *) -> \(a_0 : a_0) -> error {a_0 -> a_0} a_0

should give an alpha-equal term back.