IntersectMBO / IntersectMBO/plutus
PLC.eraseTerm is overly constrained to non-debruijn Terms
- Dominant language
- Haskell
- Stars
- 1.6k
- Forks
- 508
- Avg merge
- 3d 10h
- Merged PRs (30d)
- 22
Description
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.
Contributor guide
Assessment
This issue has not been assessed yet.