Fresh variable names should avoid both local and global names

[davidweichiang]

define x1 = ((), ());
define y = \a:() . a;
let z = (x1, y) in ()

gives the error

perplc: Name collisions for edge labels: x1
CallStack (from HasCallStack):
  error, called at ./Compile/RuleM.hs:149:11 in main:Compile.RuleM

Originally posted by @davidweichiang in https://github.com/diprism/perpl/issues/126#issuecomment-1262684280

[davidweichiang]

The reason is at AffLin.hs:86:

  let y = newVar localName (`Map.member` tmVars g)

because it also should avoid tmNames g.

[ccshan]

I'm thinking of a fix along these lines...

diff --git a/src/Util/FGG.hs b/src/Util/FGG.hs
index 9f656ab..21e7686 100644
--- a/src/Util/FGG.hs
+++ b/src/Util/FGG.hs
@@ -62,6 +62,7 @@ data EdgeLabel =
   | ElTerminal Factor
   deriving (Eq, Ord)
 instance Show EdgeLabel where
+  show (ElNonterminal (TmVarL x tp)) = "TmVarL[" ++ show x ++ ":" ++ show tp ++ "]"
   show (ElNonterminal tm) = show tm
   show (ElTerminal fac) = show fac

[davidweichiang]

But isn't it a problem affLin to choose a local variable name x that shadows a global variable x? What if rtm uses the global variable x?

[ccshan]

The stance I'm considering is that they're just not the same variable name, so it makes sense for the same term to use both a global variable and a local variable of the same-looking name. On this stance, it's the non-injectivity of show on EdgeLabel that's to blame. (If we have to turn an EdgeLabel into a string for JSON's sake, then maybe we should intern it into a compact ID, actually.)

[davidweichiang]

I see, but am not convinced yet...one consequence of this is that the output of -c becomes less re-compilable than before (cf. #74).