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

plutus/plutus-core/plutus-core/src/PlutusCore/Compiler/Erase.hs

Lines 8 to 16 in d99ba33

	{-| Erase a Typed Plutus Core term to its untyped counterpart.
	Restricted to Plc terms with `Name`s, because erasing a (Named-)Debruijn term will
	mess up its debruijn indexing and thus break scope-checking.
	-- FIXME: Lift this restriction of `eraseTerm` for (Named-)DeBruijn terms.
	-}
	eraseTerm :: HasUnique name TermUnique
	=> Term tyname name uni fun ann
	-> UPLC.Term name uni fun ann

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.