IntersectMBO / IntersectMBO/plutus

PLC.eraseTerm is overly constrained to non-debruijn Terms

Open
#6,014 2 comments 0 reactions 0 assignees View on GitHub
bug Internal Name handling status: triaged tech debt
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

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.