描述
Currently the PIR inliner relies on global uniqueness, but doesn’t perform renaming itself. No renaming => no marking => the inliner starts in the initial state of Quote, i.e. counting from 0 => subsequent renaming of subterms can rename bound variables to free ones or to ones already bound by unrelated bindings. It’s what I got by staring at the output of the scoping tests, e.g.
DuplicateBindersInTheOutput (fromList [TypeName (TyName {unTyName = Name {_nameText = "a", _nameUnique = Unique {unUnique = 12}}})]) (fromList [TypeName (TyName {unTyName = Name {_nameText = "a", _nameUnique = Unique {unUnique = 11}}}),TypeName (TyName {unTyName = Name {_nameText = "a", _nameUnique = Unique {unUnique = 12}}})])
when checking that transformation of
[
(let
(nonrec)
(termbind
(nonstrict)
(vardecl a_11 a_1)
[
(error
[
(lam a_9 (type) [ [ (lam a_10 (type) [ a_4 a_10 ]) a_3 ] a_9 ])
a_2
]
)
a_0
]
)
[ (iwrap a_5 [ (lam a_12 (type) [ a_7 a_12 ]) a_6 ] a_8) a_11 ]
)
a_0
]
to
[
[
(iwrap a_5 [ (lam a_12 (type) [ a_7 a_12 ]) a_6 ] a_8)
[
(error
[
(lam a_11 (type) [ [ (lam a_12 (type) [ a_4 a_12 ]) a_3 ] a_11 ])
a_2
]
)
a_0
]
]
a_0
]
is correct
If I'm reading it correctly in the above case the body of a_11 gets substituted for a_11, which causes renaming of the body, which bumps lam a_10 to lam a_12, which clashes with an existing binding (not in the variable capture sense, it doesn't create an ill-scoped term, just one not satisfying global uniqueness).
May apply to the UPLC inliner as well, although scoping tests for that one don't fail, so maybe it doesn't.
Breaking global uniqueness while simultaneously relying on it results in undefined behavior (unless proven otherwise in a specific case), hence we should fix this.
PlutusIR.Transform.NonStrict doesn’t perform renaming either, but it’s not clear whether it’s fine for it to break global uniqueness or not, so this should be investigated too.